Implementation of Functional Programming Languages Chapter 7

Finished reading “Chapter 6: List Comprehension”. Oh my god that was a good chapter! Always thought list comprehensions were a mere syntactic sugar, but having them as second class constructs open up some important optimizations.

The next two chapters are on type checking. Looking forward to them!

Implementation of Functional Programming Languages Chapter 6

Finished reading “Chapter 6: Transforming the Enriched Lambda Calculus”, and then immediately reread it. It discusses how to compile the lambda calculus enriched with pattern matching lambdas into the ordinary lambda calculus. Two schemes are discussed, compiling to a calculus with and without let bindings.

I had to reread it immediately because the first reading was done in too many sittings. One notable thing that I took away was the dependency checking section, which shows how to hoist independent definitions from recursive definitions.

The Implementation of Functional Programming Languages Chapter 5

Finished reading Chapter 5: Efficient Compilation of Pattern-matching. Some of the code presented will probably make more sense if I actually implement the functions. Other than my understanding of the code being a little fuzzy, I liked the chapter overall. In particular, I liked how all the transformation rules are explained separately at first and then combined together into the pattern-matching compiler. I really like this sort of explanation where the reader is presented with the simple ideas which can be understood in isolation, and then it is explained how different ideas are combined.

Lectures on the Curry-Howard Isomorphism Chapter 2

Finally finished reading chapter 2 of Sorensen and Urzyczyn. Was a good read overall. I was really looking forward to the Kripe semantics parts, but it seems that the more spicy parts are left as an exercise to the reader. I am not sure which exercises I want to do, but I plan to do at least some of them. The exercises also point out that consistency (which they define as not being able to prove bottom), is equivalent to there existing a formula which is not provable. I still don’t have a good intuition why these are equivalent.

Pierce's Law and an Interesting Lattice

I’m still reading through Chapter 2 of Sorensen and Urzyczyn (Lectures on the Curry-Howard Isomorphism). One thing that they pointed our earlier in the chapter is that Pierce’s Law ((p→q)→p) → p is purely implicational, but it is still not provable in intuitionistic logic. So it is not only the formulae which use negation which are different between the two logics. I had not really noticed that before.

I have also been thinking about bounded lattices which are not complete. An easy example of such a lattice is [0,1] ∩ ℚ. This is bounded by 0 and 1 but not complete – there is no greatest upper bound for the following: {{x} | x ∈ [0, 1/π) ∩ ℚ}. Sorensen and Urzyczyn provide the following as an example of a lattice which is a field of sets: {A ⊆ X | A finite or X − A finite}. This is also not complete when X is infinite. This is a little more interesting because it is not a totally ordered lattice.

Older   Newer