Dependent types: formal definition and examples

Dependent types have been gaining a lot of attention among programmers. Some would say it’s “the next thing” in programming. Why is it gaining popularity? In this post, I hope to show some of the advantages of dependent types and get you started on programming in dependent types. To understand…

Programming with Envelopes in OCaml and Haskell

In this post, I continue going through the famous paper “Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire” by Meijer et al.  They show that we can treat recursions as separate higher order functions known as recursion schemes.  Each of the four things in the paper title corresponds to…

Using Unfolds to Iterate in Haskell and OCaml

This post picks up from where we left off here, in which I explained anamorphisms.  Here we look at another example of applying unfolds: iterate.  Iterate Iterate is one of the most common uses of unfold.  The definition of the iterate function is: iterate f x = Cons (x, iterate…

Why Blockchain Engineers Should Learn Functional Programming

As a software engineer who wants to work with blockchains, you may ask: what languages should I learn?  Answers on the internet (e.g., here, here, and here) mostly recommend prominent languages like C++, Python, Java, and Javascript, and the smart contract language Solidity.  None of them mention any functional languages! …

Programming with Lenses in Haskell and OCaml

In this post, I continue going through the famous paper “Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire” by Meijer et al.  They show that we can treat recursions as separate higher order functions known as recursion schemes.  Each of the four things in the paper title corresponds to…

Eliminating Run Time Errors In OCaml and Haskell

Run Time Versus Compile Time Error Run time errors are those that happen when the program runs, as opposed to compile time errors which happen when the program compiles.  In a sense, having compile time errors is no big deal, because the errors guarantee that the ill-defined program won’t be…