Skip to content
/ ttstar Public

Dependently typed core calculus with erasure

License

Notifications You must be signed in to change notification settings

ziman/ttstar

Repository files navigation

TTstar

Dependently typed core calculus with erasure inference.

Examples from the dissertation

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