Agda Core

Where do we come from and where do we go?

Jesper Cockx

13 October 2020

January 2020

September 2020

Currently

Core language, wa’s da?

A question of trust

Agda’s type checker checks correctness of our programs and proofs…

…but who checks the checker?

Criteria of a core language

  • Small
  • Formally defined
  • Most/all of surface language can be translated
  • Independent checker
  • Unreadable syntax (?)

Reasons to want a core language

  • Minimizing trusted code base
  • Enabling theoretical study
  • Intermediate language for compiler optimization
  • As an interface for reflection
  • Interoperability with other languages

Reasons to NOT want a core language

  • Makes it harder to implement certain new features
  • Errors in core language can be incomprehensible
  • Performance overhead of encoding vs direct implementation

Where do we come from?

Current syntax representations:

  • Internal syntax
  • Reflected syntax
  • Treeless syntax

Internal syntax

  • internal double-checker CheckInternal!

BUT: does not cover datatypes and pattern matching

Reflected syntax

  • embedded in Agda!

BUT: no formally defined type system

Treeless syntax

Nice for doing optimizations

BUT: impossible to implement a type checker

The Agda spec

https://github.com/agda/agda-spec/

MetaCoq

  • A formalization of Coq in Coq
    • Quoting library Template-Coq
    • Standard metatheory for PCuIC
    • MetaCoq SafeCheck, a safe-by-construction typechecker
    • Verified Erasure to untyped lambda calculus
  • No good story yet for termination, eta-equality, and irrelevance

PiSigma: dependent types without the sugar (2010)

  • A small core language designed for Agda
  • Boxed terms to control unfolding
  • Potential issues
    • Type : Type
    • No support for general indexed datatypes (no propositional equality!)
    • Very nontrivial notion of alpha-equality

Where do we go?

Agda Core

My goal: develop a core language for Agda that:

  • Is embedded in Agda itself
  • Has a correct-by-construction typechecker
  • Can be connected to the main typechecker
  • Covers all basic features of Agda:
    • Inductive datatypes and records
    • Dependent pattern matching
    • Eta equality for functions and records
    • Universe levels
  • Can easily be extended with new features

Features that could be added later

  • Module system
  • Termination checking / sized types
  • Coinduction
  • Irrelevance
  • Cubical primitives
  • Rewrite rules

Challenge 1: level of encoding

The more features can be encoded, the smaller the core language can be…

… but the more complex the elaboration and the harder to understand the core code!

  • Inductive families: direct support or encoding?
  • Pattern matching: clauses/case trees/eliminators?
  • Implicit or explicit conversion rule?

Challenge 2: syntax representation

  • Spine form? Do we allow let-bindings?
  • Case trees as part of syntax?
  • Substitution: explicit or implicit?
  • Scoping and typing: intrinsic vs extrinsic vs mixed?

Challenge 3: extensibility

How to ensure new features can be added without rewriting Agda Core from scratch?

Let’s go on to the core!

References