| (** Core Types *) | |
| module Syntax = | |
| struct | |
| type t = | |
| | Local of int | |
| | Hole of string | |
| | Let of string * t * t | |
| | Lam of string * t | |
| | Ap of t * t | |
| | Pair of t * t |
On September 28, 2021, I asked on Twitter:
PL Twitter:
you get to recommend one published PL paper for an undergrad to read with oversight by someone experienced. the paper should be interesting, approachable, and (mostly) self-contained.
what paper do you recommend?
If you want to see how it works, see the README on the repo.
When first reading programming language papers, it can be challenging to figure out how to translate the notation into working implementations. The following post is intended to help show how these rules correspond to working implementations in Prolog, OCaml, and Lean, for a very simple language of arithmetic expressions.
T ::=
| Int
| Bool
| {-# language Strict, LambdaCase, BlockArguments #-} | |
| {-# options_ghc -Wincomplete-patterns #-} | |
| {- | |
| Minimal demo of "glued" evaluation in the style of Olle Fredriksson: | |
| https://github.com/ollef/sixty | |
| The main idea is that during elaboration, we need different evaluation |