Scala type programming resources

Question

According to this question, Scala's type system is Turing complete. What resources are available that enable a newcomer to take advantage of the power of type-level programming?

Here are the resources I've found so far:

• Daniel Spiewak's High Wizardry in the Land of Scala
• Apocalisp's Type-Level Programming in Scala
• Jesper's HList

These resources are great, but I feel like I'm missing the basics, and so do not have a solid foundation on which to build. For instance, where is there an introduction to type definitions? What operations can I perform on types?

Are there any good introductory resources?

Answer 1

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
  • see here
• 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 B
    • A =:= B, compiles only if A is a subtype of B and B is a subtype of A
    • A <%< 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:

• Equal[A, B]
  • with: trait Equal[T1 >: T2 <: T2, T2] (taken from apocolisp)
• implicitly[A =:= B]

Alternatively, you can convert the type to a value (as shown above) and do a runtime check of the values. E.g. assert(toInt(a) == toInt(b)), where a is of type A and b is of type B.

Additional Resources

The complete set of available constructs can be found in the types section of the scala reference manual (pdf).

Adriaan Moors has several academic papers about type constructors and related topics with examples from scala:

• Generics of a higher kind (pdf)
• Type Constructor Polymorphism for Scala: Theory and Practice (pdf) (PhD thesis, which includes the previous paper by Moors)
• Type Constructor Polymorphism Inference

Apocalisp is a blog with many examples of type-level programming in scala.

• Type-Level Programming in Scala is a fantastic guided tour of some type-level programming which includes booleans, natural numbers (as above), binary numbers, heterogeneous lists, and more.
• More Scala Typehackery is the lambda calculus implementation above.

ScalaZ is a very active project that is providing functionality that extends the Scala API using various type-level programming features. It is a very interesting project that has a big following.

MetaScala is a type-level library for Scala, including meta types for natural numbers, booleans, units, HList, etc. It is a project by Jesper Nordenberg (his blog).

The Michid (blog) has some awesome examples of type-level programming in Scala (from other answer):

• Meta-Programming with Scala Part I: Addition
• Meta-Programming with Scala Part II: Multiplication
• Meta-Programming with Scala Part III: Partial function application
• Meta-Programming with Scala: Conditional Compilation and Loop Unrolling
• Scala type level encoding of the SKI calculus

Debasish Ghosh (blog) has some relevant posts as well:

• Higher order abstractions in scala
• Static typing gives you a head start
• Scala implicits type classes, here I come
• Refactoring into scala type-classes
• Using generalized type constraints
• How scalas type system words for you
• Choosing between abstract type members

(I've been doing some research on this subject and here's what I've learned. I'm still new to it, so please point out any inaccuracies in this answer.)