More suitable data structure needed

[John Hughes]

On Wed, 21 Aug 2002, Hal Daume III wrote:

> I snipped most of the aside :).  The main problem with structures without
> names is that it would be very difficult for the typechecker to do its job
> (as I understand it, though certainly typechecking is not my forte).  But
> basically, this amounts to the same thing as trying to say:
>
>     type MyList a = (a, MyList a)
>
> First of all, there's no base case (like "[]" in lists or "Nothing" in
> Maybe, etc.).  So we can sort of fix that by saying:
>
>     type MyList a = (a, Maybe (MyList a))
>
> So the list ends when we get to 'Nothing'.  The problem here is on the
> type inference.  Suppose I write:
>
>     ('a', Just ('b', Just ('c', Nothing)))
>
> Now, for a human point of view, this doesn't pose a problem.  This is of
> type MyList Char.  The problem is that haskell uses types eagerly, so when
> it gets down to 'Nothing', it will say, "okay, what type does this
> have?  ah, it must by 'MyList a'.  What does MyList a mean?  Oh, it means
> '(a, Maybe (MyList a))'.  Let me substitute."  It will then continue ad
> infinitum.  Of course, it's not that stupid and will simply reject the
> type at the very begginning for having a loop.
>
> Someone else will have to say a word or two about what would happen if
> type inference were done lazily, though presumably "bad things" would
> happen (and it's not even clear this would help).

It can be done, and it isn't even particularly difficult. The trick is
just to make the type-checker use graph rather than term unification,
which means that when two (possibly recursive) types are compared, the
type-checker remembers which pairs of types it is currently comparing, and
if it later encounters the same pair of types again (at a recursive
occurrence), simply assumes they match --- any failure would be caught by
the previous (enclosing) comparison. It's the standard way a graph
traversal avoids falling into a loop on cyclic graphs.

But indeed, "bad things" happen. The bad things are that type errors would
be reported later in some cases. The effect of allowing recursive types is
that, every time hugs reports "unification would give infinite type" (or
corresponding messages from other compilers), the definition concerned
*would actually be type correct*. In a few cases (such as the one that
kicked this discussion off), that is actually what we want. The trouble is
that, in many other cases, the program is actually wrong! For example,
look at

	f x y = if x==0 then y else f (x-1)

Clearly a type error, right? (I left out the second parameter in the
recursive call). But the error message from hugs is

ERROR Junk.hs:1 - Type error in function binding
*** Term           : f
*** Type           : a -> b -> b
*** Does not match : a -> b
*** Because        : unification would give infinite type

which means that if recursive types were allowed, then this definition
would be type correct! Its type would be

       	f :: Num a => a -> b where b = b -> b

(We can see that if b = b -> b, then the two types in the error message
above actually do match).

The trouble is that you can't actually call this function in any useful
way. If you try, say with the call

	f 10 15

then you'll get an error message. In this case, Hugs would probably
say

ERROR - Illegal Haskell 98 class constraint in inferred type
*** Expression : f 10 15
*** Type       : Num b => b where b = b -> b

Now, when you forget a parameter, one can perhaps question just how
friendly a way today's error message is of telling you so. But making type
definitions containing such errors type correct until they are used is
scary!

And that's the reason recursive types have never been added to Haskell.
The consequences for type error reporting just seem to be too horrible to
contemplate.

I should add that recursive types ARE implemented in OCAML --- but after
experiencing just these kinds of problems, recursion was restricted to
OCAML object types, where it clearly doesn't cause much problem.

John Hughes