Apply Kick-the-tires feedback
I think it can typecheck under Agda 2.7.3/standard-library 1.7.1
Add more comments
This repository contains an Agda formalization of the semantics of Kalpis and RRArr, presented in the ESOP24 paper Reconciling Partial and Local Invertibility (Ågren Thuné, Matsuda and Wang 2024). The main purpose of this implementation is to be type-checked, rather than to be executed.
The code in this repository was tested using Agda versions 2.6.3/2.6.4 and Agda stdlib version 1.7.1/1.7.3. Your mileage may vary on other versions (but we suspect that any sufficiently recent version supporting sized types should work).
To type check the proofs, invoke make
at the project root, or manually run agda Everything.agda
.
Agda will then type check all modules of the repository, outputting a line Checking ...
for each one to indicate its progress.
Note that this will take a long time (up to an hour or more), with the vast majority of the time spent on the file Kalpis/Properties/Completeness.agda
.
To reduce the type-checking time (if you trust us), you can disable the termination checker for that file by uncommenting the line {-# OPTIONS --no-termination-check #-}
at the top of the file.
With this line uncommented, the type-checking finishes in roughly 10 minutes on the development machine.
Type checking the proofs produces cache files in the _build
folder, which makes consecutive executions faster.
If you wish to remove the cache files to check the proofs from scratch, run make clean
, or simply remove the _build
folder.
This mechanized development is mentioned as a contribution in Section 1.1 of the paper. Thus, we have strived to keep definitions and proofs here very close to the paper's presentation, but there are a few differences.
This Agda formalization uses a well-scoped and intrinsically typed syntax based on De Bruijn indices, both for terms and types.
The dynamic semantics of Sections 3.5 and 4.2 in the paper are implemented in the form of definitional interpreters, using the sized delay monad to allow nontermination.
We use different arrow symbols to the paper's notation---double arrows for arrow combinator types and squiggly arrows for higher-order function types (see the table below).
For Theorems 3 and 4 in the paper, the Agda code features only the full version of the proof which covers the higher-order constructs introduced in Section 4.5 in the paper. Hence, the statements of these theorems are slightly more complicated than in the paper, and more resemble the paper's Theorems 5 and 6.
As stated in Section 5 of the paper, we fix the set of datatype constructors to tunit
, _⊗_
, _⊕_
, and μ A
(in addition to functional types) without loss of generality.
We do not implement the invertible first-match policy, instead observing only the first postcondition of a binary match (_⊕_
) and ignoring the postcondition for unary matches (tunit
, _⊗_
, and μ A
).
All major proofs are performed by well-founded induction on the step-count of evaluation, using the machinery in agda-stdlib's Data.Nat.Induction
.
More precisely, the 'step count' is the number of later
constructors (of the delay monad) wrapping the computation, and we use a judgment n ⊢ d ↠ v
(defined in PInj.agda
) to denote d
evaluating to v
in a finite n
number of steps.
To denote a pair of partial functions we use the notation i ⊢ A ⇔ B
(defined in PInj.agda
), where i
is the Size
of the results.
The property IsPInj (n : ℕ) (f : ∞ ⊢ A ⇔ B)
(defined in PInj.agda
) then asserts that n
-step evaluation of f
has an n
-step inverse in each direction.
By proving this property for all n
, we can show that f
is a partial injection such that forward and backward evaluation always take the same number of steps.
For semantics preservation proofs, we typically have to prove multiple mutually recursive statements for each of the soundness and completeness statements: one for unidirectional terms and one or two for invertible terms.
We use a naming convention where the soundness theorem is called LangA⊇LangB
(e.g., Kalpis⊇RRArr
), and the completeness theorem is called LangB⊇LangA
(e.g., RRArr⊇Kalpis
) for a translation from LangA
to LangB
.
Each 'helper statement' is named Aterm⊇Bterm
, where Aterm
and Bterm
are the Agda names/notations for the corresponding terms (e.g., UTerm⊇⇒
for Kalpis and RRArr unidirectional terms).
This development uses Agda's Sized Types (--sized-types
) to allow modelling non-termination in our definitional interpreters.
Although this flag is known to be unsound in general, we use it only through modules defined in Agda's standard library (Codata.Delay
and Codata.Thunk
) which we believe to be sound.
In addition, we use them only in a limited set of our own modules, namely the ones defining and reasoning about the definitional interpreters for each language (PInj.adga
, PiArr/{Definitional,Properties}.agda
, RRArr/{Definitional,Properties}.agda
, Kalpis/{Definitional,Properties/*}.agda
).
Although these modules together constitute a significant number of lines of code, we hope that it should be clear that no intentional abuse of --sized-types
is performed in them.
The table below enumerates the definitions and theorems stated in the paper and lists the corresponding Agda definitions in this mechanization. For each definition, the relevant language is stated first: Kalpis/RRArr/PiArr, where PiArr is our variant of Πᵒ with higher-order constructs. Then, the definition / theorem and its location in the paper is given, after which location and name of the corresponding Agda definition(s) follow. For the last column, helper functions or cases to note are sometimes given in parentheses after the main definition(s).
Language | Definition / Theorem | Paper | File | Agda definition |
---|---|---|---|---|
Kalpis | Unidirectional term syntax | Page 9 | Kalpis/Syntax.agda |
UTerm |
Kalpis | Invertible term syntax | Page 9 | Kalpis/Syntax.agda |
RTerm |
Kalpis | Constructor/pattern syntax | Page 9 | Kalpis/Syntax.agda |
Con |
Kalpis | Datatype constructor syntax | Page 10 | Kalpis/Types.agda |
TyCon |
Kalpis | Type syntax | Page 10 | Kalpis/Types.agda |
Ty |
Kalpis | Unidirectional term typing | Page 12, Fig. 1 | Kalpis/Syntax.agda |
UTerm |
Kalpis | Invertible term typing | Page 12, Fig. 1 | Kalpis/Syntax.agda |
RTerm |
Kalpis | Pattern typing | Page 12, Fig. 1 | Kalpis/Syntax.agda |
Con |
Kalpis | Values | Page 13 | Kalpis/Value.agda |
Value |
Kalpis | Value environments | Page 13 | Kalpis/Value.agda |
ValEnv |
Kalpis | Unidirectional evaluation | Page 14, Fig. 2 | Kalpis/Definitional.agda |
evalU |
Kalpis | Forward/backward evaluation | Page 14, Fig. 2 | Kalpis/Definitional.agda |
evalR |
Kalpis | Theorem 1 (Subject reduction) | Page 14 | Kalpis/Definitional.agda |
evalU , evalR |
Kalpis | Theorem 2 (Invertibility) | Page 15 | Kalpis/Properties/Invertibility.agda |
evalR-pinj (evalR-pinj-ind ) |
RRArr | Unidirectional arrow syntax and typing | Page 16, Fig. 3 | RRArr/Syntax.agda |
_⇒_ |
RRArr | Invertible arrow syntax and typing | Page 16, Fig. 3 | RRArr/Syntax.agda |
_·_⇔_ |
RRArr | Base invertible combinators | Page 16, Fig. 3 | RRArr/PiO/Syntax.agda |
_⇔_ |
RRArr | Values | Page 17 | RRArr/Value.agda |
Value |
RRArr | Unidirectional evaluation | Page 18, Fig. 4 | RRArr/Definitional.agda |
evalU |
RRArr | Forward/backward evaluation | Page 18, Fig. 4 | RRArr/Definitional.agda |
evalR |
RRArr | Subject reduction | Page 17 | RRArr/Definitional.agda |
evalU , evalR |
RRArr | Invertibility | Page 17 | RRArr/Properties.agda |
·⇔-pinj (·⇔-pinj-ind ) |
PiArr | Syntax of Πᵒ | Page 17, Fig. 5 | PiArr/Syntax.agda |
_⇔_ |
RRArr/PiArr | Translation to Πᵒ (unidirectional arrows) | Pages 17-20 | RRArr/ToPiArr.agda |
⟦_⟧⇒ |
RRArr/PiArr | Translation to Πᵒ (invertible arrows) | Pages 17-20 | RRArr/ToPiArr.agda |
⟦_⟧· |
RRArr/PiArr | Theorem 3 (RRArr-->Πᵒ soundness) | Page 20 | RRArr/Properties.agda |
RRArr⊇PiArr (⇒⊇⇔ᵃ , ·⇔⊇⇔ᵃ ) |
RRArr/PiArr | Theorem 4 (RRArr-->Πᵒ completeness) | Page 20 | RRArr/Properties.agda |
PiArr⊇RRArr (⇔ᵃ⊇⇒ , ⇔ᵃ⊇·⇔-fwd , ⇔ᵃ⊇·⇔-bwd ) |
RRArr | Higher-order combinator syntax and typing | Page 20, Fig. 6 | RRArr/Syntax.agda |
_⇒_ , _·_⇔_ (curry , curry● , app , app● ) |
RRArr | Higher-order combinator semantics | Page 20, Fig. 6 | RRArr/Definitional.agda |
evalU , evalR (curry , curry● , app , app● ) |
PiArr | Higher-order combinator syntax | Page 21 | PiArr/Syntax.agda |
_⇔_ (curry , app ) |
PiArr | Higher-order combinator semantics | Page 21 | PiArr/Definitional.agda |
eval (curry , app ) |
RRArr/PiArr | Translation of higher-order combinators | Page 21 | RRArr/ToPiArr.agda |
⟦_⟧⇒ , ⟦_⟧· (curry , curry● , app , app● ) |
RRArr/PiArr | Theorems 3,4 with higher-order combinators | Page 21 | RRArr/Properties.agda |
RRArr⊇PiArr , PiArr⊇RRArr (curry , curry● , app , app● ) |
Kalpis/RRArr | Γˣ operation |
Page 22 | Kalpis/ToRRArr.agda |
⟦_⟧ˣ |
Kalpis/RRArr | lookupₓ combinator |
Page 22 | Kalpis/ToRRArr.agda |
lookupVar |
Kalpis/RRArr | splitΘ₁,Θ₂ combinator |
Page 22 | Kalpis/ToRRArr.agda |
splitEnv |
PiArr | distl combinator |
Page 22 | PiArr/Syntax.agda |
distl (we take this as the primitive and derive distr ) |
RRArr | case combinator |
Page 22 | RRArr/Syntax.agda |
caseᵣ |
RRArr | mkCond operator |
Page 22 | Kalpis/ToRRArr.agda |
case●-postcond |
Kalpis/RRArr | Translation to RRArr (unidirectional terms) | Pages 21-23 | Kalpis/ToRRArr.agda |
⟦_⟧ᵘ |
Kalpis/RRArr | Translation to RRArr (invertible terms) | Pages 21-23 | Kalpis/ToRRArr.agda |
⟦_⟧ʳ |
Kalpis/RRArr | Translation to RRArr (values and environments) | Page 23 | Kalpis/ToRRArr.agda |
⟦_⟧ᵛ , ⟦_⟧ᵉ |
Kalpis/RRArr | Theorem 5 (Kalpis-->RRArr soundness) | Page 23 | Kalpis/Properties/Soundness.agda |
Kalpis⊇RRArr (UTerm⊇⇒ , RTerm⊇·⇔ ) |
Kalpis/RRArr | Theorem 6 (Kalpis-->RRArr completeness) | Page 23 | Kalpis/Properties/Completeness.agda |
RRArr⊇Kalpis (⇒⊇UTerm , ·⇔⊇RTerm-fwd , ·⇔⊇RTerm-bwd ) |
The repository is structured into folders based on the various languages formalized (Kalpis/
, RRArr/
, and PiArr/
, where PiArr
is Πᵒ extended with higher-order constructs).
Each folder contains at least Syntax.agda
defining the language's intrinsically typed syntax, Definitional.agda
giving a definitional interpreter of the language, and Properties.agda
establishing properties like invertibility of the corresponding semantics.
For an overview of all modules, see Everything.agda
at the repository root, which also provides more detailed descriptions of each module's contents.