Injective type families?

[Roman Leshchinskiy]

On 14/02/2011, at 21:28, Conal Elliott wrote:

> Is there a way to declare a type family to be injective?
> 
> I have
> 
> > data Z
> > data S n
> 
> > type family n :+: m
> > type instance Z   :+: m = m
> > type instance S n :+: m = S (n :+: m)

You could prove it :-)

class Nat n where
  induct :: p Z -> (forall m. p m -> p (S m)) -> p n

instance Nat Z where
  induct z _ = z

instance Nat n => Nat (S n) where
  induct z s = s (induct z s)

data P n1 n2 m where
  P :: (forall a. (m :+: n1) ~ (m :+: n2) => (n1 ~ n2 => a) -> a) -> P n1 n2 m

injective :: forall m n1 n2 a. (Nat m, (m :+: n1) ~ (m :+: n2)) => n1 -> n2 -> m -> (n1 ~ n2 => a) -> a
injective _ _ _ x = case induct (P (\x -> x)) (\(P f) -> P f) :: P n1 n2 m of
                      P f -> f x

This is a bit inefficient, of course, because it involves recursion. With a little bit of safe cheating, it is possible to get by without recursion, basically by making induction an axiom rather than "proving" it.

It would be nicer if the compiler could prove it for us, of course.

Roman