We show that type families let us write Leibniz equality witnesses of the injectivity of type constructors. We may use Leibniz equality not only for introduction but also for elimination. The paper on ``Typing Dynamic Typing'' (Baars and Swierstra, ICFP 2002) demonstrated the first implementation and application of Leibniz equality witnesses in Haskell:
newtype EQU a b = EQU{subst:: forall c. c a -> c b}
A term (eq :: EQU a b) witnesses the equality of the types a and b: in any context c, the type a can be substituted with the type b. The context is represented by the type constructor c. The witness gives the constructive prove of substitutability: given a term of the type c a, we can always obtain a term of the type c b. Since we don't know anything about the context c, such a substitution can only happen if the two types are indeed equal. Hence the sole non-bottom witness is
refl :: EQU a a refl = EQU id
testifying that equality is reflexive. Leibniz equality became quite popular since it lets us represent GADTs to a large extent. The power of Leibniz equality comes from the fact that the context c may indeed be anything we want. The following example illustrates that power, by concisely proving that the equality is transitive. The proof of transitivity is very short
tran :: EQU a u -> EQU u b -> EQU a b tran au ub = subst ub au
We treat the type EQU a u as (EQU a) u, that is, as an application of the `type constructor' (EQU a) to the type 'u'. We then use the witness EQU u b to replace the type u with the type b in the context (EQU a), giving us the desired EQU a b. When writing type checkers and type inferencers in Haskell along the lines of typing dynamic typing, we also need to know that two arrow types are equal if and only if their components are equal. In one direction,
eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2)
if the argument and result types of two arrow types are equal, the arrow types themselves are equal. Fortunately, for this, commonly used direction, the proof is easy, after we define suitable type-level combinators F1 and F2 to place the types being equated in the right context:
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
In the type EQU (a1->b1) (a2->b2), the type `constructor' (F1 (a1->b1) b2) represents the context of the type a2, and the type constructor (F2 (a1->b1) a2) is the context of the type b2. Leibniz equality only applies if the context of a type is represented as a type constructor; therefore, we sometimes have to define auxiliary newtypes to put the contexts in the required form. In the reverse direction, we have to prove that if two arrow types are equal, their components (e.g., the argument types) are equal as well. The proof will witness the injectivity of the arrow type constructor. It is thought that injectivity cannot be proven with Leibniz equality at all. For example, the paper ``Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell'' by Chen, Zhu and Xi, PADL'04, needed the reverse, elimination direction and found it impossible to obtain with Leibniz equality witnesses. We demonstrate that type families help. Type families let us define ``subtractive contexts'', so that we can view a type 'a' as the type (a->b) placed into the context that removes (->b). Again we use an auxiliary newtype to make the subtractive context appear as a type constructor.
type family Fst a :: * type instance Fst (x->y) = x type instance Fst (x,y) = x -- etc.
newtype FstA a b = FstA{unFstA :: EQU (Fst a) (Fst b)}
eq_arr1 :: EQU (a1->b1) (a2->b2) -> EQU a1 a2 eq_arr1 eq = unFstA . subst eq $ ra where ra :: FstA (a1->b1) (a1->b1) ra = FstA refl
The complete code is available at http://okmij.org/ftp/Haskell/LeibnizInjective.hs The code includes a simple test of the injectivity.