Archon

An experimental language that tries to combine dependent type, lexical algebraic effects & handlers, and quantitative types.

Design

Overall the core type theory is a mixture of

• EMLTT of Danel Ahman
• Effect instance of Dariusz Biernacki et al.
• A specialized graded modal dependent type theory of Andras et al.

The type checker supports meta variable and unification is implemented based on the Agda paper by Norell.

On top of that, inductive type and co-pattern matching is implemented based on Elaborating dependent (co)pattern matching from Jesper Cockx et al.

For detailed design, one can check out term.scala for core type theory IR and typing.scala for the type checker.

Progress

✅ completed | 🚧 under construction | 💡 planned

• [🚧] Core type theory
  • [✅] IR
  • [🚧] Type checker
    • [✅] Normalization and conversion
    • [✅] Subtyping
    • [✅] Meta variable unification
    • [✅] Escape analysis to detect effect instance leak
    • [💡] Totality checker
    • [💡] Proof searcher
    • [💡] Nominal subtyping of records and effects
  • [✅] Function elaboration
• [🚧] Low-level IR
  • [🚧] LIR (Archon VM) - need to adopt lexical effects
  • [💡] IR -> LIR lowering
  • [💡] Primitives
• [💡] Frontend IR (User language)
  • [💡] Mix-fix parser
  • [💡] FIR -> IR lowering
    • [💡] Type class via record and proof search
    • [💡] Type-driven resolution? (likely limited to only certain heuristics)
• [💡] Standard library