## Four design challenges

- Substitution vs let-bindings
- Typed vs untyped conversion
- Checking vs inferring case expressions
- Minimal vs invariant-rich syntax

## 1. Substitution vs let

We define reduction using an *abstract machine*:

- An
**environment** of shared terms
- A
**focus** term currently being evaluated
- A
**stack** of frames to continue evaluating later

## 1. Substitution vs let

Ways to convert a machine state back into a term:

**Substitution**: duplicates terms! (*)
`let`

-bindings: retains unused
terms!
- 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?