Re: [Haskell-cafe] Polymorphic algebraic type constructors
(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. You either mean: f :: (a->a) -> Either String a -> Either String a Or you mean f :: (a->b) -> Either String a -> Either String b actually the second form a and b can be the same but they cannot be unified inside the closure. One way of doing this is to group all the string types on one side: so instead of: data A a = A a | B String | C String | D String you do: data A a = A a | B Strings data Strings = S1 String | S2 String | S3 String you can then write: f :: (a->b) -> A a -> A b f g (A a) = (A $ g a) f g (B a) = (B a) and use (S1 . B), (S2 . B), (S3 . B) to access each string. Keean.
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
participants (2)
-
Adrian Hey -
MR K P SCHUPKE