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.

Advertisements

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 πŸ™‚