[Haskell-cafe] Polymorphic algebraic type constructors

[Adrian Hey]

On Tuesday 22 Jun 2004 9:09 pm, Duncan Coutts wrote:

> I think the point is that [] (or e in your example) has type
> forall a.[a]
> where as in the original example e was bound to an argument with the
> type [Int], so e could not be used where something of type [Bool] was
> required. On the other hand
> [] :: forall a.[a]
> could be used in either context.

Whilst I understand perfectly well why this inconsistency arises, I don't
agree that this is the point :-) I think the point is this inconsistency
should not arise. I think that function definitions of form..

 f v@<pat> = <expr>

should be type checked as if they had been written..

 f <pat> = let v = <pat> -- assuming <pat> is syntactically correct expr
           in <expr>

Same applies to case expressions to.

Of course one would need to be careful if <pat> contained '_'.

However, cases like this..

 f (i:is) = even i : f is
 f e      = e

are a bit more ambiguous. Although we all know e must be [], that
isn't immediately obvious. So I guess the answer depends on whether
type checking should be done before or after pattern match compilation.

Regards
--
Adrian Hey