Day 4: Exhaustion
Our goal is to show once and for all that, contrary to popular belief (even among experts in the field!), the semantics of ML modules is immediately accessible to anyone familiar with System Fω, the higher-order polymorphic λ-calculus.
…
ML modules are merely a particular mode of use of System Fω. (Rossberg, Russo, and Dreyer 2010)
Vibe
Tuckered out and feeling a bit numb. I need to turtle a bit tomorrow and recover from all the lovely (but quite intense) social engagement.
Today’s Progress
Due to over-extending myself over the last three days, I wasn’t able to stay on task with my planned goals today. I did manage to make some meaningful progress however.
By the third page of (Rossberg, Russo, and Dreyer 2010) (the epigraph to this entry) is was clear that I would need improve my graphs of System Fω in order to work effectively on 1Ml. This has motivated me to see through ongoing studies into typed lambda calculi, and push forward quickly until I have covered the left face of the lambda cube:
PLT: Type Theory
I spent some time working on the menhir parser-generator for my WIP experiments in typed lambda calculi, themis. For a long while I’ve been stuck on a shift/reduce ambiguity arising from this grammar rule:
term: /* ... */ | m = term; n = term { Term.app m n} /* ... */
This rule is meant to say that any two juxtaposed terms are to be parsed as
function application. However, due to the necessarily recursive definition of
terms and the lack of an operator to use for indicating precedence of grouping,
menhir doesn’t know if a sequence such as l m n should be parsed into the
correct left-associative expression Term.app((Term.app l m) n) or the
incorrect, right associative Term.app(l Term.app(m n)).
I finally came across a resource that described a solution to a similar problem (also in a lambda calculus interpreter, but with different syntax). What we want is a way to clearly instruct the parser generator that term application should be left-associative. To achieve this, we restructure the rule to ensure that the parser is left-recursive on the first term of the application:
terms: | m = terms; n = term { Term.app m n } | t = term; { t } term: /* singular terms here */
Category theory
- CT reading group: folks presented motivating reasons behind their desires to learn Category Theory.
Writing
- Created a yas snippet to generate the template for these logs. Getting savy with yas snippets should improve the speed and quality of writing and code in general.
Tomorrow’s Program
PLT: 1ML × Type Theory
- Study and take notes on the distinction between small and large types in 1ML
- Continue reading (Rossberg, Russo, and Dreyer 2010)
- Begin working on tuple type-checking error
- Begin trying to fix the biggest type-checking bug I found today
- Finish parser for λ⟶
Writing
- Write up implementation of stack
- Write up notes on small vs. large types