astle dsa

NOTE: I am no subject matter expert and have chose to learn about this field through utilizing LLMs to guide me using practical implementations. Also, I am assuming a basic familiarity with Haskell and the Functional Programming paradigm. Our journey starts with the concept of lambda calculus and the existence of the Curry-Howard Correspondence. These concepts basically bridge the gap between Mathematics and Computer Science in a specific manner [1]. This gives rise to a very interesting piece of software: theorem provers, which is a beautiful combination of compiler design, type theory and mathematics, three of my favourite concepts ! There aren’t many blogs on writing theorem provers from scratch, hence I thought I would fill the gap up myself! Now, to be fair, there is this excellent essay on writing one from scratch from Federico Carrone, who implements a very simple one in Python. Taking his implementation as the base starting point, I proceeded to re-implement, before moving on to a slightly more expressive one, which utilizes Dependant Type Theory. I have extensively utilized LLMs to guide me (guide not code! Every line is hand-written by me) on creating the extended version, although at this stage, I do trust them to be excellent at this task (I must admit, it took some effort for me to get the LLMs to guide me in a manner that provided a smooth path to implement and understand the extended version). Without further ado, let’s jump in! Version 1 The first version is essentially a copy of Federico’s version, as I wanted to start from a very basic and minimalist version. The only difference was that I re-wrote it in Haskell: data Type = Atom String | Arrow Type Type deriving (Show, Eq) data Term = Var String | Lam String Type Term | App Term Term deriving (Show, Eq) type Context = [(String, Type)] search :: Context -> String -> Type search [] var = error ("unbound variable: " ++ var) search ((k,