Variable-arity polymorphism from scratch in Scala, Part II: Type-level computation, HList, KList

(Disclaimer, once again: much of this code is shamelessly stolen from the truly mind-blowing series of blog articles over at Apocalisp. Also, the main thrust of this blog post requires very little in the way of type-level computation – go figure.)

So, in the last installment we talked about how type constructors are functions, and higher-kinded types are higher-order functions, and then I said a whole bunch of other stuff, too. The important part was that type constructors are functions. The corollary of that  is that type-checking involves evaluation, and thus computation, on the level of types.

In fact, it turns out that adding higher-kinded types to even the most basic type system requires embedding the entire simply-typed lambda calculus into the type system. The simply-typed LC is a mathematical language for computation and while it’s not Turing-complete (thankfully, otherwise the type checker might not terminate), it’s remarkably expressive. As an aside, I thought I heard that due to nasty interactions with subtyping, recursive types, and all-around bad-assery, the core Scala type checking algorithm is in fact not guaranteed to terminate (they of course practically get around this in prodction by adding a fixed limit to recursion depth or some such mechanism).

Anyhow, cool, we have the ability to perform computations in the type system (as a matter of fact, we already had that due to bounded quantification and recursive types, but I don’t understand exactly how much power that buys you (gotta be at least Peano arithmetic) and how it compares). To that end, check out this cool thingie we can build without using any higher kinds:

  sealed trait HList { }

  final case class HCons[H, T <: HList](head : H, tail : T) extends HList

  case class HNil extends HList

  object HNil extends HNil

  val hl = HCons(1, HCons("asdq", HCons(3, HNil)))
  val a : Int = hl.head
  val b : String = hl.tail.head
  val c : Int = hl.tail.tail.head

An HList is a type and data structure for heterogeneous lists. It’s sort of like an extensible tuple – it permits any length but keeps all the type information of each node. You can see it basically does its consing at the type level as well as the term level, increasing the number of *‘s in the kind as it builds the list. This is an example of the tremendous power of bounded quantification, it’s all done without appealing to any “magic” Scala features. It uses case classes for simplicity, but you can actually build these in Java – it’s just completely insane because you have to write out the types by hand. (Note: I did a little checking and it turns out the secret ingredient here, allowing a type constructor to appear in the bound of its own variable, has a special name – F-bounded polymorphism)

