Formalisation of some logical systems, in Agda, Idris, and Haskell.
This work compares a number of techniques for formalising typed higher-order languages in a typed meta-language, with an eye towards the readability of programs written in the resulting object-language.
Following Troelstra and Schwichtenberg, we use M, I, and C for minimal, intuitionistic, and classical first-order predicate calculus, respectively; Mp, Ip, and Cp stand for the corresponding propositional systems. For technical reasons, we refer to minimal implicational logic as ArrMp, and to minimal implicational modal logic as BoxMp.
We investigate the issue of binder representation by contrasting the use of de Bruijn indices against parametric higher-order abstract syntax (PHOAS), after Chlipala. Each approach is presented in the widely-used initial encoding, using a generalised algebraic data type, and the final encoding of Carette, Kiselyov, and Shan, using a sequence of type classes.
We refer to the de Bruijn, vector-based de Bruijn, and PHOAS approach as B, V, and P, respectively; i and f correspond to the initial and final encoding.
Pi | Pf | Bi | Vi | Bf | |
---|---|---|---|---|---|
ArrMp | agda , idr , hs |
agda , idr , hs |
agda |
agda |
agda |
BoxMp | agda , idr , hs |
agda , idr , hs |
agda |
agda |
agda |
Mp | agda , idr , hs |
agda , idr , hs |
agda |
agda |
agda |
Ip | agda , idr , hs |
agda , idr , hs |
agda |
agda |
agda |
Cp | agda , idr , hs |
agda , idr , hs |
agda |
agda |
agda |
M | agda , idr |
||||
I | agda , idr |
||||
C | agda , idr |
To check all files automatically:
$ make
To load a particular file for interactive use:
$ agda --safe -I -i src src/FILE.agda
$ ghci -Wall -isrc src/FILE.hs
$ idris -i src src/FILE.idr
Tested with Agda 2.4.2.3, Idris 0.9.19, and GHC 7.8.4.
This section describes the notation available in the PHOAS approach; in the de Bruijn approach, variable binding is not part of the constructors or eliminators.
Op | Type | Constructors | Eliminators |
---|---|---|---|
→ | => |
lam v => e |
e₁ $ e₂ |
∧ | && |
[ e₁ , e₂ ] |
fst e ; snd e |
∨ | ` | ` | |
⊥ | FALSE |
— | I: abort e ; C: abort v => e |
↔︎ | <=> |
— | — |
¬ | NOT |
— | — |
⊤ | TRUE |
— | — |
∀ | FORALL |
pi v => e |
e₁ $$ e₂ |
∃ | EXISTS |
[ e₁ ,, e₂ ] |
split e₀ as v => e |
□ | BOX |
box e |
unbox e₀ as v => e |
◇ | DIAMOND |
— | — |
Op | Type | Constructors | Eliminators |
---|---|---|---|
→ | :=> |
lam v :=> e |
e₁ :$ e₂ |
∧ | :&& |
[ e₁ , e₂ ] |
fst e ; snd e |
∨ | `: | ` | |
⊥ | FALSE |
— | I: abort e ; C: abort v :=> e |
↔︎ | :<=> |
— | — |
¬ | NOT |
— | — |
⊤ | TRUE |
— | — |
∀ | FORALL |
pi v :=> e |
e₁ :$$ e₂ |
∃ | EXISTS |
[ e₁ ,, e₂ ] |
split e₀ as v :=> e |
□ | BOX |
box e |
unbox e₀ as v :=> e |
◇ | DIAMOND |
— | — |
Op | Type | Constructors | Eliminators |
---|---|---|---|
→ | :=> |
lam λ |
i: e₁ :$ e₂ ; f: e₁ .$ e₂ |
∧ | :&& |
pair ( e₁ , e₂ ) |
fst' e ; snd' e |
∨ | `: | ` | |
⊥ | FALSE |
— | I: abort e ; C: abort λ |
↔︎ | :<=> |
— | — |
¬ | NOT |
— | — |
⊤ | TRUE |
— | — |
∀ | FORALL |
pi λ |
i: e₁ :$$ e₂ ; f: e₁ .$$ e₂ |
∃ | EXISTS |
sig ( e₁ , e₂ ) |
split e₀ λ |
□ | BOX |
box e |
unbox e₀ λ |
◇ | DIAMOND |
— | — |
Made by Miëtek Bak. Published under the MIT X11 license.
Thanks to Dominique Devriese, Darryl McAdams, and Andrea Vezzosi for comments and discussion.
- J.-P. Bernardy,
PHOAS.hs
, 2008 - G. Boolos, “The logic of provability”, 1993
- J. Carette, O. Kiselyov, C. Shan, “Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages”, 2009
- A. Chlipala, “Parametric higher-order abstract syntax for mechanized semantics”, 2008
- N.A. Danielsson,
HOAS.SimplyTyped.agda
, 2008 - D. Devriese, F. Piessens, “On the bright side of type classes: Instance arguments in Agda”, 2011
- F. Pfenning, R. Davies, “A judgmental reconstruction of modal logic”, 2001
- A.S. Troelstra, H. Schwichtenberg, “Basic proof theory”, 2000