More suitable data structure needed

[Dr Mark H Phillips]

On Fri, 2002-08-23 at 19:22, John Hughes wrote:

> 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!

I'm a bit new to functional programming ideas, so please excuse me
if I sound ill-informed (because I probably am:-), but...

Am I right in thinking the trade-off is between
* the expressability power of the type system; and
* the ability pick up certain forms of human error?

Why not allow infinite types thereby gaining extra power which
may sometimes be useful, but introduce the option (in hugs or
ghc) of providing a warning every time "unification would give infinite
type"?  This would allow us to "have our cake and eat it too"!  (But
probably there's a catch:-)

Cheers,

Mark.

> 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
> 
> 
> 
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell