| {-# 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 |
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
If you want to see how it works, see the README on the repo.
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?
| (** 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 |
