Isomorphism and Embedding

To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.

Continue reading

Haskell Library Demonstrating Dependent Types in eDSL

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.

Continue reading