Overview
Type-level programming has many similarities with traditional, value-level programming. However, unlike value-level programming, where the computation occurs at runtime, in type-level programming, the computation occurs at compile time. I will try to draw parallels between programming at the value-level and programming at the type-level.
Paradigms
There are two main paradigms in type-level programming: "object-oriented" and "functional". Most examples linked to from here follow the object-oriented paradigm.
A good, fairly simple example of type-level programming in the object-oriented paradigm can be found in apocalisp's implementation of the lambda calculus, replicated here:
// Abstract trait
trait Lambda {
type subst[U <: Lambda] <: Lambda
type apply[U <: Lambda] <: Lambda
type eval <: Lambda
}
// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
type apply[U] = Nothing
type eval = S#eval#apply[T]
}
trait Lam[T <: Lambda] extends Lambda {
type subst[U <: Lambda] = Lam[T]
type apply[U <: Lambda] = T#subst[U]#eval
type eval = Lam[T]
}
trait X extends Lambda {
type subst[U <: Lambda] = U
type apply[U] = Lambda
type eval = X
}
As can be seen in the example, the object-oriented paradigm for type-level programming proceeds as follows:
- First: define an abstract trait with various abstract type fields (see below for what an abstract field is). This is a template for guaranteeing that certain types fields exist in all implementations without forcing an implementation. In the lambda calculus example, this corresponds to
trait Lambda that guarantees that the following types exist: subst, apply, and eval.
- Next: define subtraits that extend the abstract trait and implement the various abstract type fields
- Often, these subtraits will be parameterized with arguments. In the lambda calculus example, the subtypes are
trait App extends Lambda which is parameterized with two types (S and T, both must be subtypes of Lambda), trait Lam extends Lambda parameterized with one type (T), and trait X extends Lambda (which is not parameterized).
- the type fields are often implemented by referring to the type parameters of the subtrait and sometimes referencing their type fields via the hash operator:
# (which is very similar to the dot operator: . for values). In trait App of the lambda calculus example, the type eval is implemented as follows: type eval = S#eval#apply[T]. This is essentially calling the eval type of the trait's parameter S, and calling apply with parameter T on the result. Note, S is guaranteed to have an eval type because the parameter specifies it to be a subtype of Lambda. Similarly, the result of eval must have an apply type, since it is specified to be a subtype of Lambda, as specified in the abstract trait Lambda.
The Functional paradigm consists of defining lots of parameterized type constructors that are not grouped together in traits.
Comparison between value-level programming and type-level programming
- abstract class
- value-level:
abstract class C { val x }
- type-level:
trait C { type X }
- path dependent types
C.x (referencing field value/function x in object C)C#x (referencing field type x in trait C)
- function signature (no implementation)
- value-level:
def f(x:X) : Y
- type-level:
type f[x <: X] <: Y (this is called a "type constructor" and usually occurs in the abstract trait)
- function implementation
- value-level:
def f(x:X) : Y = x
- type-level:
type f[x <: X] = x
- conditionals
- checking equality
- value-level:
a:A == b:B
- type-level:
implicitly[A =:= B]
- value-level: Happens in the JVM via a unit test at runtime (i.e. no runtime errors):
- in essense is an assert:
assert(a == b)
- type-level: Happens in the compiler via a typecheck (i.e. no compiler errors):
- in essence is a type comparison: e.g.
implicitly[A =:= B]
A <:< B, compiles only if A is a subtype of BA =:= B, compiles only if A is a subtype of B and B is a subtype of AA <%< B, ("viewable as") compiles only if A is viewable as B (i.e. there is an implicit conversion from A to a subtype of B)- an example
- more comparison operators
Converting between types and values
In many of the examples, types defined via traits are often both abstract and sealed, and therefore can neither be instantiated directly nor via anonymous subclass. So it is common to use null as a placeholder value when doing a value-level computation using some type of interest:
- e.g.
val x:A = null, where A is the type you care about
Due to type-erasure, parameterized types all look the same. Furthermore, (as mentioned above) the values you're working with tend to all be null, and so conditioning on the object type (e.g. via a match statement) is ineffective.
The trick is to use implicit functions and values. The base case is usually an implicit value and the recursive case is usually an implicit function. Indeed, type-level programming makes heavy use of implicits.
Consider this example (taken from metascala and apocalisp):
sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat
Here you have a peano encoding of the natural numbers. That is, you have a type for each non-negative integer: a special type for 0, namely _0; and each integer greater than zero has a type of the form Succ[A], where A is the type representing a smaller integer. For instance, the type representing 2 would be: Succ[Succ[_0]] (successor applied twice to the type representing zero).
We can alias various natural numbers for more convenient reference. Example:
type _3 = Succ[Succ[Succ[_0]]]
(This is a lot like defining a val to be the result of a function.)
Now, suppose we want to define a value-level function def toInt[T <: Nat](v : T) which takes in an argument value, v, that conforms to Nat and returns an integer representing the natural number encoded in v's type. For example, if we have the value val x:_3 = null (null of type Succ[Succ[Succ[_0]]]), we would want toInt(x) to return 3.
To implement toInt, we're going to make use of the following class:
class TypeToValue[T, VT](value : VT) { def getValue() = value }
As we will see below, there will be an object constructed from class TypeToValue for each Nat from _0 up to (e.g.) _3, and each will store the value representation of the corresponding type (i.e. TypeToValue[_0, Int] will store the value 0, TypeToValue[Succ[_0], Int] will store the value 1, etc.). Note, TypeToValue is parameterized by two types: T and VT. T corresponds to the type we're trying to assign values to (in our example, Nat) and VT corresponds to the type of value we're assigning to it (in our example, Int).
Now we make the following two implicit definitions:
implicit val _0ToInt = new TypeToValue[_0, Int](0)
implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) =
new TypeToValue[Succ[P], Int](1 + v.getValue())
And we implement toInt as follows:
def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()
To understand how toInt works, let's consider what it does on a couple of inputs:
val z:_0 = null
val y:Succ[_0] = null
When we call toInt(z), the compiler looks for an implicit argument ttv of type TypeToValue[_0, Int] (since z is of type _0). It finds the object _0ToInt, it calls the getValue method of this object and gets back 0. The important point to note is that we did not specify to the program which object to use, the compiler found it implicitly.
Now let's consider toInt(y). This time, the compiler looks for an implicit argument ttv of type TypeToValue[Succ[_0], Int] (since y is of type Succ[_0]). It finds the function succToInt, which can return an object of the appropriate type (TypeToValue[Succ[_0], Int]) and evaluates it. This function itself takes an implicit argument (v) of type TypeToValue[_0, Int] (that is, a TypeToValue where the first type parameter is has one fewer Succ[_]). The compiler supplies _0ToInt (as was done in the evaluation of toInt(z) above), and succToInt constructs a new TypeToValue object with value 1. Again, it is important to note that the compiler is providing all of these values implicitly, since we do not have access to them explicitly.
Checking your work
There are several ways to verify that your type-level computations are doing what you expect. Here are a few approaches. Make two types A and B, that you want to verify are equal. Then check that the following compile:
