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
10 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 + […]

  5. javawerks says:

    Can you kindly explain the value proposition of this ‘type’ approach? Because the value approach is much cleaner. Or is this just an academic exercise? And do you really use this technique in production code? Just curious. Thanks!

    • barnesjd says:

      Thanks for taking the time to read and comment! Up to this point, it has been an academic exercise. However, if you check out the next post in this series (http://proseand.co.nz/2014/03/17/type-programming-constraining-values/), you’ll see where you can begin to utilize these types to constrain values at run time.

      I’ve not used the IntType I developed in this blog post in production, but I certainly utilize types in programming. That is unavoidable in Java and Scala. After going through these exercises, I gained a much better perspective on how to think about types.

      Hope this helps!

      • javawerks says:

        Thanks, mate. I appreciate the timely response. I’ll read your next blog entry on this topic.

        For sure, generic types are a way of life in Java and Scala. To what extent, though?

        In the Scala space, it’s difficult to separate what’s useful to the real world developer and the library wizard. I think I know. But I’d like to have a better sense of where that line divides us mere mortals from the gods of abstraction.;)

        For instance, I’m going through the Functional Programming in Scala book to get the Haskell perspective. Oops.;) And in that vein, I recall, Paul recently debating Roland on the usefulness of Actors versus a pure functional approach. Interesting.

        Given those kind of differences of opinion within the Scala space, no doubt the curious among us want to more deeply understand both sides of the Scala spectrum.

        Because the poorly worded Typesafe marketing expression of — just stay in the shallow end of the pool — is elitist and deeply insulting. For instance, how long before a kid would swim to the deep end of the pool when told to stay in the shallow end? A few seconds?;)

        Thanks, again, for your blog entries and thoughtful replies.

      • barnesjd says:

        Glad you’re finding this mess I make over here helpful. :D I like how Scala has a low-entry fee in that you can be quite productive in the “shallow end”. I can’t stay there tho. I venture out into the murky waters, and leave these blog posts behind like breadcrumbs so I know how I got there.

        I don’t worry myself much with what people are saying about it in those regards. I find Scala to be an incredibly useful tool, and I love exploring areas I’m underutilizing.

        As for the usefulness of generics and static-typing, I know you can get away without it and be quite productive. However, it can really solidify your code base and make rock-solid APIs. I don’t understand it well enough yet to make great use of it. I plan to soon resume this exploration and dive into shapeless. Just be on the lookout for blog updates in the coming weeks.

      • javawerks says:

        Having lived in Japan for 7 years, I enjoyed you zen-like response. Perhaps, in the future, you can give it more depth and shape.;)

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

Follow

Get every new post delivered to your Inbox.

Join 622 other followers

%d bloggers like this: