A question of trust

Our type checkers check correctness of our programs and proofs…

Agda Core

This talk is about my attempts to build Agda Core:

• A formally specified core language
• A correct-by-construction type checker for it
• A backend connecting Agda Core to Agda

Talk overview

• The dream
  What is the goal of Agda Core?
  
• The reality
  What are the obstacles and challenges in implementing it?
  

Why a core language?

• To minimize the trusted code base
• To enable theoretical study
• As an intermediate language for optimizations
• As an interface for reflection
• For interoperability with other languages
• …

Criteria for a core language

• Small and readable implementation
• Formally specified static and dynamic semantics
• Support for all surface features through elaboration
• Ideally: formal metatheory with a soundness proof

Agda Core goals

Goal. a core language for Agda that…

• Is implemented in Agda itself
• Has a correct-by-construction typechecker that can double-check the output of Agda
• 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

A spectrum of core languages

Agda Core is…

• More than a reference type checker: formal specification of semantics + type checker that produces derivations
• Less than a fully formal metatheory: no proofs of confluence, subject reduction, canonicity, or consistency

Main parts of the implementation

• A scope library for well-scoped names
• A syntax with dependent functions + universes + simple datatypes + global definitions
• An abstract machine for reduction
• Extrinsic typing and conversion rules
• Correct-by-construction type and conversion checkers

Well-scoped syntax of Agda Core

Implementation decisions

• Extensive use of erasure annotations
• Extraction of simple and readable Haskell typechecker through agda2hs
• Eventually: connection to main Agda implementation as a backend

Four design challenges

1. Substitution vs let-bindings
2. Typed vs untyped conversion
3. Checking vs inferring case expressions
4. Minimal vs invariant-rich syntax

1. Substitution vs let

We define reduction using an abstract machine:

1. An environment of shared terms
2. A focus term currently being evaluated
3. A stack of frames to continue evaluating later

1. Substitution vs let

Ways to convert a machine state back into a term:

1. Substitution: duplicates terms! (*)
2. let-bindings: retains unused terms!
3. Retaining the environment everywhere?

2. Typed vs untyped conversion

Agda uses typed conversion for a few features:

• Eta-equality for functions
• Eta-equality for record types
  • In particular: eta-equality for the unit type
• Definitional proof irrelevant Prop universe

2. Typed vs untyped conversion

2. Typed vs untyped conversion

How can we allow for comparing types at different sorts (e.g. domain of pi type)?

• A typed conversion judgement
  • always need to compare sorts of types first
• An untyped conversion judgement
  • do eta-expansion in the elaborator?
  • do eta-expansion in the conversion checker? (*)
• Two conversion judgements: a typed one for terms and an untyped one for types

3. Checking vs inferring case expressions

In Agda Core, pattern matching is represented as an elimination:

We’d like to use case without typing annotations, but that does not fit cleanly in a bidirectional discipline!

3. Checking vs inferring case expressions

Possible solutions:

• Require a type annotation on each case (*)
• Model only definition-level pattern matching
• Only allow case on a variable

4. Minimal vs invariant-rich syntax

Data/record types are represented with as a Def, so checking a constructor application requires:

• checking if the given type is a datatype
• extracting its parameters and indices

4. Minimal vs invariant-rich syntax

4. Minimal vs invariant-rich syntax

This would be much cleaner with a dedicated syntax constructor for datatypes!

Is simplifying the type checker worth adding extra complexity to the syntax?

Agda Core: overambitious …

This took much more time than initially planned:

• Experimenting with different scope representations
• Fixing bugs and adding features agda2hs
• Figuring out how to deal with non-termination
• Developing techniques to work with erasure
• Working around particularities of Agda’s internals

… and it’s still far from being finished!

… or exactly right?

These challenges suggest a research question:

What are best practices for designing and implementing correct-by-construction type checkers?

Let’s go and find out!

Time for questions!