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






More information about the Glasgow-haskell-users mailing list