Type Theory Forall - #37 Compilers, Staging, Futamura Projections (podcast)
(www.typetheoryforall.com)
from armchair_progamer@programming.dev to programming_languages@programming.dev on 12 Mar 2024 19:29
https://programming.dev/post/11368933
from armchair_progamer@programming.dev to programming_languages@programming.dev on 12 Mar 2024 19:29
https://programming.dev/post/11368933
It’s just one part, but the Futamura Projections] are techniques to “compile” interpreted programs using partial evaluation:
partialEval : (a : Function) -> a -- Specializes a partially-applied function: returns something with the same arity and semantics but faster interpret prog inp -- Runs the interpreter on a program with input
- The first futamura projection turns an interpreted program into a compiled one by “partially evaluating” (AKA “specializing”) the interpreter on the source code (e.g. hard-coding things that would remain constant during the code’s execution).
partialEval (interpret prog) inp
- The second futamura projection turns an interpreter into a compiler by partially-evaluating the partial evaluator on the interpreter.
partialEval (partialEval interpret) prog inp
- The third futamura projection partially-evaluates the partial-evaluator on itself, creating a “compiler compiler”: a function which takes an interpreter and returns a compiler, or more precisely, takes an interpreter and returns something that takes a program and returns a compiled program, or more precisely, takes an interpreter and returns something that takes a program and returns something that takes an input and produces the same output the original program would, but faster:
partialEval (partialEval partialEval) interpret prog inp
More detailed explanation. An example of this in practice is Truffle in GrallVM.
threaded - newest
Good summary. A couple notes before I listen:
mix
, particularly in The Book and also a few important papers like Glück 2009. This also extends to project nomenclature; “Logimix” for Prolog or “Similix” for Scheme are both based onmix
.