Just this morning these two books landed my mailbox:
The Littler Typer and Verified Functional Programming in Agda
The Little Typer is a new book on dependent type theory, written by Daniel P. Friedman, an author of The Little Schemer, and David Thrane Christiansen, an Idris contributor. Verified Functional Programming in Agda is a book by Aaron Stump, on using dependent types in Agda to prove various properties of programs. After having read the Type-driven Development with Idris book by Edwin Brady, I am hoping these two books will significantly expand my knowledge of and improve my skills in type theory, theorem proving and typed functional programming. Looking forward to reading the books! If you haven’t noticed by now, I got hooked on dependent types!
Haskell Servant’s logo
In Haskell, servant is a library for declaring web APIs. What is interesting about the library is that it utilises the power of Haskell’s type system, in particular the power of dependent types in computing a return type of a function.
On February 6 in Zagreb I’ll be giving a talk on the role of types in programming as part of the Lambda Zagreb group. It will be about pushing the domain into types. I’ll cover various topics, including dependent types and refinement types. An example that I’ll give and that will hopefully be most interesting is about encoding a state machine at the type level. This means that if you try to make an illegal state transition in the code, it won’t compile. My code snippets are going to be in Idris, but I’ll provide Haskell and Scala equivalents where applicable.
The talk is going to be in Croatian, but I’ll do my best to have the slide deck ready in English just in case.
Until today I wasn’t aware it is possible to do dependently-typed programming in Haskell. It turns out it is possible! This is amazing news for writing code with even less bugs. I would argue that dependent typing takes software verification in software engineering to the next level. The key feature that enables it in Haskell is singleton, a type that has only one inhabitant, i.e., exactly one value. Justin Le has a nice blog post about this topic and I highly recommend it! It is part 1 of a series so I’m looking forward to the rest of the series.
Liquid Haskell is an extension to Haskell to provide via logic what Idris has in its type system (via dependent types): a way to provide more precise properties to programs, including totality.
Idris is a pure functional programming language with dependent types. In this post I am giving an example by David Christiansen on proving a parity theorem (or property) in Idris. The theorem states that every natural number is either even or odd. The example below demonstrates how to do theorem proving with a functional programming language such as Idris. It relies on equality expressed at the type level, which is possible thanks to dependent types. With that, Idris stands in stark contrast to languages such as Scala, where equality is broken. In the example, allEvenOrOdd k is a proof for every natural number k.