[Haskell] Should the following program be accepted by ghc?
J.N. Oliveira
jno at di.uminho.pt
Wed Jan 16 04:18:38 EST 2008
On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:
> Hello,
>
> 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.
Cheers
jno
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3082 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell/attachments/20080116/530dccc8/smime-0001.bin
More information about the Haskell
mailing list