TTstar

Dependently typed core calculus with erasure inference.

Examples from the dissertation

• Palindrome (source, erased)
• Binary adder (source, erased)
• RLE (source, erased)
• Scope-indexed lambda calculus (source, erased)
• Other example programs and their outputs

Features

Erasure

• erasure inference (fills in erasure annotations)
• separate erasure checker (verifies consistency of inferred annotations)
• erasure from higher-order functions
• complete removal of unused arguments (rather than passing in NULL)
• erasure polymorphism for functions
• four constraint solvers
  • simple and straightforward O(n²) solver
  • graph-based constraint solver
  • indexing solver (fastest, default)
  • LMS solver
    • "last man standing"
    • Adapted from "Chaff: Engineering an efficient SAT solver" by Moskewicz et al., 2001.
    • theoretically faster than the indexer, my implementation is slower
• a tentative implementation of irrelevance (example)

Language

• full dependent pattern matching clauses
• pattern matching local let definitions are useful for emulating
  • case expressions
  • with clauses
  • mutual recursion
• rudimentary term/type inference via first order unification

Practicalities

• type errors come with backtraces
• rudimentary FFI via foreign postulates
• a simplified intermediate representation for backends (IR)
  • translation from TT to IR compiles patterns into case trees
• native code generators
  • a codegen from TT: via Scheme (Chicken Scheme or Racket)
    • uses the matchable extension
  • a codegen from IR: produces standard Scheme
    • mostly R5RS-compliant
      • except that some programs redefine the same name repeatedly in let*
    • when interpreted with csi, the IR-generated code runs much (~3x) faster than the TT-generated code
    • only about 10% faster than TT-generated code when compiled using csc
  • a codegen via Malfunction, using IR
    • produces fast native code

Other stuff

• dependent erasure (if x == 3 then erased else not_erased)
• unused functions are removed entirely
• Refl is always erased
• Maybe sometimes becomes Boolean after erasure

Does not feature

• totality checking
• mutual recursion
  • a restricted form is easy to achieve using local let bindings
  • sufficient in all cases I've come across
• much syntax sugar