[Haskell-cafe] Polymorphic algebraic type constructors

[Adrian Hey]

On Tuesday 22 Jun 2004 1:50 pm, MR K P SCHUPKE wrote:
> >(I still think it's a bug though:-)
>
> It is definitely not a bug... you cannot assert that the types:
>
> Either String a
> Either String b
>
> are both equal ant not equal at the same time.

I wasn't.

> You either mean:
>
> f :: (a->a) -> Either String a -> Either String a
>
> Or you mean
>
> f :: (a->b) -> Either String a -> Either String b

My gripe with the current Haskell (and every other statically typed
FPL I've used) treatment of this is that if you view a type as an
abstract description of a set of values then it seems that these
sets are not permitted to intersect. I.E In any given context the
same value can only be a element of one and only one set, even
if the value is partially known as a result of pattern matching.

I don't know if this is the correct interpretation in a type
theoretical sense (I'm not a type theorist), but I would say
that this is the most intuitive interpretation from Joe programmers
perspective, and so should be allowed unless there are persuasive
technical arguments why this is impossible. There might well be, but
I was left quite unconvinced that this is the case last time I mentioned
this, and my opinion hasn't changed since.

It's especially strange I think, because Haskell doesn't seem to apply
the same rules to values which are partially (or completely) known as a
result of pattern matching as it does to values which are partially
(or completely) known as a result of let binding.

for example..

 let e=[] in e:e

is perfectly legal, whereas..

 f :: [Int] -> [Bool]
 f (i:is) = even i : f is
 f e@[]   = e

will give a type error, despite the fact that e's value is known
to be [] in each case.

Regards
--
Adrian Hey