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.
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
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
> 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
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.
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.
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
from are the two morphisms used to build the isomorphism.
fromTo are proofs. They are populated if and only if for (
to . from) and (
from . to) behave like the
Thus, being able to build an instance of
Iso a b is a proof that
b are isomorphic. Let’s buils these instances for
oneTypeUnion : Iso (Union [ty]) ty oneTypeUnion = MkIso cast cast toFrom fromTo where toFrom _ = Refl fromTo (MemberHere _) = Refl fromTo (MemberThere x) = absurd x
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.