Type programming: Shifting from values to types

Earlier this week, I got an itch to tinker around some more with SNMP4S, even tho I’m far removed from the telecom industry. It was really a fun project, and it still has a long way to go. Out of the ideas I’ve had since starting Scala, it is the one that has the most to benefit from the language features. It is still my most popular github repository, and I hate how much of a train wreck it is. In order for me to get it into a respectable state, I need to understand a lot more about the type system in Scala. So as of this morning, I have decided it is time for me to actually learn type programming in Scala. For someone who has written so much about static typing, I sure know little about getting the compiler to work for me.

There are certainly no shortages to information on type-level programming in Scala. I found a great starting point with this Stack Overflow answer/wiki page. However, I find that all of the resources out there thrust the reader so quickly into the deeper areas of the pool, that reading them is akin to flailing for my life until the lifeguard rescues me and the only lesson I’ve learned is how to not die while in the pool. In this post, I will gently break us into type programming in the kiddie pool. The product of this blog post will be no more useful than the first program I ever wrote. The education gathered a long the way is the value more so than the artifact produced. If all goes well, I will continue to learn type programming out loud and erupt into a blog series much like Eugene Yokota‘s foray into learning Scalaz. However, don’t be surprised if the series mysteriously disappears much like this well-written series on Scala Monads, because well… I’m a busy guy. Hopefully I can keep it up, though because the best way I know to learn something is to teach it to someone else. All of the source I use in the post is available on GitHhub, tagged 1.0 for this particular blog post. Also of note is my choice to utilize Scala version 2.10.3. Originally I began this with Scala 2.9.1 with cross-compilation from 2.9.1 all the way up to 2.10.3. In general, this is just how I roll when I’m not building an application. But I later brought in a dependency for testing which required me to bump up to 2.10.3.

First things first, what is type programming and what is the motivation for type programming? I’ll answer it colloquially and leave you to Google for the proper academic response. After you write Scala code, it gets crunched twice. First by the scalac compiler, secondly by the JRE run time. Type programming executes in the compiler, value programming executes in the run time. Mistakes in your type programming translate to errors from the compiler, while mistakes in your value programming manifest as errors at run time.

Since we don’t like mistakes, we want to use whatever tools are available to validate our work. Catching mistakes sooner is always better. It seems natural then that validating code with the compiler is preferable to validating with test code at run time. It is especially preferable when we consider all code is validated by the compiler, while the only code that is validated at run time by tests is the code you didn’t forget to test. Hence, the onus is on you the developer to write a good run time test.

Let’s start with some value programming, which we all know and love. This seems to be a natural starting point for me and the audience I have in mind, because we’re already adept to good value programming. From there, I hope we can ease our way into some likewise good type programming. Let’s start with the simplest value there is, a Boolean. We’ll write our own Boolean implementation called BoolVal.

Define BoolVal, TrueVal, and FalseVal

First, let’s define BoolVal as a trait and define the two lone members of the set of Boolean values, TrueVal and FalseVal.

sealed trait BoolVal

case object TrueVal extends BoolVal
case object FalseVal extends BoolVal

We can easily see that we satisfy the first property of Boolean values we’ve come to expect in that there are only two existing (the sealed keyword guarantees that the only types which extend BoolVal are defined in the current file). Because we’re utilizing case objects, we also get the equality properties of Boolean algebra satisfied as the following test code demonstrates.

class BoolValSpecs extends WordSpec with ShouldMatchers {
  "FalseVal" should {
    "equal itself" in { FalseVal should equal (FalseVal) }
    "not equal TrueVal" in { FalseVal should not equal (TrueVal) }
  }

  "TrueVal" should {
    "equal itself" in { TrueVal should equal (TrueVal) }
    "not equal FalseVal" in { TrueVal should not equal (FalseVal) }
  }
}

Define BoolVal.or, BoolVal.not

Now let’s define the or binary operator and the not unary operator to make things a little more interesting.

sealed trait BoolVal {
  def not:BoolVal
  def or(that:BoolVal):BoolVal
}

The implementations are straight-forward. I don’t mean to be overly tedious… I know my intended audience is good at value programming, but just bear with me.

case object TrueVal extends BoolVal {
  override val not = FalseVal
  override def or(that:BoolVal) = TrueVal
}
case object FalseVal extends BoolVal {
  override val not = TrueVal
  override def or(that:BoolVal) = that
}

