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.