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.
Just FYI, your slides link is giving me a 404.
ReplyDeleteThanks a lot, I'll see to it asap.
Deletewonderful video! how about making the source code available?
ReplyDeleteThank 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.
DeleteExcellent presentation. It would be great to see more videos.
ReplyDeleteThank you so much. I'm looking forward to publishing some more stuff in the near future.
DeleteNice presentation: very clearly explained :-)
ReplyDeleteWell, thank *you* for providing us with shapeless ;-)
Deleteat 25:24 you said a + b' = a' + b, but why this doesn't work in the opposite way (a' + b = a + b')?
ReplyDeletefor 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] {} }
You'd have to change the base case as well, that should do the trick.
Delete