Programming at the type level

[jducoeur]

In my continuing explorations of functional and higher-order programming, I just came across the Up Library, and the series of blog posts that motivate it. This is *wild* stuff, and helps explain some of the strangenesses in Scalaz. Basically, it starts with a demonstration that Scala's type system is, itself, a full programming language, and then goes to town with it. It starts out seeming like wankery, but it's worth pushing through the series, which eventually gets around to building up concepts like HLists -- arbitrarily heterogeneous, yet completely type-safe, lists. (And thence KLists -- lists of items that share a higher-order Kind: for instance, a List of Lists, where the subsidiary lists have different object types, but you still want to be able to treat them as Lists.)

Brain-breaking stuff, and it's going to take me a while to fully internalize it, but the potential in these examples is clear: if you're willing to get into it, you can push the Scala type system *way* beyond what you would normally expect. This allows you to do things that you'd kind of intuitively *like* to be able to do with complex data structures, but are normally prevented by the type system. He does call out limitations of the Scala type system (and freely admit that he is abusing the system mercilessly), but it's an excellent series for pushing the boundaries of your assumptions about what's possible...

Comments

[laurion]

Whoa. Sounds like it lands on the 'bend things to do what -you- want them to do' square. Playing with fire, yes, but Prometheus gave us that for a reason...

[alexx-kay.livejournal.com]

Last time I counted, the game egine I use at work exposes to the Designers *three* different Turing-complete systems. A fourth almost emerged, but I think I've stymied it for the time being...

[jducoeur]

There's a fair amount of value in that, of course -- knowing that you can build arbitrarily insane simulations at the design layer is kind of neat. (Although, admittedly, it does sometimes tend to make for hard-to-test games.)

The neat thing here is the meta-layer: having a Turing-complete language on *top* of another Turing-complete language. That's where the true brain-breakingness comes in. The Up examples mix stuff that's happening in the compiler with stuff happening at runtime so freely that it's downright scary...

[alexx-kay.livejournal.com]

We don't quite have that, as the Programmers guard their level jealously. On the other hand, each of those three systems I mentioned has hooks to communicate with the other two, so we have quite a lot of *sideways* wackiness going on :)