ionchy/system-f-redex
1
0
Fork 0
Code Issues Pull requests Activity
Church-style System F with definitions in Redex.
59 commits 1 branch 0 tags 105 KiB
  • Racket 100%
Find a file
Exact
Jonathan Chan 22c56450e3 An independent attempt at adding inductive types to System F.
2020-10-15 20:41:01 -07:00
.gitignore Several changes: 2020-05-07 20:16:52 -07:00
acc.rkt Added booleans to F-ACC and ACC. 2020-05-15 13:15:05 -07:00
anf-naive.rkt Copy ANF translation to naive file; the improved version will be in the original anf file. 2020-05-14 15:39:35 -07:00
anf.rkt Changed ANF to use a join point when compiling if expressions. ANF translation now occurs over a typing judgement. 2020-05-15 12:16:18 -07:00
hoisting.rkt Added booleans to F-H and hoisting. However, the typing rules are currently incorrect, since it assumes that code blocks never refer to lables of other code blocks. 2020-05-15 14:08:04 -07:00
README.md Fixed typing in F-H. 2020-05-15 18:37:13 -07:00
redex-chk.rkt Finished implementation of reduction in System F-ACC. Still needs tests though. 2020-04-27 22:01:42 -07:00
reductions.rkt Added a list of reduction strategies. 2020-04-29 17:13:47 -07:00
system-f-acc.rkt Added booleans to F-ACC and ACC. 2020-05-15 13:15:05 -07:00
system-f-anf.rkt Added booleans to F-ACC and ACC. 2020-05-15 13:15:05 -07:00
system-f-h.rkt Fixed typing in F-H. 2020-05-15 18:37:13 -07:00
system-f-ind.rkt An independent attempt at adding inductive types to System F. 2020-10-15 20:41:01 -07:00
system-f-omega.rkt Moved redex-judgement-equals-chk to redex-chk; use custom redex-chk instead. 2020-04-27 21:45:07 -07:00
system-f.rkt Added booleans to F-ACC and ACC. 2020-05-15 13:15:05 -07:00

README.md

System F in Redex

This is an implementation of a Church-style (explicitly typed-annotated) System F (polymorphic) lambda calculus with definitions (let-expressions) and branching (booleans) in Redex. Included are:

System F

  • Type synthesis, CBV small-step semantics
  • Church encodings of numerals and some arithmetic

ANF-Restricted System F

  • Type synthesis, CBV small-step semantics
  • Uses Redex's in-hole contexts for continuations used during compilation
  • Compiler from System F to ANF-restricted System F (defined with an ambient continuation)
    • The naïve version copies the continuation twice when compiling if expressions
    • The improved version is defined over System F's typing rules and avoids code copying

(ANF-Restricted) System F with Closures

  • Type synthesis, CBV small-step semantics that evaluate closures during application
  • Compiler from ANF-restricted System F to closure-converted System F (defined over System F-ANF's typing rules)

(ANF-Restricted) Hoisted System F (with Closures)

  • Type synthesis, CBV big-step semantics (implemented as a judgement rather than a reduction-relation)
  • Compiler from closure-converted System F to hoisted System F
  • N.B. Each code block label is only visible in subsequent code blocks

System Fω (extends System F)

  • Why? I don't know.
  • Higher-kinded polymorphic lambda calculus with NO let-expressions
  • Type synthesis, term evaluation, type evaluation

redex-chk, but Better

  • Renames judgment to judgement
  • Adds redex-judgement-equals-chk to test for equivalence between judgement output term and a provided term

Reduction Strategies

  • This doesn't belong here

TODOs

  • Consider adding fixpoints (this might be of interest for ACC... or not)
  • Add inventory of metafunctions and how to run things to this README
  • Fix redex-judgement-equals-chk macro so that when check-true fails, the highlight goes over the failed branch, not over the macro itself (redex-chk)
  • Consider a heap allocation pass. This is primarily to concretize what a closure would look like at low level. I'm guessing the free types and terms would each be an array.