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