Union Type in Idris (Part 1)

TL;DR: This article discusses the interest of union types and presents an implementation of this concept in Idris.

An introduction to sum and union types

If you are familiar with language like Haskell or Scala, you may know what a sum type is. Consider the following example in Haskell:

data Whisky = Whisky {age :: Nat, alcohol :: Float}
data Beer = Beer {alcohol :: Float}

data Alcohol = AlcoholWhisky Whisky
             | AlcoholBeer Beer

myAlcohol :: Alcohol
myAlcohol = AlcoholWhisky (Whisky 12 40)

In this short example, Alcohol is a sum type. It’s called like this because the number of inhabitants of this type is the sum of the inhabitants of the type Whisky and of those of the type Beer.

I always thought that the need of the Alcohol constructors (AlcoholWhisky and AlcoholBeer) is a little clumpsy in such types. It’s getting worse when we stack sums:

data Water = Water {calcium :: Float}
data OrangeJuice = Water {sugar :: Float}

data NoAlcohol = NoAlcoholWater Water
               | NoAlcoholOrangeJuice OrangeJuice

data Beverage = BeverageAlcohol Alcohol
              | BeverageNoAlcohol NoAlcohol

myBeverage :: Beverage
myBeverage = BeverageAlcohol myAlcohol

It would be easier if we can claim that a type t is a union of several types and provides any of these types vaule as a value of type t.

This idea is not new, it’s for example investigated in the open-union package. Thanks to this package, we can replace the first example with something like:

type Alcohol = Union '[Whisky, Beer]


myAlcohol :: Alcohol
myAlcohol = liftUnion (Whisky 12 40)

open-union is a great solution in Haskell. However, it relies on Data.Dynamic which means that we need to carry over the representation of the type.

Defining union types in Idris

Idris is a purely functional programming language with dependent-type designed by Edwin Brady. I assume here a basic knowledge of Idris and of dependent types.

Declaring union types

Suppose that you can promote the values as types, how would it helps to build an union type? This question was the one that started the journey.

Here was the idea: we can define a type as a list of type. From there, it suffices to find a way to “point” the valid type in our union and we obtain an union for free. Here is the implementation:

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

So, Union is a type that is parametrized by a list of types. For example, with this data declaration, Union [Char, String] is a valid type.

To build members of Union we have two constructors. MemberHere is the easiest. Given a value of type ty, we can build an instance of any Union type such that the list of its composed types starts with ty, whatever are the other types of the union. MemberThere provides a way to prepend other types in our Union. Let’s see these types in action:

x : Union [String, Nat, List String]
x = MemberHere "Ahoy!"

y : Union [String, Nat, List String]
x = MemberThere (MemberHere 3)

With this basic definitions, we have in hands all we need to create union types. Altough, the instances are really painful to write, even more than with classic sum types.

We can do way better with a small helper:

member : ty -> {auto e: Elem ty ts} -> Union ts
member x {e = Here} = MemberHere x
member x {e = There later} =
  MemberThere (member x {e = later})

This short function takes advantages of Idris auto implicit arguments, which automatically computes argument at compile times, depending on the executino context. The idea is that, given a type ty, such that ty is in the union, we can compute the location of this type in the union and provide an Elem. This Elem is then used to compute the Union boilerplate. An we obtain:

x : Union [String, Nat, List String]
x = member "Ahoy!"

y : Union [String, Nat, List String]
x = member 3

Note that as complex as the union will be, the instanciation will always straightforward.

Extracting union type

Ok, so union type are easy to declare and to instanciate. We also need an easy way to get our value back if we want to compete with sun types.

Let’s define a get function that extract a value of type ty from an union. To typecheck, ty must be a valid type (a type listed in the union). And we can’t be sure to obtain a ty. Thus, the type of get is:

get : Union ts -> {auto p: Elem ty ts} -> Maybe ty

And once again, the idea is to use the witness of the type position in the union (p) to compute the answer.

get : Union ts -> {auto e: Elem ty ts} -> Maybe ty
get (MemberHere x)  {e = Here}    = Just x
get (MemberHere x)  {e = There _} = Nothing
get (MemberThere x) {e = Here}    = Nothing
get (MemberThere later) {e = There l} =
  get later {e=l}

All these case should be straight forward. And now we can have (in the REPL):

>>> :let x = the (Union [String, Nat, List String]) $ member "Ahoy!"
>>> the (Maybe String) $ get x
Just "Ahoy!" : Maybe String
>>> the (Maybe Nat) $ get x
Nothing : Maybe Nat

We uset the here to provide a Type hint, but it won’t be useful in most of the cases, as the type will be provided by the context.

Part 1 is over

That’s all for today, you can continue with the fold for union type.