[Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]

[Philippa Cowderoy]

Warning for Andrew: this post explains a new-to-you typed lambda calculus 
and a significant part of the innards of Hindley-Milner typing in order to 
answer your questions. Expect to bang your head a little!

On Tue, 27 May 2008, Andrew Coppin wrote:

> - A function starts out with a polymorphic type, such as 'x -> x'.
> 

Which is the same as "forall x. x -> x".

> - Each time the function is called, all the type variables have to be locked
> down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or
> something.
> 

Yep, in fact in the explicitly-typed calculus commonly used as a model for 
rank-n polymorphism (System F) there are explicit type lambdas and type 
applications that do exactly this. Using /\ for a type lambda and [term 
type] for type applications, id might be written thus:

id = /\t.(\x::t->x)

and called thus:

[id Int] 1

> - By the above, any function passed to a high-order function has to have all
> its type variables locked down, yielding a completely monomorphic function.
> 

Yep.

> - The "forall" hack somehow convinces the type checker to not lock down some
> of the type variables. In this way, the type variables relating to a function
> can remain unlocked until we reach each of the call sites. This allows the
> variables to be locked to different types at each site [exactly as they would
> be if the function were top-level rather than an argument].
> 

Not a hack. If there is a hack, it's in /not/ including a forall for 
rank-1 types. Foralls correspond to type lambdas in the same way that ->s 
correspond to ordinary lambdas.

> - Why are top-level variables and function arguments treated differently by
> the type system?

The big difference is between lambdas and binding groups (as in let, 
top-level etc). With the binding group, any constraints on a value's type 
will be found within its scope - so the type can be 'generalised' there, 
putting a forall around it. The same isn't true of lambdas, and so their 
parameters can only be polymorphic given an appropriate type annotation. 
For extra confusion, type variables are themselves monomorphic[1].

> - Why do I have to manually tell the type checker something that should be
> self-evident?

It isn't - the general case is in fact undecidable.

> - Why do all type variables need to be locked down at each call site in the
> first place?

Find an alternative model for parametric polymorphism that works!

Note that 'not locking down' is equivalent to locking down to parameters 
you took from elsewhere. As such, if you stick to rank-1 types you never 
actually notice the difference - whereas it makes the type system an awful 
lot easier to understand.

> - Why is this virtually never a problem in real Haskell programs?

I wouldn't go so far as to say virtually never, I've run into it a fair 
few times - but normally until you're trying to do pretty generalised 
stuff it's just not necessary.

> - Is there ever a situation where the unhacked type system behaviour is
> actually desirably?

There are plenty of situations where a rank-1 type is the correct type. If 
you give id a rank-2 type, it's more specific - just as if you typed it 
Int->Int.

> - Why can't the type system automatically detect where polymorphism is
> required?

Because there's often more than one possible type for a term, without a 
'most general' type.

> - Does the existence of these anomolies indicate that Haskell's entire type
> system is fundamentally flawed and needs to be radically altered - or
> completely redesigned?
> 

About as much as the undecidability of the halting problem and the 
incompleteness theory suggest our understanding of computation and logic 
is fundamentally flawed - which is to say, not at all.

> The key problem seems to be that the GHC manual assumes that anybody reading
> it will know what "universal quantification" actually means. Unfortunately,
> neither I nor any other human being I'm aware of has the slightest clue what
> that means. 

Guess nobody on this list's human, huh?

It's really not the GHC manual's job to teach you the language extensions 
from scratch any more than it should teach Haskell 98 from scratch. I 
guess the real question is where the relevant community documentation is, 
something I have to admit to not having needed to check.

>  existential quantification = "this is true for SOMETHING"
>  universal quantification = "this is true for EVERYTHING"
> 

The type "forall x. x -> x" is "for all types x, x -> x". As in, "for all 
types x, (\y -> y) :: x -> x".

[1] Actually this is no longer quite true since GHC now supports 
impredicative polymorphism in which type variables can be instantiated 
with polymorphic types. But please ignore that for now?

-- 
flippa at flippac.org

'In Ankh-Morpork even the shit have a street to itself...
 Truly this is a land of opportunity.' - Detritus, Men at Arms