The goal of this project is to experiment with frames, i.e. records with some fields left empty, as the basis of an untyped (for now) programming language. See https://xavier.montillet.ac/talks/TYPES-2019/ for an explanation of why frames are useful in a dependently typed setting.
The code is split into three libs:
-
mypl contains my experiments with frames.
-
modular-calculi allows combining independent calculi, and in particular adding integers to a candidate frame calculus to make testing it easier. It is slightly overengineered, mainly because I wanted to have fun with GADTs and primitive modules.
-
mycore contains things that I would have liked to find in Janestreet's Core library.
Questions I would like to eventually provide an answer to are:
-
How efficiently can frames be implemented? Is hash-consing necessary? Are co-de-Bruijn indices relevant?
-
What can frames simulate? In particular, can a call-by-value variant of frames be used to simulate pattern-matching (somewhat efficiently)?