Union Type in Idris (Part 3)

Go back to the first part.

Some are better than others, Union is better than sum

At this point, we have a slightly less complex syntax than sum types (with some drawbacks, but I will detail them in another part), but did we have other benefits?

Well, yes.

Today, we are going to inverstigate how flexible union types are. More precisely, I will detail union type restrictions and generalisation.

Shrink my union

Let suppose that we have a variable x of type Union [Nat, String, List String] and the following repl session:

> the (Maybe Nat) x
Nothing : Maybe Nat

We know that x does not contain a Nat. Thus, x contains either a String or a List String. Well, we can explicitly express it with union types.

Let’s compute the type of this reasoning. Given an union instance, we can either get a value of a type in this uion or we can restrict the union. Quite clear and easy to write:

retract : Union xs -> {auto p: Elem ty xs}
                   -> Either (Union (dropElem xs p)) ty

The result type may require some explanations. The presence of Either and the right case (ty) is clear. The left case (dropElem xs p) is straightforward if we look at the dropElem documentation: it removes the element pointed by p from the list.

The implementation is almost as easy to write as the type:

retract : Union xs -> {auto p: Elem ty xs}
                  -> Either (Union (dropElem xs p)) ty
retract (MemberHere x) {p = Here} = Right x
retract (MemberHere x) {p = (There _)} =
  Left (MemberHere x)
retract (MemberThere x) {p = Here} =
  Left x
retract (MemberThere x) {p = (There later)} =
  either (Left . MemberThere)
         Right
         $ retract x {p = later}

The 3 first cases are trivial, they can almost be completed automatically by Idris (I should talk about this really cool feature in a next post). The last case is a bit more complex. The idea is to lift the result of retract to the next step: on a right, propagate the found value, on a left, just buried it one step further.

It’s time to see retract in action:

> :let x = the (Union [Nat, String, List String]) $ member "foo"
> the (Either _ Nat) $ retract x
Left (MemberHere "foo") : Either (Union [String, List String]) Nat
> the (Either _ String) $ retract x
Right "foo" : Either (Union [Nat, List String]) String

Enlarge my union!

Can we do the opposite of retract? If I have a member of Union [Nat, List String], can we claim that we have a member of a broader union?

Yes, we can but it is a bit more complex than the retract case. The main reason is that we have an infinity of target types for the result union.

Identifying the broader unions

The objective is to define a data type that contain a proof that an union is broader than another one. Or, by transitivity, that each element of a list of types is contained in another list. This is as simple as it sounds. I mean, really, if its sounds complicated to you, it will be complicated to read, if it sounds simple, it will be simple to read:

data Sub : List a -> List a -> Type where
  SubZ : Sub [] ys
  SubK : Sub xs ys ->  Elem ty ys -> Sub (ty::xs) ys

To build a Sub type, we must be able proof that each element of the first list are in the second one.

Trying to generalize union

Now that we have a definition of Sub, we can type our generalize function more easily:

generalize : (u: Union xs) -> {auto s: Sub xs ys}
                           -> Union ys

Given an union, if we have a proof that the list of type in the union is a subset of the list of type in the resulting union, we can generalize the union. Yes, it’s that easy.

Things are getting more complex when we want to implement generalize. Let’s start with a naive implementation and see how it goes:

generalize : (u: Union xs) -> {auto s: Sub xs ys}
                           -> Union ys
generalize (MemberHere x) = member x
generalize (MemberThere x) {s = (SubK y z)} =
  generalize x {s=y}

If we have at MemberHere, x is the value of the union, and thus, must be put in the result union, and we use previously defined member to do so. If we haven’t find the value yet, we just restart one step further.

This version reallly seemed ok to me. Unfortunately, it didn’t match the compiler expactations:

When checking right hand side of generalize with expected type
        Union ys

When checking argument p to function Data.UnionType.member:
        Can't find a value of type
                Elem ty ys

Almost there, the sole issue is that Idris wasn’t able to compute the new location of the value. Fortunately, this location is carried along by Sub and can be easily added:

generalize : (u: Union xs) -> {auto s: Sub xs ys}
                           -> Union ys
generalize (MemberHere x) {s = (SubK _ z)} =
  member x {p = z}
generalize (MemberThere x) {s = (SubK y _)} =
  generalize x {s=y}

And here we go:

> :let x = the (Union [Nat, String]) $ member 2
> the (Union [String, Nat, List String]) $ generalize x
MemberThere (MemberHere 2) : Union [String, Nat, List String]

Part 3 is over

That’s all for today.