In this month’s episode of Functional Futures, our guest is David Christiansen – the Executive Director of the Haskell Foundation and the co-author of The Little Typer, a book on dependent types.
In the previous post, we briefly introduced the reader to dependently typed programming and theorem proving in Agda. Now we present an empty type to work with constructive negation. We discuss Marko…