# Dependently Typed Lambda Calculus in Haskell

I found this awesome paper “A tutorial implementation of a dependently typed lambda calculus“, by Löh, A., C. McBride, W. Swierstra and I decided to give it a go.

I read the paper a few times. The first time when I did it, it was just skimming through, copying and pasting the code as I go. Then, after doing the examples and playing with them for a bit, I read it again thoroughly to try to understand the mathematical definitions and the corresponding Haskell definitions and how they map to each other.

As I was implementing the code, I made sure to make a Git tag of every chapter implementation. This made it easier to match code to its mathematical definitions in the paper for the corresponding chapter.

Besides my interest in dependent types, I also noted this learning process was interesting, thus this blog post 🙂

Even though papers take some time to read and digest, I highly recommend this paper to anyone interested in diving deeper into dependent types.

You can check the source code at https://github.com/bor0/lambdapi.

Bonus: Had some fun implementing TAPL exercise 3.2.4 in literate Haskell here.

# Proving Monoids with Idris

I was watching an interesting video, Opening Keynote by Edward Kmett at Lambda World 2018. Note in the beginning of that video how in Haskell you’d put code comments in place of proofs.

Enter Idris.

As a short example, we can abstract a proven Monoid as an interface:

interface ProvenMonoid m where
mappend : m -> m -> m
mempty  : m
assocProof : (a, b, c : m) -> mappend a (mappend b c) = mappend (mappend a b) c
idProofL   : (a : m) -> mappend mempty a = a
idProofR   : (a : m) -> mappend a mempty = a


Do Nats make a Monoid? Sure they do, and here’s the proof for that:

implementation ProvenMonoid Nat where
mappend x y = x + y
mempty      = 0

-- Proofs that this monoid is really a monoid.
assocProof  = plusAssociative
idProofL    = plusZeroLeftNeutral
idProofR    = plusZeroRightNeutral


Note that plusAssociative, plusZeroLeftNeutral, and plusZeroRightNeutral are already part of Idris’ prelude. In the next example we’ll do an actual proof ourselves instead of re-using existing proofs.

What about List of Nats? Yep.

implementation ProvenMonoid (List Nat) where
mappend x y = x ++ y
mempty      = []

-- Proofs that this monoid is really a monoid.
assocProof [] b c      = Refl
assocProof (a::as) b c = rewrite assocProof as b c in Refl
idProofL a             = Refl
idProofR []            = Refl
idProofR (x::xs)       = rewrite idProofR xs in Refl


Some valid questions are:

• Why should I care about monoids?
• Edward covers this in the video at around 3:00.
• Why should I care about proving monoids?
• Let’s assume that there’s an algorithm running in production that relies on Monoids. What we don’t want to happen is associativity to break, because if it does then the “combine” function applied on all of the produced results will likely be wrong.

🙂

EDIT: Updated first example per u/gallais’s comment.

# Partial orders in Idris

A binary relation $R$ is a partial order if the following properties are satisfied:

1. Reflexivity, i.e. $\forall a, a R a$
2. Transitivity, i.e. $\forall a, b, c, a R b \land b R c \to a R c$
3. Antisymmetry, i.e. $\forall a, b, a R b \land b R a \to a = b$

Let’s abstract this in Idris as an interface:

interface PartialOrder (a : Type) (Order : a -> a -> Type) | Order where
total proofReflexive     : Order n n
total proofTransitive    : Order n m -> Order m p -> Order n p
total proofAntisymmetric : Order n m -> Order m n -> n = m


The interface PartialOrder accepts a Type and a relation Order on it. Since the interface has more than two parameters, we specify that Order is a determining parameter (the parameter used to resolve the instance). Each function definition corresponds to the properties above.

This interface is too abstract as it is, so let’s build a concrete implementation for it:

implementation PartialOrder Nat LTE where
proofReflexive {n = Z}   = LTEZero
proofReflexive {n = S _} = LTESucc proofReflexive

proofTransitive LTEZero           _                 = LTEZero
proofTransitive (LTESucc n_lte_m) (LTESucc m_lte_p) = LTESucc (proofTransitive n_lte_m m_lte_p)

proofAntisymmetric LTEZero           LTEZero           = Refl
proofAntisymmetric (LTESucc n_lte_m) (LTESucc m_lte_n) = let IH = proofAntisymmetric n_lte_m m_lte_n in rewrite IH in Refl


Now you can go and tell your friends that the data type LTE on Nats makes a partial order 🙂