I’ll spare you the validation code, but you’re welcome to go see it for yourself.

Define BoolVal.and, BoolVal.imp

What I find genuinely interesting is that we can define everything else about predicate logic from these two functions. For our discussion, I will only implement and and imp for “implies”.

sealed trait BoolVal {
  def not:BoolVal
  def or(that:BoolVal):BoolVal
  def and(that:BoolVal) = (this.not or that.not).not
  def imp(that:BoolVal) = this.not or that
}

Again you’re welcome to the validation code. Let’s call our BoolVal “done”. Now let’s see if we can write this some logic into the type system. We’ll go through the same incremental steps as with BoolVal.

Define BoolType, TrueType, and FalseType

So first things first, let’s define the base type and the true/false types. (Note, here I am borrowing heavily from this Apocalisp blog post. In fact, it’s a copy/paste/rename for the production code)

sealed trait BoolType
sealed trait TrueType extends BoolType
sealed trait FalseType extends BoolType

The definition is basically the same as our value-programming counterpart. The big difference of course is that we originally had an object which is an instantiated instance of the BoolVal type, but here we have fully-abstracted traits. Yet a simple pattern is preserved here, which is the notion of a parent Bool_ thing and two (and only two thanks to the sealed keyword) child things. While both worlds have the same construct as a parent (a sealed trait), the children are very different. The value world has two instances of the parent type, and the type world has two sub-types of the parent type. It’s as if we’re staying in the type axis of programming, rather than crossing over to the value axis.

When we created our TrueVal and FalseVal case objects, we got equality (and hence inequality) for free. We also get that for free with our types. For this, we utilize implicitly and the operator =:=. Here is our “test” code.

object BoolTypeSpecs {
  implicitly[TrueType =:= TrueType]
  implicitly[FalseType =:= FalseType]
}

How do you test it? Simply run the compiler, of course! Since I’ve defined this in the test directory, we invoke the compiler for the test tree in sbt thusly:

> test:compile
[info] Compiling 3 Scala sources to C:\Users\jbarnes\code\type-prog\target\scala-2.10\classes...
[info] Compiling 2 Scala sources to C:\Users\jbarnes\code\type-prog\target\scala-2.10\test-classes...
[success] Total time: 6 s, completed Feb 16, 2014 12:02:12 PM
>

We can also validate the negative test cases.

object BoolTypeSpecs {
  implicitly[TrueType =:= TrueType]
  implicitly[FalseType =:= FalseType]
  implicitly[TrueType =:= FalseType]
  implicitly[FalseType =:= TrueType]
}

Again, we only need to compile. What do you expect to happen? If you thought “compilation failure,” then you are correct.

> test:compile
[info] Compiling 1 Scala source to C:\Users\jbarnes\code\type-prog\target\scala-2.10\test-classes...
[error] C:\Users\jbarnes\code\type-prog\src\test\scala\com\joescii\typed\BoolTypeSpecs.scala:6: Cannot prove that com.joescii.typed.TrueType =:= com.joescii.typed.FalseType.
[error]   implicitly[TrueType =:= FalseType]
[error]             ^
[error] C:\Users\jbarnes\code\type-prog\src\test\scala\com\joescii\typed\BoolTypeSpecs.scala:7: Cannot prove that com.joescii.typed.FalseType =:= com.joescii.typed.TrueType.
[error]   implicitly[FalseType =:= TrueType]
[error]             ^
[error] two errors found
[error] (test:compile) Compilation failed
[error] Total time: 0 s, completed Feb 16, 2014 12:02:53 PM
>

Although this is precisely what we expect to happen, we have a big of a problem here. How can we keep this code as part of our test suite? The compilation fails, so we aren’t able to go on and run our specs for BoolVal. If you take a look at the scaladocs for Predef where =:= comes from, you won’t find the negation. Fortunately, there is already a solution to this problem in the macro-based illTyped from the notorious Shapeless library. Let’s add it to our code…

import shapeless.test.illTyped

object BoolTypeSpecs {
  implicitly[TrueType =:= TrueType]
  implicitly[FalseType =:= FalseType]
  illTyped("implicitly[TrueType =:= FalseType]")
  illTyped("implicitly[FalseType =:= TrueType]")
}

…And compile…