We can even add a neat little infix type shorthand for both the type and the constructor HCons:

  final case class HCons[H, T <: HList](head : H, tail : T) extends HList {
    def :+:[T](v : T) = HCons(v, this)

  case class HNil extends HList {
    def :+:[T](v : T) = HCons(v, this)

  type :+:[H, T <: HList] = HCons[H, T]
  val :+: = HCons

  val hl = 1 :+: "asdq" :+: 3 :+: HNil

So, what is the point of this? Well, HLists are a key ingredient in the variable-arity polymorphism which is the namesake of this blog post. That’s right, there is an actual point to this.

Well after HLists, there’s something called a KList. The motivation is thus – HLists are well and good, but they don’t let me exploit any shared properties between elements of the list. For example, maybe the elements all have different element types, but they’re all Lists. This comes up a lot – for example, in Typed Racket, the creator’s decision to include a mechanism for variable-arity polymorphism was mainly to support functions such as map and fold over variable numbers of lists. These functions are often called map2, map3, map4, etc. or zipWith, and the key element is application of some single-argument type constructor (that is, a constructor of kind * -> *) to a list of types. So, the KList consists of a pair: a type constructor of kind * -> *, and an HList. You could thus store a variable-length, heterogeneous list of List‘s and have a suitable input type for your variable-arity map function.

  sealed trait KList[+M[_], HL <: HList]

  final case class KCons[H, T <: HList, +M[_]](head: M[H], tail: KList[M, T])
    extends KList[M, H :+: T] {
    def :^: [N[X] >: M[X], G](g: N[G]) = KCons(g, this)

  sealed case class KNil extends KList[Nothing, HNil] {
    def :^: [M[_], H](h: M[H]) = KCons(h, this)

  object KNil extends KNil

  val :^: = KCons

  val (m : KList[List, (Int :+: String :+: HNil)]) =
    List(1, 2, 3, 4) :^: List("str1", "str2") :^: KNil

You can see from the type of m (annotation provided for checking purposes, it is optional and inferred by the compiler), that the KList type is doing its job – the List type is separate from the element types. Cool!

Oh also, there’s probably a bunch of crazy stuff that requires explaining up in that there definition there. The +M[_] means its covariant in the type constructor argument. The N[X] >: M[X] means it’s allowed to get less specific in the type constructor argument as it builds up the list (this makes sense). Also note that the way HCons (a.k.a. :+:) is used in the KCons type, and HNil in the KNil type, means that it’s impossible to build a KList with a different number of elements than its associated HList. Very cool.

Ok, so now we have the KList, what do we do with it? Let’s try making that variable-arity map from earlier. We know it’ll take a KList with constructor type List, and to operate on the HList of argument types it will need to take a function that operates on HLists. The type should look something like:

  def mapN[HL <: HList, T](kl : KList[List, HL])(f : HL => T) : List[T]

So now we can actually express the type of a variable-arity, variable-type, polymorphic map function like in Typed Racket – but we built it ourselves! In fact, TR’s dotted type variables seem very much like KLists – they abstract part of their type-definition and apply it to a variable-length list of type arguments. Look at the type-signature for TR’s map:

  (: map
     (All (C A B ...)
          ((A B ... B -> C) (Listof A) (Listof B) ... B
           (Listof C))))

Looking at it through what we know about KLists, it’s like TR turns the “dotted type” into a single-argument type constructor ((Listof B) parametrized by B, which gives the Listof constructor), and create a KList using that and the type list (B). This is exactly what we’re doing with our mapN definition. Of course TR’s version is limited in power and first-class in the type system, which has the advantage of nicer syntax, and not requiring full higher-kinded types to implement, which results in much less type system complexity. On the other hand… we built it ourselves! Wow!

We have left one thing out up until now, which is the actual implementation of the mapN function. I guess technically it counts as cheating unless we do.

The main challenge is to find a way to get the values out of the lists. By that, I mean – fundamentally, the KList is built from values of type List[T] – we’re attempting to apply a function that requires individual elements. It is not, in general, possible to construct a function C[T] => T for every type constructor C. If it was, things like the Haskell IO monad wouldn’t work – effects would be able to escape into the rest of the code. There’s a cool concept underlying this, called natural transformations, (covered in the Apocalisp articles), but I’m going to save that for next time. Right now let’s just get the values out of the Lists the old fashioned way – pattern matching:

def heads[HL <: HList] : (KList[List,  HL] => HL) = {
  case KCons((hd :: _), tail) => HCons(hd, heads(tail))
  case KNil => HNil

def tails[HL <: HList] : (KList[List,  HL] => KList[List,  HL]) = {
  case KCons((_ :: tl), tail) => KCons(tl, tails(tail))
  case KNil => KNil

def toList : (KList[List, _] => List[List[Any]]) = {
  case KCons(hd, tl) => hd :: toList(tl)
  case KNil => List.empty

def anyEmpty(kl : KList[List, _]) : Boolean = toList(kl).exists(_.isEmpty)

def mapN[HL <: HList, T](kl : KList[List, HL])(f : HL => T) : List[T] =
       f(heads(kl)) :: mapN(tails(kl))(f)

Keep in mind that those match cases are not exhaustive because I know we’re pre-checking the KList for any empty components. We write it in curried style so that Scala can infer the type of later arguments from earlier ones. When tested, our mapN does what we expect it to do:

val m = List(1, 2, 3, 4) :^: List("str1", "str2") :^: KNil
println(mapN(m){ case (intVal :+: strVal :+: _) => intVal.toString() + strVal })

It prints “List(1str1, 2str2)”.

So, we’ve succeeded in implementing the nasty mapN function and proving that we can construct variable-arity polymorphism in Scala. With a little syntactic sugar (why can’t Scala have macros!?) this would be a pretty reasonable foundation for a language feature.

What we’ll show next time is that there’s a broader concept hidden under all the digging around for heads and tails that we were doing in the implementation of mapN – It doesn’t have to be this ugly. It can be easy, and, well, natural.

(In progress. Come back later.)

About these ads

One Response to Variable-arity polymorphism from scratch in Scala, Part II: Type-level computation, HList, KList

  1. [...] as “the mother of all HList implementations.” If you’ll remember, I did a post on using HLists to kinda-sorta simulate variable-arity polymorphism, as a followup to my very frist psot using Typed Racket’s variable-arity features to make a [...]

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your 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.

%d bloggers like this: