[Haskell] Should the following program be accepted by ghc?
jno at di.uminho.pt
Wed Jan 16 04:18:38 EST 2008
On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:
> I have been playing with ghc6.8.1 and type families and the
> following program is accepted without any type-checking error:
>> data a :=: b where
>> Eq :: a :=: a
>> decomp :: f a :=: f b -> a :=: b
>> decomp Eq = Eq
> However, I find this odd because if you interpret "f" as a function
> and ":=:" as equality, then this is saying that
> if f a = f b then a = b
This is saying that f is injective. So perhaps the standard
interpretation leads implicitly to this class of functions.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 3082 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell/attachments/20080116/530dccc8/smime-0001.bin
More information about the Haskell