Type Programming: Recursive types

A few weeks ago, I posted my first foray into type programming by exploring the parallels between value-level programming and type-level programming. In that post, I shared a simple implementation of Boolean logic using two types along with some familiar operations. In this post, I will continue to look at these parallels with an example of a recursive type. Before we get started there, I want to first improve upon the last post’s example.

Thanks to this answer to my stack overflow question, I have discovered that self types work in type programming as well. For the scope of this post, you can think of self types as an alternative to the keyword this where you specify the name you want to use although here and in most cases, the name self is used. (For a more exhaustive treatment of the self type annotation, read this excellent post.) This is what it looks like in our BoolVal code:

sealed trait BoolVal { self =>
  def not:BoolVal
  def or(that:BoolVal):BoolVal
  def and(that:BoolVal) =
    (self.not or that.not).not
  def imp(that:BoolVal) =
    self.not or that

In this source the self alias doesn’t gain us much. However, it substantially improves the BoolType code. Firstly, we are using the exact same construct as in the BoolVal source, which makes the type/value parallel even more pronounced. Secondly and more importantly, there is no burden on the sub types to implement This. See for yourself:

sealed trait BoolType { self =>
  type Not <: BoolType
  type Or[That <: BoolType] <: BoolType
  type And[That <: BoolType] = self.type#Not#Or[That#Not]#Not
  type Imp[That <: BoolType] = self.type#Not#Or[That]
sealed trait TrueType extends BoolType {
  override type Not = FalseType
  override type Or[That <: BoolType] = TrueType
sealed trait FalseType extends BoolType {
  override type Not = TrueType
  override type Or[That <: BoolType] = That

Thanks EECOLOR for taking the time to give your answer to my question.

So moving along, we don’t have to limit ourselves to a finite set of types as we did in our BoolType example. What I mean is that there are ultimately only two different types available, namely FalseType and TrueType. Everything else is equivalent to one of the two. Just as with value-level programming where we can have an unbounded set of values, we can have a set of types which has an unbounded cardinality thanks to type recursion.

For our recursive type, we will examine Peano numbers. (Thanks again to the apocalyspe blog for the inspiration). For our discussion, Peano numbers are the natural numbers (starting with zero) defined recursively. As with the previous post, we will start with a look at the value-level implementation.

sealed trait PeanoVal 
case object Val0 extends PeanoVal
case class ValN(prev:PeanoVal) extends PeanoVal

Here we have our base trait, an object for zero, and a recursive definition for every successive value. Hence we can define more values like this.

val Val1 = ValN(Val0)
val Val2 = ValN(Val1)
val Val3 = ValN(Val2)

Now let’s begin to make these more interesting with an add operation.

sealed trait PeanoVal {
  def add(that:PeanoVal):PeanoVal
case object Val0 extends PeanoVal {
  override def add(that:PeanoVal) = that
case class ValN(prev:PeanoVal) extends PeanoVal {
  override def add(that:PeanoVal) = ValN(prev add that)

The thoroughly curious are welcome to see the test code. With the above definition we can construct an arbitrarily-large set of values and add them to one another with our add operator. Just as with our last post, we can do the parallel of these values in the Scala type system. Let’s get right to it.

sealed trait PeanoType {
  type add[That <: PeanoType] <: PeanoType
sealed trait Type0 extends PeanoType {
  override type add[That <: PeanoType] = That
sealed trait TypeN[Prev <: PeanoType] extends PeanoType {
  override type add[That <: PeanoType] = TypeN[Prev#add[That]]

Now we have an example of a recursive type. The TypeN trait takes as an argument another PeanoType. This guy is called a type constructor. Given a type (Prev in this case), it constructs a new type (TypeN[Prev]). Thanks to the Turing-complete Scala compiler, we now have a recursively-defined type and hence an unbounded set of types. Here is some test code to show some playing around with the types. I first defined a few types for convenience, then used our handy implicitly and illTyped from shapeless.

object PeanoTypeSpecs {
  type Type1 = TypeN[Type0]
  type Type2 = TypeN[Type1]
  type Type3 = TypeN[Type2]

  implicitly[Type0 =:= Type0]
  illTyped("implicitly[Type0 =:= Type1]")

  implicitly[Type0#add[Type1] =:= Type1]
  implicitly[Type1#add[Type1] =:= Type2]
  implicitly[Type1#add[Type2] =:= Type3]

Pretty cool, huh? Now we are able to generate an unlimited (in theory) number of types from our type definition. This is an interesting shift in paradigm, as I have always thought of as creating single types which are a mere footprint for the values that conform to them. Even the familiar type constructors such as List[T] are limited by the cardinality of T. In this case, the cardinality is limited only by the machine.

There are a few limitations that I’ve run into with the last two posts I’d like to highlight. Firstly notice that we cannot drop the hashtag or the square brackets like we can drop the period and parentheses with value-level programming. Also I’ve noticed that type names are a little more restrictive than values, functions, etc. Otherwise, I would have used + in lieu of add.

In my next post (UPDATE: posted) I have in mind to play around with these types in value-level programming. Now that we’ve begun to explore this power in the compiler, I’m curious how we can leverage it to improve our value-level programming.

About these ads
Tagged with: , , ,
Posted in Software Development
5 comments on “Type Programming: Recursive types
  1. […] pretty jazzed about this topic, so don’t expect a long delay before a follow up (EDIT: posted). I plan to stroll around in value land with our new types and then look at defining types for an […]

  2. […] my last type-programming post, I briefly touched on the topic of recursive type definitions by creating a Peano-encoded integer […]

  3. Jesper de Jong says:

    You don’t even need the self-type annotation (“self =>”), you could have used “this” directly, for example:

    sealed trait BoolType {
    // …
    type And[That <: BoolType] = this.type#Not#Or[That#Not]#Not

  4. […] time we explored how we can use the Peano-encoded natural number type to define constraints on on values. In particular, we created an IntList type which has a + […]

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


Get every new post delivered to your Inbox.

Join 548 other followers

%d bloggers like this: