Types

Previous theme in this lecture -- Keyboard shortcut: 'p'

Next slide in this lecture -- Keyboard shortcut: 'n'

Expressions, Types, and Functions

5. Types

It is hard to justify a text about functional programming without a fair treatment of types. In this chapter we will go over the most important concepts of types, as relevant in the functional programming paradigm.

5.1 Types	5.4 An example of type checking
5.2 Type checking	5.5 Types in functional programming languages
5.3 Static type checking

5.1. Types
Contents Up Previous Next Slide Subject index Program index Exercise index

In general, we see three advantages of dealing with types:

The notion of type is used to make programs more readable, make them run more efficient, and to detect certain errors before they cause errors in the calculation.

Let us now make a more detailed characteristics of these advantages in the following itemized list.

Readability
- Explicitly typed variables, parameters and function serve as important documentation, which enhances the program understanding.
Efficiency
- Knowledge of the properties of data makes it possible to generate more efficient code
Correctness
- Explicit information about types in a program is a kind of redundancy against which it is possible to check expressions and values
- Programmers usually wish to identify type errors as early as possible in the development process

The correctness quality is often brought into focus. In the next few sections we will therefore discuss type checking issues.

5.2. Type checking
Contents Up Previous Next Slide Subject index Program index Exercise index

Type checking is the processes of identifying errors in a program based on explicitly or implicitly stated type information

Below we will identify three kinds of 'typing', which are related to three different approaches to type checking.

Weak typing
- Type errors can lead to erroneous calculations
Strong typing
- Type errors cannot cause erroneous calculations
- The type check is done at compile time or run time
Static typing
- The types of all expressions are determined before the program is executed
- The type check is typically carried out in an early phase of the compilation
- Comes in two flavors: explicit type decoration and implicit type inference
- Static typing implies strong typing

According to section 1.1 the Scheme Report (R5RS) 'Scheme has latent as opposed to manifest types. Types are associated with values (also called objects) rather than with variables.' In our categorization, Scheme is strongly typed and types are dealt with at run time (on values) as a contrast to compile time (on variables).

It is worth noticing that we classify Scheme as supporting strong typing. Many programmers will probably be surprised by this categorization, because the 'typing' in Scheme is experienced to be relatively 'weak' and 'dynamic'. However, type errors in Scheme do not cause erroneous calculations. Type errors are discovered at a low and basic level. As such we find it justifiable to classify the typing in Scheme as being strong. Notice however, that there is no trace of static type checking in Scheme. Static type checking is the rule in most modern programming languages today, and static type checking is also an absolutely key aspect in functional programming languages such as ML [Harper88] and Haskell [Hudak92].

5.3. Static type checking
Contents Up Previous Next Slide Subject index Program index Exercise index

There are two main kinds of static type checking: explicit type decoration and implicit type inference

For the sake of the discussion we will involve the following example:

Let us study the expression (+ x (string-length y))

Explicit type decoration
- Variables, parameters, and others are explicitly declared of a given type in the source program
- It is checked that y is a string and that x is a number
Implicit type inference
- Variables and parameters are not decorated with type information
- By studying the body of string-length it is concluded that y must be a string and that the type of (string-length y) has to be an integer
- Because + adds numbers, it is concluded that x must be a number

Explicit type decoration is well-known to most computer science students.

If you want to study additional details about implicit type inference you should consult a textbook of ML or Haskell programming.

5.4. An example of type checking
Contents Up Previous Next Slide Subject index Program index Exercise index

We will now discuss type checking relative to the three kinds of 'typing', which we identified in Section 5.2.

Is the expression (+ 1 (if (even? x) 5 "five")) correct with respect to types?

Weak typing
- It is not realized that the expression (+ 1 "five") is illegal.
- We can imagine that it returns the erroneous value 47
Strong typing
- If, for instance, x is 2, the expression (+ 1 (if (even? x) 5 "five")) is OK, and has the value 6
- If x is odd, it is necessary to identify this as a problem which must be reported before an evaluation of the expression is attempted
Static typing
- (+ 1 (if (even x) 5 "five")) fails to pass the type check, because the type of the expression cannot be statically determined
- Static type checking is rather conservative

When we use the word conservative for static type checking, we refer to the caution of the type checker. Independent of branching, and in 'worst cases scenarios', the type constraints should be guaranteed to hold.

5.5. Types in functional programming languages
Contents Up Previous Next Slide Subject index Program index Exercise index

Scheme is not representative for the handling of types in most contemporary functional programming languages

ML and Haskell
- Uses static typing ala implicit type inference
- Some meaningful programs cannot make their way through the type checker
- There will be no type related surprises at run time
Scheme
- Is strongly typed with late reporting of errors
- Type errors in branches of the program, which are never executed, do not prevent program execution
- There may be corners of the program which eventually causes type problems

Due to the handling of types, Scheme and Lisp are elastic and flexible compared with ML, Haskell, and other similar language which are quite stiff and rigid.

5.6. References
[Hudak92] Paul Hudak and Joseph H. Fasel, "A Gentle Introduction to Haskell", ACM Sigplan Notices, Vol. 27, No. 5, May 1992.
[Harper88] Robert Harper, Robin Milner and Mads Tofte, "The Definition of Standard ML, Version 2", Tech Report no. ECS-LFCS-88-62, University of Edinburgh, August 1988.

Generated: Tuesday July 2, 2013, 09:14:49

[Hudak92]	Paul Hudak and Joseph H. Fasel, "A Gentle Introduction to Haskell", ACM Sigplan Notices, Vol. 27, No. 5, May 1992.
[Harper88]	Robert Harper, Robin Milner and Mads Tofte, "The Definition of Standard ML, Version 2", Tech Report no. ECS-LFCS-88-62, University of Edinburgh, August 1988.