communicating-type-theory.md

Communicating type theory and formal systems

Doing a better job of communicating type theory and formal systems

Problems to solve

• languages should have better specifications
• our current notation limits our reach
• puts up barriers between researchers and potential implementers
• hard to gain an intuition of complicated formal systems from static descriptions
• hard to manage large specifications
• even researchers haver a hard time decoding type theory notation
• type theory notation is optimised for the blackboard and the notebook, not necessarily for communicating

Inspiration

• Web assembly specification
  • hyperlinks do judgement definitions
  • uses records for contexts
  • uses longer, descriptive identifiers instead of single letters
  • self-contained description of the notation
  • still limits itself to type theory notation
• Swift reference manual
  • IDE-style bubbles for non-terminals
  • hyperlinks
  • self-contained description of the notation
  • examples and prose throughout
  • https://docs.swift.org/swift-book/ReferenceManual/Declarations.html#ID367
• Dhall specification
• TypesWhoSayNi
  • https://github.com/pigworker/TypesWhoSayNi/blob/master/bis/Deriv.agda
  • https://github.com/pigworker/TypesWhoSayNi/blob/master/bis/STLC.agda
  • https://github.com/pigworker/TypesWhoSayNi/blob/master/bis/ML71.agda

A better specification format

• how might we envisage a better notation?
• embeddable in
  • specifications
  • presentations
• database of
  • productions
  • judgement forms
  • inference rules
  • natural language descriptions
  • examples (failing and passing)
  • bidirectional links from specification to reference implementation
• render different views:
  • index of judgement forms
  • index of productions
  • english descriptions
  • type theory view
  • dependency graphs
  • example proof trees
• queries
  • find usage sites (in rest of spec)
  • find reference implementation