[Haskell-cafe] A voyage of undiscovery
andrewcoppin at btinternet.com
Thu Jul 16 14:34:18 EDT 2009
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...
More information about the Haskell-Cafe