roadmap.md

Roadmap

Language features

• top-level items
• recursive definitions
• let expressions
• dependent function types
  • condensed syntax for multiple parameters
  • implicit parameters
• records
  • non-dependent
  • dependent
• holes
  • named holes
• numeric types
• numeric literals
  • decimal literals
  • non-decimal radixes
  • custom parsing
• array types
• array literals
• binary format descriptions
  • succcess formats
  • failure formats
  • end-of-input formats
  • record formats
    • conditional field sugar
    • skipped fields
  • position formats
  • link formats
  • map formats
  • numeric formats
  • array formats
  • uniform-choice formats
  • choice formats
  • repeat formats
• refinement types
• match expressions
  • single-layer pattern matching
  • multi-layer pattern matching
  • dependent pattern matching
• patterns
  • wildcard patterns
  • named patterns
  • annotated patterns
  • numeric literal patterns
  • record literal patterns
• invertible format descriptions

Implementation

• command line interface
  • parse arbitrary top-level items
  • parse from an offset
  • navigation through links and offsets
  • serialise data to JSON for use with tools like jq
• parser
• pretty printing
  • surface language
  • core language
• source locations
  • surface language
  • core language
• string interning
• arena allocation
• value interning (for commonly used values)
• normalisation-by-evaluation
  • stack traces
• elaborator
  • error recovery
  • unification
  • zonking
• distiller
  • improve binder names
  • improve hole names
• core language validation
• binary format interpreter
  • parser
  • pretty printer
• compiler
• codespan diagnostics
  • unification solutions
  • terms and types included in messages
• integration tests
  • basic error code checks
  • snapshot testing
  • diagnostic expectations
  • binary parser tests

Ideas for future experimentation

• integer refinements (see Refinement Types: A tutorial and sprite-lang, and also this twitter thread)