# Migratable Types in Idris 2

In the middle of last year I was introduced to a neat bit of Haskell code (which you can find here), which uses type-level programming to demonstrate the concept of *migratable types*. The idea here is to construct types which have versioning information associated with them, and to provide a means of migrating from one version of a type to the next.

This is probably more interesting as a theoretical exercise than something with practical uses, but the idea of having API versions and version dependencies encoded at the type level certainly seems rather novel.

Having seen this idea, I spent a while wondering whether it would be possible to implement the same thing (or something suitably similar) in Idris 2. Idris 2 is (the second iteration of) a pure, functional, dependently-typed programming language — this means that types are first-class, and can be treated like any other value, which is the gateway to all sorts of fun and interesting things.

## Idris trivia for Haskellers

(This is optional reading — feel free to skip down to the next section.)

As a toy example of the whole first-class types thing, here's an Idris function which returns a different type depending on the value it was passed:

toyExample : Bool -> Type
toyExample True = String
toyExample False = Int

Like Haskell, one can define types which are themselves parameterised by other types in Idris:

-- This is valid syntax in both Haskell and Idris.
data Either a b = Left a | Right b

However, Idris also allows one to define polymorphic types which are distinguished by different *values* (as opposed to other types), which is known as *dependent typing* in the literature. The canonical example of a dependent type is a vector, where the length of the vector is encoded in its type:

-- This is Idris's generalised algebraic data type syntax.
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
Cons : a -> Vect n a -> Vect (S n) a

where `Z`

and `S`

are the zero value and successor function in the Peano representation of natural numbers, respectively. The concrete type of a vector then depends on the natural number in its type as well as the type of the values it contains; `Vect 3 Int`

and `Vect 4 Int`

are different types, and attempting to use one where the other is expected will result in a type error.

Loading these examples into an Idris REPL (I'm using version 0.2.1 unless otherwise specified), we can inspect the types of the toy example function and the `Vect`

type constructor:

Main> :t toyExample
Main.toyExample : Bool -> Type
Main> :t Vect
Main.Vect : Nat -> Type -> Type
Main>

Given that `toyExample`

takes a value and computes a type, you could also consider the `Vect`

type constructor to be a function, which computes a type based on a natural number and another type.

One subtle little observation I've seen, which follows from this, is that you could consider Haskell's type aliases to be a form of type-level programming. Consider this Haskell code:

-- Using the monad transformer classes from the "transformers" library
import Control.Monad.Trans.Reader
import Control.Monad.Trans.State
data Config = Config { filepath :: String }
type MyApp = ReaderT Config (StateT Bool IO)

The `MyApp`

type is an alias for the stack of monad transformers sitting on top of the `IO`

context.

The Idris equivalent to the above code would look a bit like this:

-- Reader isn't in Idris v0.2.1, so you'll need a more recent version from git to
-- make these imports work.
import Control.Monad.Reader
import Control.Monad.State
record Config where
constructor MkConfig
filepath : String
MyApp : Type -> Type
MyApp = ReaderT Config (StateT Bool IO)

Idris doesn't have type aliases — you just define a function which takes a type as an argument, and then returns some other type!

## Migrating in Idris

Armed with a little Idris knowledge, and having seen the migratable types in Haskell, I thought that Idris's type system seemed like it would be amenable to writing something equivalent in a slightly more elegant manner.

In order to migrate types between different versions, they need an associated version number, which we can express as a dependent type with a natural number as a parameter:

Versioned : Type
Versioned = Nat -> Type

For demonstration purposes, I'm going to use the following versioned type:

data Example : Versioned where
Ex : (n : Nat) -> Example n

Now that I have a type which has an associated version number, I then need to provide some means for that type to declare how to take a value of one version and return a value of the next version. However, the steps required to move between two versions of a type depends on both the abstract type family (e.g. is this an `Example`

or is this a `Foobar`

?) and the concrete versioned type (e.g. are we starting with version 1 of an `Example`

or version 2?).

I can therefore write an interface definition which looks like this:

interface Migrate (n : Nat) (t : Versioned) | t where
migrate : t n -> t (S n)

This can be read as "types which are migratable at version N will provide an operation which converts a value of version N into a value of version N+1".

While this is a good start, it has a pretty significant problem. I'm going to implement this interface for version 2 of the `Example`

type:

implementation Migrate 2 Example where
migrate (Ex 2) = Ex 3

This code typechecks just fine, and I can verify that it works in the REPL:

Main> migrate (Ex 2)
Ex 3
Main>

If I have an `Example`

of version 2, then there must have been a version 1 preceding that, right?

Main> migrate (Ex 1)
(interactive):1:1--1:15:Can't find an implementation for Migrate 1 Example at:
1 migrate (Ex 1)
^^^^^^^^^^^^^^
Main>

What's missing here is a means of saying that for all versions of a type, except the first, there must exist some means of migrating from the predecessor version. This is also why the version number parameter in the `Versioned`

type is a `Nat`

, as Idris's natural number type is implemented using the Peano representation, which shares this recursive structure. (The original Haskell version had to implement type-level Peano numbers, but Idris's dependent types permit the reuse of the existing value-level definition.)

