Re: [Haskell] Should the following program be accepted by ghc?

Wed, 16 Jan 2008 01:19:10 -0800 


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

Attachment: smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to