[Haskell-cafe] type inference and named fields

[Lennart Augustsson]

Jonathan Cast wrote:
> No  type theory  (that I  know  of) goes  beyond System  F in  accepting
> anything  like foo.   So, given  the current  state of  the art,  foo is
> unconditionally ill-typed.  That could change if someone comes up with a
> /consistent/ type theory  that accepts foo, but foo  is ill-typed at the
> moment.

As you say, we use types in programming languages because they help us,
not because we want to implement type systems.  So if a program makes
sense when you ignore the types, it would be nice if the type system
accepts it.  My little program makes sense, but is not accepted by
Haskell.  Nor am I proposing that it should be accepted by Haskell.
I was only giving an example of something that makes sense, but isn't
allowed.

There are, of course, type systems where my program works fine.
O'Haskell is an example of a language with such a type system.
In O'Haskell the Either type is defined like this:

   data Left a = Left a
   data Right a = Right a
   data Either a b > Left a, Right b

which means that Either is really a union of the Left and Right types.
Now my program type checks. :)

   foo :: Either a b -> Either () b
   foo (Left _) = Left ()
   foo x@(Right _) = x

And it has type checked in various type systems for quite a while, but
not in System F.  But System F is not the end all of type systems.

	-- Lennart