Determine the effect of a function by its type

Question

One of the interesting properties of Haskell's type system (*) is that sometimes you can tell exactly what the function does based only on its type signature (assuming there's no unsafe IO dark magic invloved).

For example, any function with the type signature a -> a must be the identity function, and any function of type (a,b) -> a is equivalent to fst. In some cases you cannot determine the function completely: there is an infinite number of different possible functions of type a -> Int, but all of them are constant - they all ignore the first parameter.

I find this property fascinating, but I suspect it only applies to "trivial" functions such as id and const. Am I correct?

Also, my reasoning here is based only on intuition - for example, in a -> a, we "know nothing" about a (as opposed to constrained functions like Num a => a -> a) so "can't do anything" with it other than to return in unchanged. Is there a formal way to deal with these kind of deductions?

_{* I know Haskell's type system is based on the Hindley–Milner type system, but I'm not familiar with it enough to assume anything about it}

Answer 1

The concept you are referring to is known as parametricity. Universal quantification over types gives parametric polymorphism and a "uniformity" property that is intuitively this notion that "we don't know anything about" a in forall a. a -> a and so "can't do anything" with it other than return it unchanged. What the uniformity property says is that a type f :: [a] -> [a] does not depend on the type of a, or, more precisely, depends uniformly on it: that anything one "does" to the [a] must be "doable" for all choices of a. Wadler uses this to show that mapping the values in the list and then permuting the list is equivalent to permuting first and mapping after.

The formal way to deal with these intuitions is given in, e.g., Philip Wadler's Theorems for Free and involves an isomorphism between types and relations (in fact the category PER of partial equivalence relations (p.e.r.'s)) which shows that this uniformity is a universal property in the category.

One interesting result of parametricity is that you can go "both ways": from a type to theorems about that type, and from a type to inhabitants of that type. Wadler's free theorems are an example of the former and Djinn, a theorem prover (inhabitants of a type are "proofs" of the type's "theorem"), is an example of the latter.