Equality in haskell

Prelude

I've recently begun an attempt to understand lens. I've found nothing gets you into the code like implementing it yourself and subsequently using it. And there's nothing better that helps with the process like Haskell does.

Equality

Our quest begins in modest surroundings. We have a staff surrounded by an aura of artificial light, kitted out for ergonomic handling and some stuffy robes that just about manage to conceal boxer shorts. As a humble warlock we begin by practicing our type magic before tackling the big bosses.

type Equality s t a b = forall p f. p a (f b) -> p s (f t) is the type of an equality. 

The strange points about it are:

• Equality is usually a relation defined on two variables, we're confronted with four over here.
• At first glance the above does not really seem to constrain the variables to be equal to each other.
• We have two absolutely arbitrary contexts that will allow us to do absolutely nothing with these variables.
• Is it even possible to create any equalities?

Well, we can answer the last one quite easily with type Equality' s t = Equality s t s t

The equality in that case is the identity function. This function says, for absolutely any context 'p' and 'f', given a p a (f b) we can get the same back. 

Thus an obvious equality exists when the type variables are the same, so lets create a data type that reifies the idea of identical type variables.

data Identical s t a b where

Identical :: Identical a b a b

The ONLY inhabitant of this type has the type

Thus an inhabitant of Identical s t a b must mean that s is equal to a (represented by the type constructor ~ for the constraint kind) and b is equal to t.

The existence of an inhabitant of this type is thus a 'proof of equality' between s and a, b and t. 

In order to fit this into our general model of equality we make the observation that 

x ~ Truth -> x

Identical s t a b ~ Truth -> Identical s t a b

Identical s t a b ~ Identical s t s t -> Identical s t a b

Identical s t a b ~ Identical s (Identity t) s (Identity t) -> Identical s (Identity t) a (Identity b)

Thus our proof is of type

type AnEquality s t a b = Identical a (Identity b) a (Identity b) -> Identical a (Identity b) s (Identity t)

What can we do with our proof? 

Glad you asked..

substEq :: AnEquality s t a b -> ((s ~ a, t ~ b) => r) -> r

This function says that given a proof of equality between s and a, t and b, i.e. (s ~ a, t ~ b) and an r that can only exist when the aforementioned constrains hold, create the r.

This function is thus modus ponens at the type level.

substEq f r = case (f Identical) of

Identical -> r

This function gives us the ability to construct r's under the assumption that  (s ~ a, t ~ b) which allows us to perform substitutions of s and t with a and b respectively and vice versa.

Some examples of these substitutions are mentioned below:

Substitution of a variable in a random context.

mapEq :: AnEquality s t a b -> f s -> f a

mapEq proof fs = substEq proof fs

Equality is symmetric:

fromEq :: AnEquality s t a b -> AnEquality b a t s

fromEq f = substEq f (\Identical :: Identical b (Identity a) b a -> Identical :: Identical b (Identity a) t (Identity s))

Ruminations

Although, we've used AnEquality in our proof they will work with an Equality as Equality is strictly more general. 

To address the questions raised in the beginning

• I'm still not sure why we have to represent an equality between two pairs of type variables.
• It is the function and the contexts that constrains the type variables.

Afterword

Our warlock has pushed 'forward' through the undergrowth into a splendorous wide open clarity. 

He must now dive 'backward' back into it to explore Iso's ;)