[Haskell-cafe] Leibniz equality can be made injective

[oleg at okmij.org]

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.