[Haskell-cafe] Polymorphic algebraic type constructors

[MR K P SCHUPKE]

Adrian Hey wrote:

I think all occurences of [] have type forall a. [a]
The case expression..
         case a of
                 (a':as) -> <expr1>
                 []      -> <expr2>

Should be typed as if written..
         case a of
                 (a':as) -> let a=(a':as) in <expr1>
                 []      -> let a=[]      in <expr2>

----------------------------------------------------

Well, we will have to agree to disagree, I find the
current system makes perfect sense, and is easy to
reason with. If I want a let binding I can write one.

The difference is really this:

case a of
	(a:as) -> <expr1>
	e -> e

In this case e represent 'the same []' as on the left hand
side.

in the let binding this is a new and fresh '[]'... 

When I pattern match a variable in a case extression
I really expect it to get the type of the case...

There are circunstances when I go on to use e, and if
it is not grounded by the case expression I will get
hit by the monomorphoism restriction, and have to
add non haskell98 type annotation to ground 'e'...

for example If I pass e to a polymorphic function, it
won't know what type e has...

case a of
	(a':as) -> let a=(a':as) in <expr1>
	[]      -> let a=[]      in (polyfn a)

where polyfn a has a type like

polyfna :: Ord a -> [a] -> String

Now the above won't work and you will have to do:

	[]      -> let a=[]      in (polyfn (a :: [SomeListType]))

and of course if you are using generics then how can
polyfn get the original type of 'a' in the case expression...

for example:

	polyfn :: Typable a -> [a] -> ShowS
	polyfn a = shows (typeOf a)

then:

	case a of
	(a:as) -> <expr1>
	e -> polyfn e

is correct, but:

	case a of
	(a':as) -> let a=(a':as) in <expr1>
	[]      -> let a=[]      in (polyfn a)

does what?

	Keean.