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.

- Type recursion (this post)
- “Implicitly” and type equality
- Booleans
- Naturals
- Binary type-level numbers
- Heterogeneous Lists
- Natural Transformation Literals
- KList: a higher-kinded HList

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/

The link to http://www.cs.kuleuven.be/~adriaan/files/higher.pdf is messed up. A lot of extraneous text got into the href=”” attribute.

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

HLists and natural transformation (parts 6,7,8) are examples from this series. See also the references and Adriaan’s type constructor inference article.

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

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.

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

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

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.

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

Like it. Thanks…. followed that article before: http://www.kammerath.co.uk/The-Joys-of-functional-programming-in-Scala.html — My question when it comes to typing is always, what is the ideal compromise between PHP (no or extremely weak typing) to CPP (heavy/strong typing)… I think Scala, Java and C# have quite a good compromise.