[mostly of interest to myself as a future reference]

I set myself a goal of learning how programming languages work this year, and to use exercise as an excuse to write Idris. Here’s what I’ve been up to so far.

Started off with this python tutorial on how to interpret a simple imperative language. Got a bit stuck on the meaning of a lot of basic terms (expression, term, factor…) so checked out this tutorial on basic maths terms.

The python tutorial uses parser combinators for parsing, and I wasn’t sure how they worked. I learned a good bit by going through the start of this paper on monadic parser combinators.

After that I took a step back from the python tutorial and implemented a calculator by copying this repo. That made a bunch of things about expressions start to make sense, so I got brave and ported haskell’s buildExpressionParser to Idris. Can see it here.

With that under my belt I went back and finished parsing the imperative language, with the help of this Haskell tutorial, the results are up here.

That was mostly parsing, and there’s a few more fun steps in how programming languages work, like type checking and evaluation. Still shaky on these areas, but as of the end of February I’m starting to explore them via lambda calculus.

Had a good talk with an old friend who knows this stuff, and he gave me a whirlwind tour of untyped, simply typed and dependently typed lambda calculus, along with using the dhall typechecker for examples. I should write up this talk sometime, was really helpful.

I’ve started reading pu on David Christiansen’s and Andras Kovaks’ work on typechecking/normalisation. So far I have copied this parser/evaluator for untyped lambda calculus. I’ve used it to play with arithmetic and Boolean logic, so I can get a better handle on lambda calculus in general.

Currently working on explicitly writing out a few lambda calculus substitutions, much as they do in the middle of this post. Just posted some boolean expansions, will do some arithmetic ones soon.

Once I get that down, next stop is the typechecker from elaboration zoo. This has given me a bit of a goal to aim for with all this, but more on that later.