Tuesday, February 21, 2012

Type-level programming

Some time ago I became interested in type-level programming in Scala. Subsequently I've spent quite some time surfing the web and looking for nice examples, projects, blog posts, discussions on SO, and more stuff like that.

Turns out there's a vast amount of information out there. However, it's spread all over the net. Hence I've created the following demo on basic type-level programming which aims at summing up the introductory steps. At this point, major thanks to Miles Sabin and Mark Harrah for sharing shapeless and/or their elaborate blog posts.

Apart from some explanatory slides the demo shows how to implement a type-level representation for natural numbers and arithmetics because that seemed to be an appropriate topic and, in case people were interested, they could easily find more information on the net.

You can download the slides here, and the full video is available here. Get the source code here.

Errata

  • When I checked the video I realised there's one major semantic "mischief" at or around time 15:35 where I said "successor of any other number" but really meant "successor of some other number" instead.

Please let me know if you happen to find any mistakes so that I can list them here.

10 comments:

  1. Just FYI, your slides link is giving me a 404.

    ReplyDelete
  2. wonderful video! how about making the source code available?

    ReplyDelete
    Replies
    1. Thank you very much for your kind words! And you're right, of course. How could I forget? I'll make the source available once I get home from work.

      Delete
  3. Excellent presentation. It would be great to see more videos.

    ReplyDelete
    Replies
    1. Thank you so much. I'm looking forward to publishing some more stuff in the near future.

      Delete
  4. Nice presentation: very clearly explained :-)

    ReplyDelete
    Replies
    1. Well, thank *you* for providing us with shapeless ;-)

      Delete
  5. at 25:24 you said a + b' = a' + b, but why this doesn't work in the opposite way (a' + b = a + b')?

    for example this works:
    implicit def sumN[A <: Nat, B <: Nat, C <: Nat](implicit ev: SumAux[Succ[A], B, C]) = new SumAux[A, Succ[B], C] {}

    this doesn't work:
    implicit def sumN[A <: Nat, B <: Nat, C <: Nat] (implicit ev: SumAux[A, Succ[B], C]) = new SumAux[Succ[A], B, C] {} }

    ReplyDelete
    Replies
    1. You'd have to change the base case as well, that should do the trick.

      Delete