Union Type in Idris (Part 4)

Go back to the first part.

A glimpe of equality

Idris handles equality with a typeclass, just like Haskell. Whilst equality must be define specifically for each sum type, we can define the equality in a generic manner for union types. The idea is to define the equality iteratively on the list of types of the union.

Equality for Union x::xs

Let’s start with the recursive case, do we really need to elaborate?

(Eq ty, Eq (Union xs)) => Eq (Union (ty::xs)) where
  (==) (MemberHere x) (MemberHere y) = x == y
  (==) (MemberHere x) (MemberThere y) = False
  (==) (MemberThere x) (MemberHere y) = False
  (==) (MemberThere x) (MemberThere y) = x == y

We need equality for the previous union (induction) nd for the newly added type. Then, two terms are equal if they point to the same type and have the same value.

The base case

Things here are a little trickier. We nned an instance of Eq (Union []). Let’s look back at the Union definition:

data Union : List Type -> Type where
  MemberHere : (x: ty) -> Union (ty::xs)
  MemberThere : (x: Union xs) -> Union (ty::xs)

Do you see the potential issue? None of them allow us to build a Union []. It’s impossible to build an element of Union []? Just explain it to Idris:

Eq (Union []) where
  (==) (MemberHere _) _ impossible
  (/=) (MemberThere _) _ impossible

Profit:

> the (Union [Nat, String]) "foo" = the (Union [Nat, String]) "foo"
True : Boolean
> the (Union [Nat, String]) "foo" = the (Union [Nat, String]) "bar"
False : Boolean
> the (Union [Nat, String]) "foo" = the (Union [Nat, String]) 42
False : Boolean

Uninhabited types

There is an alternative to the impossible solution. We can claim that a type is uninhabited thanks to a typeclass:

Uninhabited (Union []) where
    uninhabited (MemberHere _) impossible
    uninhabited (MemberThere _) impossible

Uninhabited comes with an absurd funciton of type Uninhabited e => e -> a absurd can be read as: if we have an instance of an uninhabited type, we can build anything from it.

Thanks to Uninhabited, our instance of Eq can be written:

Eq (Union []) where
  (==) x _ = absurd x

Unions and synonyms

If our unions are well defined, a union of a unique type should be isomorphic to this type. A union of two types should be isomorphic to Either. Let’s transform these assumptions into proofs.

Morphisms

The morphisms can be implemented as instances of the Cast typeclass and are straightforward as soon as we know how to deal with uninhabited types:

Cast (Union [ty]) ty where
  cast (MemberHere x) = x
  cast (MemberThere x) = absurd x

Cast l (Union [l]) where
  cast x = (MemberHere x)

Cast (Union [l, r]) (Either l r) where
  cast (MemberHere x) = Left x
  cast (MemberThere (MemberHere x)) = Right x
  cast (MemberThere (MemberThere x)) = absurd x

Cast (Either l r) (Union [l, r]) where
  cast (Left x) = (MemberHere x)
  cast (Right x) = (MemberThere (MemberHere x))

Put an iso in our morphisms

Idris has a Iso type, that is use to prove that two types are isomorphic. Here is its definition:

data Iso : Type -> Type -> Type
  MkIso : (to : a -> b)
        -> (from : b -> a)
        -> (toFrom : (y : b) -> to (from y) = y)
        -> (fromTo : (x : a) -> from (to x) = x)
        -> Iso a b

to and from are the two morphisms used to build the isomorphism. toFrom and fromTo are proofs. They are populated if and only if for (to . from) and (from . to) behave like the id function.

Thus, being able to build an instance of Iso a b is a proof that a and b are isomorphic. Let’s buils these instances for Union:

oneTypeUnion : Iso (Union [ty]) ty
oneTypeUnion = MkIso cast cast toFrom fromTo
  where
    toFrom _ = Refl
    fromTo (MemberHere _) = Refl
    fromTo (MemberThere x) = absurd x

And:

eitherUnion : Iso (Union [l, r]) (Either l r)
eitherUnion = MkIso cast cast toFrom fromTo
  where
    toFrom (Left _) = Refl
    toFrom (Right _) = Refl
    fromTo (MemberHere _) = Refl
    fromTo (MemberThere (MemberHere _)) = Refl
    fromTo (MemberThere (MemberThere x)) = absurd x

Refl is a member of the type x = x. Being able to compile this code build a formal proof of the existence of the isomorphisms.

Part 4 is over

In the next part, we’ll discuss union type testing. And, by the way, the code is on github.