Screams into the Void

The Implementation of Functional Programming Languages Chapter 5

February 13, 2019

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

February 10, 2019

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

February 9, 2019

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.

Lectures on the Curry-Howard Isomorphism Chapter 2 (1/3)

February 8, 2019

Read a third of Chapter 2. It was less dry! For Natural Deduction they define the context as a set, so they did not need to discuss a permutation theorem. They did mention the substitution theorem. They next part of the chapter will talk about algebraic semantics and Heyting algebras, so that should be fun as well. Pretty excited about returning to some of the material from my Universal Algebra course.

Thoughts on WebAssembly

February 7, 2019

WebAssembly does not feel like an assembly language and there does not seem to be any plans to make it more like one. I feel that functional languages will always have a second class status on the web because we don’t have access to enough low level primitives to add our own garbage collectors.

Reference Counting

February 7, 2019

There seem to be several ways of thinking about reference counting. One is actual counts. Another way to think about the reference count is as an approximation to some kind of a remembered set.

Compiling without Continuations

February 6, 2019

Recently read the “Compiling without Continuations” paper for the nth time. Was still a fun read! I really like the IR in that paper – it’s simple and cute. Personally, I think join points are useful if exposed to the user.

Lectures on the Curry-Howard Isomorphism Chapter 1

February 3, 2019

Read the first chapter of “Lectures on the Curry-Howard Isomorphism”. It was a very technical introduction to the untyped lambda calculus. Although the theory seems very robust, it was somewhat dry. The book was recommended to me by someone who held it in high regard, so I think the later chapters will be more exciting.