[Haskell-cafe] Trouble with types

[wren ng thornton]

Vladimir Reshetnikov wrote:
> Hi Daniel,
> 
> Could you please explain what does mean 'monomorphic' in this context?
> I thought that all type variables in Haskell are implicitly
> universally quantified, so (a -> a) is the same type as (forall a. a
> -> a)

At the top level (i.e. definition level), yes. However, each use site 
this polymorphism may be restricted down (in particular, to the point of 
monomorphism).

In a syntax more like Core, the definition of the identity function is,

     id :: forall a. a -> a
     id @a (x :: a) = x

Where the @ is syntax for reifying types or for capital-lambda 
application (whichever interpretation you prefer). In this syntax it's 
clear to see that |id| (of type forall a. a -> a) is quite different 
than any particular |id @a| (of type a->a for the particular @a).


So in your example, there's a big difference between these definitions,

     (f,g) = (id,id)

     (f', g') @a = (id @a, id @a)

The latter one is polymorphic, but it has interesting type sharing going 
on which precludes giving universally quantified types to f' and g' (the 
universality is for the pair (f',g') and so the types of f' and g' must 
covary). Whereas the former has both fields of the tuple being 
polymorphic (independently).

Both interpretations of the original code are legitimate in theory, but 
the former is much easier to work with and reason about. It also allows 
for tupling definitions as a way of defining local name scope blocks, 
without side effects on types.

-- 
Live well,
~wren