Become a Better Haskeller by Learning About Inductive Types

In the functional programming world, we rely on languages with type systems that help us write, extend and maintain our software. These type systems, such as the one in Haskell, are based on solid type theory. While we usually and easily see the benefits of having a static type system on simple types such as integers, we might fail to see the benefits of applying the same principles to user-defined data types. Continue reading

Giving a Talk on Propositions as Types

On Tuesday, March 26, I’ll be giving a talk on propositions as types to the Lambda Zagreb Meetup group. The talk will be in Croatian and it is titled ¬ sve za ∀ (no ∃ uvod u propozicije kao tipove), which can be translated as ¬ everything is for ∀ (but there ∃ an introduction to propositions as types). Obviously, I incorporated logic operators into the title with the goal to make it catchy and to attract more audience with an unusual title. Given that only about 10 people RSVPed so far and that there are only three days left until the talk, it looks like I’ve achieved quite the opposite!

Continue reading

Insisting on a Three-valued Boolean Type

If your program can have only two legal states, what sense does it make to extend a Boolean type with a third data constructor to account for the possibility of an “illegal program state”? Use a coproduct type with a Boolean type on the right instead. Make illegal program states irrepresentable in your types. I’m baffled by folks that insist on having their three-valued Boolean type.

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

Gave a Talk on Function Totality

As announced last week, yesterday I gave a talk on function totality at the Institute of Electrical and Electronics Engineers, Croatian Section. The talk was located at the University of Zagreb at the Faculty of Electrical Engineering and Computing. Slides used during the talk are freely available. The talk was in Croatian.

Continue reading