# Union Type in Idris (Part 4)

Posted on August 2, 2016 by Nicolas Biri

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.