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
5. Binary type-level numbers
6. Heterogeneous Lists
7. Natural Transformation Literals
8. KList: a higher-kinded HList

Prior work/reference:

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.

12 thoughts on “Type-Level Programming in Scala”

1. Agl says:

I’m afraid I’m not even sure what to use the feature above for. Any examples?

2. philip andrew says:

> 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?

• Rúnar says:

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.

• Mark says:

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

• Runar says:

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).

• Mark says:

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.

• You should really make sure that it is not declared a bug – somehow.

How can you submit a reverse-bug report? to keep a feature?

• @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.