Dependent Types

I’ve been doing a fair amount of reading about dependent types recently, mainly because we have been working through the Idris book as a weekly lunchtime activity at work.

For a good article on the current state of play in Haskell, Richard Eisenberg’s thesis is very good – chapter 2 discusses a load of extensions of Haskell to enable type level programming. He also has a good series of blog posts on various Dependent Types aspects. There are a number of interesting YouTube videos too, including this one of using dependent types in a RegExp library.

At some level, the type checking becomes theorem proving. For the Idris language, there are slides from a talk on how this process happens, and there’s another phd thesis on type checking Haskell which discusses some of the trade offs.

While we are talking about type checking, there is a repository where the author is writing variants on Hindley-Milner type checking in F#. It’s a very interesting learning resource, as the examples are small enough to step in the debugger, so you can watch what happens when a let bound function is generalised by the system.

There’s always that interesting point between type checking and proof, and this github repository uses Idris to generate proofs about various Minesweeper boards.

This entry was posted in Uncategorized. Bookmark the permalink.

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 )

Google+ photo

You are commenting using your Google+ 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 )

Connecting to %s