> test:compile
[info] Compiling 1 Scala source to C:\Users\jbarnes\code\type-prog\target\scala-2.10\test-classes...
[success] Total time: 1 s, completed Feb 16, 2014 12:03:19 PM
>

Our code compiles. But of course it does… That’s just a string that contains something that makes the compiler break. We could do that all day. What is important is that the compiler breaks if the string is good!

object BoolTypeSpecs {
  illTyped("implicitly[TrueType =:= TrueType]")
  illTyped("implicitly[FalseType =:= FalseType]")
  illTyped("implicitly[TrueType =:= FalseType]")
  illTyped("implicitly[FalseType =:= TrueType]")
}

When the above is compiled, we get errors.

> test:compile
[info] Compiling 1 Scala source to C:\Users\jbarnes\code\type-prog\target\scala-2.10\test-classes...
[error] C:\Users\jbarnes\code\type-prog\src\test\scala\com\joescii\typed\BoolTypeSpecs.scala:6: Type-checking succeeded unexpectedly.
[error] Expected some error.
[error]   illTyped("implicitly[TrueType =:= TrueType]")
[error]           ^
[error] C:\Users\jbarnes\code\type-prog\src\test\scala\com\joescii\typed\BoolTypeSpecs.scala:7: Type-checking succeeded unexpectedly.
[error] Expected some error.
[error]   illTyped("implicitly[FalseType =:= FalseType]")
[error]           ^
[error] two errors found
[error] (test:compile) Compilation failed
[error] Total time: 0 s, completed Feb 16, 2014 12:04:53 PM
>

Define BoolType#Or, BoolType#Not

Reverting those changes, let’s move forward. That was a lot of work to just establish equality/inequality and I hope you’re still with me. Let’s start making things interesting and define the Not type.

sealed trait BoolType {
  type Not <: BoolType
}
sealed trait TrueType extends BoolType {
  type Not = FalseType
}
sealed trait FalseType extends BoolType {
  type Not = TrueType
}

So here we have strong analogies to the value world. I bet we could do a regex replace to go from the value programming to type programming. Rather than def we have type. Rather than : to separate the name from the type declaration, we have <:. Then in order to stick with conventions, we capitalized Not. Now for the test code.

