{-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE Rank2Types, ExistentialQuantification #-} {-# LANGUAGE TypeFamilies #-} -- * Leibniz equality can be made injective module LeibnizInjective where -- * Witness for the Leibniz equality newtype EQU a b = EQU{subst:: forall c. c a -> c b} -- * Leibniz equality is reflexive, symmetric and transitive -- Here is the constructive proof refl :: EQU a a refl = EQU id -- * An Unusual `functor' tran :: EQU a u -> EQU u b -> EQU a b tran au ub = subst ub au -- Why it works? We consider (EQU a u) as (EQU a) u, -- and so instantiate c to be EQU a -- To show symmetry, we have to ``swap'' the arguments -- in EQU a b. We use the following auxiliary ``type function'' newtype FS b a = FS{unFS:: EQU a b} symm :: EQU a b -> EQU b a symm equ = unFS . subst equ . FS \$ refl -- Useful type-level lambdas, so to speak newtype F1 t b a = F1{unF1:: EQU t (a->b)} newtype F2 t a b = F2{unF2:: EQU t (a->b)} eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2) eq_arr a1a2 b1b2 = unF2 . subst b1b2 . F2 . unF1 . subst a1a2 . F1 \$ refl -- We now attempt to show the converse of eq_arr -- Injectivity -- The original article used a projection type family Fst -- type family Fst a :: * -- type instance Fst (x->y) = x -- type instance Fst (x,y) = x -- -- etc. -- The following generalization (type family Arg) has been -- suggested by Jeremy Yallop type family Arg a :: * type instance Arg (f a) = a newtype ArgA a b = ArgA{unArgA :: EQU (Arg a) (Arg b)} -- The general injectivity -- f below cannot be a type synonym or a type function! eq_f :: EQU (f a) (f1 b) -> EQU a b eq_f eq = unArgA . subst eq \$ ra where ra :: ArgA (f a) (f a) ra = ArgA refl -- Why is this sound? -- First of all, 'f' in eq_f above cannot be a synonym or a type function type NI a = Bool eq_ni :: EQU (NI Char) (NI Int) eq_ni = refl {- eq_bad = eq_f eq_ni Couldn't match expected type `f a' against inferred type `Bool' Expected type: EQU (f a) (f b) Inferred type: EQU (NI Char) (NI Int) In the first argument of `eq_f', namely `eq_ni' -} -- For that reason, we cannot be arity-generic type family Arg2 a :: * type instance Arg2 (f a b) = a newtype Arg2A a b = Arg2A{unArg2A :: EQU (Arg2 a) (Arg2 b)} eq_f2 :: EQU (f a1 b1) (f1 a2 b2) -> EQU a1 a2 eq_f2 eq = unArg2A . subst eq \$ ra where ra :: Arg2A (f a1 b1) (f a1 b1) ra = Arg2A refl -- We now accomplish our task: `inverting' eq_arr eq_arr2 :: EQU (a1->b1) (a2->b2) -> EQU b1 b2 eq_arr2 = eq_f eq_arr1 :: EQU (a1->b1) (a2->b2) -> EQU a1 a2 eq_arr1 = eq_f2 -- Incidentally, the injectivity patently demonstrates -- that Leibniz equality is stronger than bijection: data Bij a b = Bij (a->b) (b->a) data FF a = FF -- A forgetful functor -- We may define a bijection between FF Int and FF Bool bij_ff :: Bij (FF Int) (FF Bool) bij_ff = Bij (\FF -> FF) (\FF -> FF) -- But we can't derive Leibniz equality witness -- EQU (FF Int) (FF Bool) -- Being inter-convertible in any context is far more -- demanding than being inter-convertible in the empty context. -- Tests -- Using the equality witness to extract values from -- under an existential wrapper data Wrap a = forall b. Wrap (EQU (a-> Bool) (b -> Bool)) (b->Bool) tw1 :: Wrap Int tw1 = Wrap refl (> 4) {- -- The following naive extraction of course does not work: extract1 = case tw1 of Wrap _ f -> f (5::Int) Couldn't match expected type `b' against inferred type `Int' `b' is a rigid type variable bound by the constructor `Wrap' at /home/oleg/langs/Haskell/LeibnizInjective.hs:71:5 In the first argument of `f', namely `(5 :: Int)' -} -- But the extraction using the type equality witness convinces -- the type checker. newtype Id a = Id{unId:: a} test = case tw1 of Wrap eq f -> f (cast_arg eq 5) where cast_arg :: EQU (a -> b1) (c -> b2) -> a -> c cast_arg eq n = unId . subst (eq_arr1 eq) \$ (Id n)