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
