Hello,
Maybe a more slightly more honest type for "decomp" would be:) :
decomp :: Injective f => f a :=: f b -> a :=: b
Cheers,
Bruno
On Wed, 16 Jan 2008, Derek Elkins wrote:
On Wed, 2008-01-16 at 09:18 +0000, J.N. Oliveira wrote:
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.
Just like data constructors, type constructors are injective. f a
doesn't simplify and so essentially you have structural equality of the
type terms thus f a = f b is -equivalent- to a = b. Obviously type
functions change this, just like normal value functions do at the value
level.
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
