Type-Level Programming in Scala

This series is intended as a guided tour of some type-level programming I have done in Scala. It generally consists of code and examples with a few lines of explanation. It is usually assumed that the reader understands the features of Scala’s type system. This is not always a good assumption about either the author or the reader of course, so comments and questions are welcome.

The series is in 10 parts, with some parts consisting of more than one post each. The present post will serve as a table of contents linking to the rest of the series, so bookmark this page for easy reference.

1. Type recursion (this post)
2. “Implicitly” and type equality
3. Booleans
4. Naturals
   1. Peano Number Basics
   2. Comparing Peano Numbers
   3. General Recursion on Peano Numbers
   4. Peano Arithmetic
5. Binary type-level numbers
   1. Binary Numbers
   2. Project Euler Problem 4
6. Heterogeneous Lists
   1. HList Basics
   2. HList Folds
   3. HList Indexing
   4. HList Zip/Unzip
   5. HList Apply
   6. Deriving Type-Class Instances Through HList
   7. Type-Indexed HLists
7. Natural Transformation Literals
8. KList: a higher-kinded HList
1. KList Motivation
2. KList Basics
3. KList zipWith

Prior work/reference:

http://www.cs.kuleuven.be/~adriaan/files/higher.pdf
http://jnordenberg.blogspot.com
http://michid.wordpress.com
http://matt.immute.net
http://jim-mcbeath.blogspot.com
http://blog.tmorris.net
http://code.google.com/p/scalaz

All source code is available at http://github.com/harrah/up.
Get the source and use sbt console to try things out.

Part 1: Type Recursion

Scala’s type system in 2.8 allows recursion, and infinite recursion at that, as demonstrated in [1,2]. Arbitrary recursion is not allowed, as seen by ‘illegal cyclic reference’ errors. Perhaps allowing recursion is actually a bug, but we’ll try to do some interesting things while it is possible.

To use recursion, define a trait with a type declaration. A type declaration is an abstract type that can have type parameters and bounds. Then, define a subtrait that implements the type declaration. Recursion is allowed in this implementation, with restrictions that are discussed later.

Infinite Loop Example:

// define the abstract types and bounds
trait Recurse {
  type Next <: Recurse
  // this is the recursive function definition
  type X[R <: Recurse] <: Int
}
// implementation
trait RecurseA extends Recurse {
  type Next = RecurseA
  // this is the implementation
  type X[R <: Recurse] = R#X[R#Next]
}
object Recurse {
  // infinite loop
  type C = RecurseA#X[RecurseA]
}

Note that Int is arbitrary and could be replaced by any type. In general, this bound will be something meaningful. Like any other bound, it allows you to know something about the result without knowing the exact parameters provided.

There are some rules to follow to enable recursion. The upper bound can be a function of the type parameters, but it cannot change during recursion.

Consider:

trait Recurse {
  type X[A, B] <: A
}

for some types A and B. The implementation of X in some subtrait of Recurse cannot change A during recursion, but B can change. Concrete examples of this will be seen in later posts dealing with type-level numbers, HLists, and binary search trees.

Another restriction is that all recursion must be through a prefix, like a type projection:

type X[R <: Recurse] = R#X[R#Next]

You cannot do direct recursion on a type member on the current type like this:

type X[R <: Recurse] = X[R#Next]

So, with some reasonable restrictions, we have recursion and corecursion in the type-system, and thus full initial algebra semantics. Scala’s type system is a Turing-equivalent programming language.

[1] https://apocalisp.wordpress.com/2009/09/02/more-scala-typehackery/
[2] http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/