[Haskell-cafe] A voyage of undiscovery

[Andrew Coppin]

I've been working hard this week, and I'm stumbled upon something which 
is probably of absolutely no surprise to anybody but me.

Consider the following expression:

  (foo True, foo 'x')

Is this expression well-typed?

Astonishingly, the answer depends on where "foo" is defined. If "foo" is 
a local variable, then the above expression is guaranteed to be 
ill-typed. However, if we have (for example)

  foo :: x -> x

as a top-level function, then the above expression becomes well-typed.

I had never ever noticed this fact before. I'm still trying to bend my 
mind around exactly why it happens. As best as I can tell, top-level 
functions (and value constructors, for that matter) seem to get a "new" 
set of type variables each time they're used, but local variables each 
get a single type variable, so every mention of a local variable must be 
of the exact same type.

Could this be what GHC's weird "forall" syntax is about? Does "forall 
x." mean that "x" gets replaced with a unique type variable each time? 
It's an interesting hypothesis...

Anyway, not that anybody is likely to care, but I've just spent an 
entire week writing a program which can type-check simple Haskell 
expressions. As in, you type in an expression and give types to any free 
variables it involves (including value constructor functions), and it 
tells you the type of the expression and all its subexpressions. (Or 
tells you that it's ill-typed.) It turns out that this is radically less 
trivial than you'd imagine. (The ramblings above being just one of the 
issues I blundered into. Others include the subtleties of writing an 
expression parser, building a pretty-printer with bracketing that works 
correctly, and the fact that expression processing malfunctions horribly 
if you don't make all the variable names unique first...) Other issues 
were mostly related to the difficulty of constantly refactoring code 
because you're not quite sure what you're trying to do or how you're 
trying to do it. (And obscure type checker warnings about GADTs...)

Well there we are. I don't suppose anybody will be overly impressed, but 
I'm glad to have finally got it to work. Now, if it could parse more 
than 10% of Haskell's syntax sugar, it might even be useful for something...