Injective type families?

Roman Leshchinskiy rl at cse.unsw.edu.au
Wed Feb 16 22:53:02 CET 2011

```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

```