I then need to write a type which encapsulates the notion of a version bound associated with a `Versioned`

type, given as a parameter. Either this version bound is associated with the initial version of the associated parameter type, or the bound is associated with some non-initial version, in which case the parameter type should be migratable up to the preceding version.

data MigrateBound : (n : Nat) -> (t : Versioned) -> Type where
Bound0 : MigrateBound Z t
BoundN : (Migrate n t) => MigrateBound (S n) t

Then, I can modify the `Migrate`

interface to add a type constraint, which says that if a type is migratable at version N, then it must be possible to construct a version bound for that version (and then, recursively, that it is either an initial version or must be migratable to the preceding version, etc):

interface (MigrateBound n t) => Migrate (n : Nat) (t : Versioned) | t where
migrate : t n -> t (S n)

Now, I've created a problem for myself with this definition, as my implementation of `Migrate 2`

for `Example`

now no longer type checks!

Can't find an implementation for MigrateBound 2 Example at:
18 implementation Migrate 2 Example where
19 migrate (Ex 2) = Ex 3

Before I can write this implementation, I need to have an implementation of `Migrate 1`

(in order to satisfy the `MigrateBound`

constraint), which in turn needs a version of `Migrate 0`

. So I now need to write the following code:

implementation Migrate 0 Example where
migrate (Ex 0) = Ex 1
implementation Migrate 1 Example where
migrate (Ex 1) = Ex 2
implementation Migrate 2 Example where
migrate (Ex 2) = Ex 3

And now the code typechecks once more.

I can then use these migration functions in the REPL like this:

Main> :t Ex 0
Ex 0 : Example 0
Main> :t Ex 1
Ex 1 : Example 1
Main> migrate (Ex 0)
Ex 1
Main> migrate (Ex 1)
Ex 2
Main> migrate (Ex 2)
Ex 3
Main> (migrate . migrate) (Ex 1)
Ex 3
Main>

Thus, migratable types, in Idris 2:

-- Note that as the definitions of Migrate and MigrateBound are mutually
-- recursive, one of them has to be declared before it's fully defined.
Versioned : Type
Versioned = Nat -> Type
data MigrateBound : (n : Nat) -> (t : Versioned) -> Type
interface (MigrateBound n t) => Migrate (n : Nat) (t : Versioned) | t where
migrate : t n -> t (S n)
data MigrateBound : (n : Nat) -> (t : Versioned) -> Type where
Bound0 : MigrateBound Z t
BoundN : (Migrate n t) => MigrateBound (S n) t

## Acknowledgements

Thanks to Vincent Ambo for writing the original Haskell implementation in the first place, and the inspiration for writing an Idris version; and to Edwin Brady for some interesting conversations on this kind of type-level programming, and some useful hints towards getting this code working.