Re-inventing the Monad wheel

Lately, I spent some time working on one of my Haskell projects: hoare-imp. It is basically an implementation of propositional calculus+first-order logic+number theory (Peano)+Hoare logic, and allows one to reason about computer programs, producing Hoare triples. The source code of this implementation is at around 600 LoC at this moment.

I will explain how I re-implemented a monad, and even used it without knowing about it. And I am sure you have done the same, at some point, too!

Algorithmic puzzle: Continuous Increasing Subsequences

In this blog post, we’ll tackle the following puzzle:

Given an array of integers, count the number of continuous subsequences, such that elements of every subsequence are arranged in strictly increasing order.

The optimal solution to this puzzle is to use the dynamic programming (DP) technique. But, in order to apply this technique, we first need to express the solution through a recurrent formula. So, I will start first by expressing it in Haskell, and then translate the implementation to PHP.

Capturing Number Theory in Haskell

In Chapter VII of GEB, the author gives a description of Gentzen’s Propositional Calculus, along with some examples of applying its rules, and in Chapter VIII, the author gives a description of TNT (Typographical Number Theory).

In this post we’ll provide an implementation of these systems in Haskell.

Performant implementation of pagination on Cartesian products

In this post we’ll tackle the following puzzle:

We are given two arrays, one with adjectives and another one with nouns . A combined list is which is the Cartesian product between the two arrays. We want to build a performant way to get specific a subarray of of arbitrary size at a specific page.

Towards Hoare logic for a small imperative language in Haskell

Recently I finished Logical Foundations, and I have to admit it was an excellent read. This post is directly inspired by the Simple Imperative Programs section of the same book.

What is an imperative programming language? Well, nowadays they run the world. C, Python, JavaScript, PHP – you name it – we all write code in them using imperative style; that is, we command the computer and tell it what to do and how to do it. The mathematical language is very unlike this – it is more declarative rather than imperative – it doesn’t care about the how.

I’ve always been fascinated by mathematical proofs, especially the mechanical part around them because computers are directly involved in this case. Hoare logic is one of those systems that allows us to mechanically reason about computer programs.

We will implement a small imperative language together with (a very simple) Hoare Logic that will allow us to reason about programs in this imperative language.