1. Introduction to types

Variable Types

Types are divisions of different classes of values with each type associated with a set of operations, they ensure programs behave in a pre-determined and precise way, and they may be explicitly given by the programmer or inferred automatically by the type system.

Link to original

Checking Types

Typing may be checked:

• before execution: static typing every valid expression must have a type expressions that cannot be ‘typed’ are considered an error a program that passes type controls is not guaranteed to be correct but is free of type errors at runtime
• during execution: dynamic typing

Types in Haskell

Haskell has the following set of predefined types:

• basic data types: booleans (Bool), characters (Char), numbers (Int, Float, Double)
• constructed types: tuples, lists, strings [Integer] is a type of lists of arbitrary precision integers (Int, Bool) is a (binary) tuple of an integer and boolean
• function types: Char -> Bool or (Int -> Int) -> Int

Polymorphism

Type systems can be:

• monomorphic: every expression has at most one type
• polymorphic: expressions may have more than one type

Example: functional composition

(.) :: (b -> c) -> (a -> b) -> (a -> c)

Where $a$, $b$, and $c$ are type variables.

Formally, the language of polymorphic types is defined as a set of terms built out of type variables ($a,b,c,\dots$), and type constructors which are either atomic (Int, Float, …) or take arguments (e.g. $T_1\to T_2,[T]$). $\begin{array}{rl}V& ::=a,b,c,\dots \\ C& ::=\text{Int},\text{Bool},\text{Char},\to ,[],(),\dots \\ T& ::=V|C(T_1,T_2,\dots ,T_n)\end{array}$

Type variables exist in languages such as C++ to specify polymorphic types

template<typename A, typename B>
pair<B,A> flip_pair(const pair<A,B> &p) {
	return pair<B,A>(p.second, p.first);
}

Polymorphism in Haskell

Type variables can be instantiated to different types.

From square :: Integer -> Integer and sqrt :: Integer -> Float, we can compose them together as sqrt . square to create a function type Integer -> Float.

The error function is also polymorphic, i.e. error :: String -> a.

Overloading

Overloading is a related notion (also referred to as ad-hoc polymorphism) where several functions, with different types, share the same name.

For example, in Haskell we may want to specify a general operation such as addition for both integers or reals. However a polymorphic type like (+) :: a -> a -> a is too general because it would allow addition with any type.

We can solve this by:

• Providing different symbols / names for operations on specific types.
• Enrich language of types (unions): `(+) :: (Integer -> Integer) ∧ (Float -> Float)
• Define the notion of a type class Haskell allows you to define one within a polymorphic type:

  (+) :: Num a => a -> a -> a

Type Inference

Type Inference

Most modern functional languages are able to infer types for the programmer using the operations used in the expression and based on the atomic constituents.

Link to original

Example of type inference with Haskell

Consider definition of square x = x * x

• square is a function, most general type is a -> b
• Using square’s definition, x :: a and x * x :: b.
• (*) :: Int -> Int -> Int is primitive
• If x :: Int then x * x :: Int, hence both a and b must be Int.
• Therefore, square :: Int -> Int.