(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, `HList`

s 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 `HList`

s, there’s something called a `KList`

. The motivation is thus – `HList`

s 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 `List`

s. 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 `HList`

s. 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 `KList`

s – 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 `KList`

s, 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 `List`

s 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] = if(anyEmpty(kl)) List.empty else 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.)

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