object BoolTypeSpecs {
  // ...
  implicitly[TrueType#Not =:= FalseType]
  implicitly[FalseType#Not =:= TrueType]
  illTyped("implicitly[TrueType#Not =:= TrueType]")
  illTyped("implicitly[FalseType#Not =:= FalseType]")
}

Again everything is analogous to value programming. The only notable difference is we use # to navigate the name space rather than .. (I’m quite sure that’s the first time I’ve ever correctly ended a sentence with two periods). Thus far I feel pretty good about type programming given what I know about value programming. Now let’s define Or.

sealed trait BoolType {
  type Not <: BoolType
  type Or[That <: BoolType] <: BoolType
}
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
}

And the test code:

object BoolTypeSpecs {
  // ...
  implicitly[TrueType#Or[TrueType] =:= TrueType]
  implicitly[TrueType#Or[FalseType] =:= TrueType]
  implicitly[FalseType#Or[TrueType] =:= TrueType]
  implicitly[FalseType#Or[FalseType] =:= FalseType]
}

The analogy from the value world continues here in that we now have [That <: BoolType] to indicate parameter rather than (that:BoolVal) syntax.

Define BoolType#And, BoolType#Imp

So now it’s time to wrap this thing up with our definitions for And and Or. I had to cry uncle when I hit this, and asked a question on Stack Overflow. Within minutes, Owein Reese answered my question. Simply put, I didn’t know the analogy for the this keyword in value-programming or the equivalent for a self-type reference. It turns out you have to make it yourself. Let’s first define a This type on our traits.

sealed trait BoolType {
  protected type This <: BoolType
  type Not <: BoolType
  type Or[That <: BoolType] <: BoolType
}
sealed trait TrueType extends BoolType {
  protected override type This = TrueType
  override type Not = FalseType
  override type Or[That <: BoolType] = TrueType
}
sealed trait FalseType extends BoolType {
  protected override type This = FalseType
  override type Not = TrueType
  override type Or[That <: BoolType] = That
}

I made This protected since this in value-programming is only available in private scope. Now that we have a This, we can define And and Imp using the same definition from when we were value-programming earlier.

sealed trait BoolType {
  protected type This <: BoolType
  type Not <: BoolType
  type Or[That <: BoolType] <: BoolType
  type And[That <: BoolType] = This#Not#Or[That#Not]#Not
  type Imp[That <: BoolType] = This#Not#Or[That]
}

For good measure, here is the verification code.

object BoolTypeSpecs {
  // ...
  implicitly[TrueType#And[TrueType] =:= TrueType]
  implicitly[TrueType#And[FalseType] =:= FalseType]
  implicitly[FalseType#And[TrueType] =:= FalseType]
  implicitly[FalseType#And[FalseType] =:= FalseType]

  implicitly[TrueType#Imp[TrueType] =:= TrueType]
  implicitly[TrueType#Imp[FalseType] =:= FalseType]
  implicitly[FalseType#Imp[TrueType] =:= TrueType]
  implicitly[FalseType#Imp[FalseType] =:= TrueType]
}

Pretty cool, huh? I feel like I’ve found the magic potion of programming that creates the door to Mario Bros. 2 Subspace. While this new world certainly looks different on the surface, we can see direct parallels to our familiar Subcon. We may be a little bit limited in Subspace, but there’s great stuff to be found here that will make us much more awesome when we return to Subcon. On the surface it appears were doing the same stuff just with different syntax, so don’t lose sight of the significance of what has happened here. We executed logic in the compiler, not in the JVM. All of this type-level programming has nothing to do with Scala being a JVM language. This runs exclusively in the scalac compiler long before the JVM is involved. While such a Turing-complete type system is often unnecessary for most use cases, I like knowing that it is plenty powerful for whatever I may find myself in need of expressing in static compilation time. I feel like there is some irony here, too. I think we can argue that type programming is just dynamically-typed programming that executes in the scalac compiler…

That wraps up this first type programming blog post. I’m 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 abstraction which isn’t finite like Booleans.

About these ads
Tagged with: , , ,
Posted in Software Development
16 comments on “Type programming: Shifting from values to types
  1. Ian says:

    Actually, with a slight tweak, you can make this analogy between types and values even more interesting. It turns out that Scala’s type system allows you to write any type with two parameters as an infix type, as Op[T,U] =:= T Op U. For example, here’s a reformulation of your BoolTypes with this modification made (Note: I chose to implement Not and Imp as the primitives, just to make this a bit easier):

    object Bools {
    sealed trait BoolType {
    type Not <: BoolType
    type Imp[That <: BoolType] <: BoolType
    }

    sealed trait TrueType extends BoolType {
    override type Not = FalseType
    override type Imp[That <: BoolType] = That
    }

    sealed trait FalseType extends BoolType {
    override type Not = TrueType
    override type Imp[That <: BoolType] = TrueType
    }

    type ![T <: BoolType] = T#Not
    type &&[T <: BoolType, U <: BoolType] = (T#Not || U#Not)#Not
    type ||[T <: BoolType, U [T <: BoolType, U TrueType =:= TrueType]
    implicitly[TrueType ==> FalseType =:= FalseType]
    implicitly[FalseType ==> TrueType =:= TrueType]
    implicitly[FalseType ==> FalseType =:= TrueType]
    }

    Now, I ended up implementing the “Not” operator as just ![T <: BoolType], but I kind of wish that you could define it as
    unary_![T <: BoolType], and then write just !T (just like you can do with unary operators on values). I suppose I'll pitch that to the community; it'll make the analogy more consistent here. Of course, if you find the symbolic operators difficult to read, you can also define the alphanumeric versions instead and still write them infix (e.g. T Or U).

    Actually, what's even more interesting is that Martin Odersky has offered that in Scala 3, we replace existential and higher-kinded types with a syntax more analogous to ordinary classes; i.e. if you want a type parameter to be accessible publicly, you write

    class test[type T] {}

    and this is equivalent to

    class test {
    type T
    }

    analogously to writing val or var in the class parameters.

    Wow, that was way longer than I intended it to be…

    ~Ian

    • barnesjd says:

      Dude Ian, get your own blog! :D

      As always, thanks for commenting. That’s cool that we can infix type operators with two arguments, just like a case class with two parameters. I likewise tried to do the unary_! when I was playing with it to write this blog. I was disappointed to find it doesn’t work. I’m looking forward to what else I have to learn in type-level programming. Good stuff!

      I haven’t read any into Scala 3 yet. I’m really curious what they have in mind. I wonder if they’ll fix all the stuff the likes of Paul Phillips lose sleep over.

      • Ian says:

        XD

        Actually, I do have a blog, though it’s severely neglected and I rarely post anything about programming principles there. Maybe this is the kind of thing I need to actually get posting…le sigh.

        AFAIK, they’re going to try to simplify the language quite a bit in Scala 3, so that we can get an essentially unified language with the same powerful features as Scala 2, but with fewer primitives.

        ~Ian

    • Timur says:

      @lan, Hi lan!
      Someting wrong happend with your code example after line
      type &&[T <: BoolType, U <: BoolType] = (T#Not || U#Not)#Not

      I think it should go somewhat like this:

      object Bools {
      import scala.language.higherKinds
      sealed trait BoolType {
      type Not <: BoolType
      type Imp[That <: BoolType] <: BoolType
      }

      sealed trait TrueType extends BoolType {
      override type Not = FalseType
      override type Imp[That <: BoolType] = That
      }

      sealed trait FalseType extends BoolType {
      override type Not = TrueType
      override type Imp[That <: BoolType] = TrueType
      }
      // convenient type operations
      type ![T [T <: BoolType, U <: BoolType] = T#Imp[U]
      type &&[T <: BoolType, U <: BoolType] = ![![T] || ![U]]
      type ||[T <: BoolType, U U
      // test AND
      implicitly[TrueType && TrueType =:= TrueType]
      implicitly[TrueType && FalseType =:= FalseType]
      implicitly[FalseType && TrueType =:= FalseType]
      implicitly[FalseType && FalseType =:= FalseType]
      // test OR
      implicitly[TrueType || TrueType =:= TrueType]
      implicitly[TrueType || FalseType =:= TrueType]
      implicitly[FalseType || TrueType =:= TrueType]
      implicitly[FalseType || FalseType =:= FalseType]
      // test implication
      implicitly[TrueType ==> TrueType =:= TrueType]
      implicitly[TrueType ==> FalseType =:= FalseType]
      implicitly[FalseType ==> TrueType =:= TrueType]
      implicitly[FalseType ==> FalseType =:= TrueType]
      }

      @barnesjd? Hi barnesjd!
      Thank you for this good and simple post! In such uncluttered examples fundamental principles are much clearer than in advanced stuff.

      • barnesjd says:

        You’re very welcome! The simplicity is a product of this being a very new concept for me, and I’m glad that the write up of my endeavor is helping others begin to understand. Thanks for reading and taking the time to explore with us!

      • Timur says:

        Oh no, my code has been ruined too :(

  2. Barnes, I found your post via the This Week in Scala series at Cake Solutions.

    And that was… beautiful.

    One of the simplest and most concise introductions to type-programming with Scala I’ve read. The example was easy to follow and wrap my head around. And the analogy between value programming and type programming was perfect. The example you used to demonstrate the analogy was also perfectly chosen.

    I’ve been meaning to explore this part of the Scala world for a long time, and your post serves as a great starting point and inspiration as well.

    Thank You!

    • barnesjd says:

      While I greatly appreciate the high praises, I most enjoy hearing that my post helped you understand the topic presented. Thank you for taking the time to read and comment. Check back occasionally and continue to explore this this powerful feature of Scala with me.

      Thanks, Balaji!

  3. […] 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 […]

  4. marcinkubala says:

    This is one of the best posts that I read this year.
    Thank you!

  5. […] definitions by creating a Peano-encoded integer type. While that and the Boolean type we created in the first post were intriguing, but I haven’t demonstrated the utility of such types. In this post, I will […]

  6. […] what about all of those interesting operations we defined on BoolType and SizeType (originally named PeanoType)? Were those just for show, but otherwise useless? Well it […]

  7. […] a project built with Scala, I have a long ways to go before achieving mastery. I’m just now exploring the type system for that matter. It may be true that new comers can become productive in a few weeks, the paradigm […]

  8. […] today I was able to finally give the presentation-version of my recent exploration into type-level programming in Scala at HuntFunc. Writing my presentation with impress.js is the other distraction from blogging I […]

  9. […] case you haven’t noticed, I’m interested in type programming. If this was the Scala type system, I’d be stoked off the chart. The Java type system will […]

  10. […] Un exemple de programmation avancée par typage: http://proseand.co.nz/2014/02/17/type-programming-shifting-from-values-to-types/ […]

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 706 other followers

%d bloggers like this: