> The classic example is that there’s an infinite number of functions with type int -> int. The logic of these functions are extremely varied, and the type does

> The classic example is that there’s an infinite number of functions with type int -> int. The logic of these functions are extremely varied, and the type doesn’t help you at all. Yet there is precisely one function with type 'forall a. a -> a', so the type guarantees it's the identity function. Likewise there are precisely two functions with type 'forall a. a -> a -> a': the type guarantees that it will return one of its two arguments (it's equivalent to branching on a boolean). The same pattern holds for selecting between any number of values (which can be useful if we need our caller to make a choice for us). Type constraints are also useful for proving guarantees about our code; e.g. if we have a function like 'forall a. List(a) -> List(a)' then it could do all sorts of rearranging of the elements; whereas 'forall f a. Poppable(f) => f(a) -> f(a)' can only use functions provided by 'Poppable' (presumably: popping elements off the start). We can still pass around 'List(a)' values, as long as 'List' implements 'Poppable', but (a) we guarantee more about the behaviour of these functions (b) the functions are easier to write (since there are fewer things we can get wrong) and (c) the functions are more generic than using a concrete type like 'List'. Note that constraints provide stronger guarantees than subtypes or interfaces, e.g. in Scala 'Poppable[A] => Poppable[A]'. The latter doesn't force the input and output types to be the same, so returning an empty 'List' will work; whereas the constraint requires we return an 'f(a)' for all possible 'f'; hence we're forced to use the input value (in the same way that 'forall a. a -> a' forces us to return the input). Of course, constraints can always be desugared into dictionary passing (e.g. http://www.haskellforall.com/2012/05/scrap-your-type-classes.html http://www.haskellforall.com/2012/05/scrap-your-type-classes... ); e.g. 'forall f a. (f a -> (a, f a)) -> f a -> f a', where the '(f a -> (a, f a))' argument is some sort of 'pop' function; however, we still benefit from static types to ensure that all of these arguments line up (i.e. the same 'f' and 'a' are used in each occurrence), and we benefit from parametricity giving us 'theorems for free' about the possible behaviour.