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] http://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/

About these ads

12 thoughts on “Type-Level Programming in Scala

  1. > Perhaps allowing recursion is actually a bug, but we’ll try to do some interesting things while it is possible.

    If its a bug, I don’t want to rely on this!…

    So is it a bug or not?

    • I think it’s definitely not a bug. Recursion is absolutely inevitable if you allow top-level defines, which is exactly what a type constructor member is. Any given type cannot recurse on itself (since the lambda calculus strictly does not support this), but it’s perfectly reasonable to refer to other types in the type environment, which opens up recursion. Scala’s type system is not a total language, so it cannot disallow recursion.

      • My uncertainty comes from a couple comments by Adriaan.

        First in a comment on the SKI encoding post, he seems to approve. But then, in a recent mailing list post, he says “… I would consider it a bug if you managed to make the type checker loop — or, more likely, overflow the stack …”. Probably

      • Yeah, while it may be possible to make Scala’s type system total, you will still want to allow recursion (and corecursion). To close the “bug” you would just be required to supply evidence that your recursion terminates (or coterminates).

      • No argument from me against it being useful to recurse- just that the infinite loop example compiles in 2.8 but not 2.7 (illegal cyclic reference or something). Since I don’t know of any official statement that this change was intentional, I can’t say for sure what will be supported in the future.

      • @philip I think the reverse-bug report would be a unit test verifying the type recursion is still present. Then if someone breaks it the test would start to fail.

  2. Pingback: High Wizardry in the Land of Scala « Another Word For It

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s