-- "Polarity and duality in type theory" -- Noam Zeilberger -- Agda code accompanying talk at Dependently Typed Programming '08 -- -- I give an encoding of a focused sequent calculus using iterated -- inductive definitions, and show how to use "abstract higher-order -- syntax" to get "pattern-matching for free". For some background, -- see the following papers: -- "Focusing and higher-order abstract syntax" (POPL '08) -- "On the unity of duality" (APAL, to appear) -- "Focusing on binding and computation", with Dan Licata and Bob Harper open import Data.List open import Data.String renaming (_++_ to concat) module Main where -- a bit of syntactic sugar for singleton lists [_] : {A : Set} -> A -> List A [_] x = x :: [] -- Following Girard, we syntactically segregate positive and -- negative formulas, with mutual coercions given by ↓ and ↑ module Types where Atom : Set Atom = String mutual data Pos : Set where X⁺ : Atom -> Pos -- positive atoms ↓ : Neg -> Pos -- shifted negative formulas 1⁺ : Pos -- unit _*_ : Pos -> Pos -> Pos -- strict products 0⁺ : Pos -- void _+_ : Pos -> Pos -> Pos -- sums 2⁺ : Pos -- booleans ℕ : Pos -- natural numbers data Neg : Set where X⁻ : Atom -> Neg -- negative atoms ↑ : Pos -> Neg -- shifted positive formulas ⊤ : Neg -- lazy unit _→_ : Pos -> Neg -> Neg -- functions _&_ : Neg -> Neg -> Neg -- lazy products Stream : Neg -> Neg -- streams infixr 14 _→_ infixr 15 _&_ infixr 15 _+_ infixr 16 _*_ -- Here we define the machinery of contexts. The restrictions -- on hypotheses/conclusions reflect the duality positive/negative. module Contexts where open Types public data Hyp : Set where HP : Atom -> Hyp HN : Neg -> Hyp data Conc : Set where CP : Pos -> Conc CN : Atom -> Conc -- LCtx's are lists of hypotheses, and proofs of membership are -- isomorphic to de Bruijn indices LCtx : Set LCtx = List Hyp data _∈_ : Hyp -> LCtx -> Set where f0 : {h : Hyp} {Δ : LCtx} -> h ∈ (h :: Δ) fS : {h h' : Hyp} {Δ : LCtx} -> h' ∈ Δ -> h' ∈ (h :: Δ) -- For convenience, we also define lists of lists of hypotheses. -- Proofs of membership are isomorphic to "2-level" de Bruijn indices. UCtx : Set UCtx = List LCtx data _∈∈_ : Hyp -> UCtx -> Set where s0 : {h : Hyp} {Δ : LCtx} {Γ : UCtx} -> h ∈ Δ -> h ∈∈ (Δ :: Γ) sS : {h : Hyp} {Δ : LCtx} {Γ : UCtx} -> h ∈∈ Γ -> h ∈∈ (Δ :: Γ) -- Now the fun part: the definitions of the connectives by pattern-typing. -- Positive connectives are defined by constructor patterns, negative -- connectives by destructor patterns. module Patterns where open Contexts public -- Pat⁺ Δ A⁺ = linear entailment "Δ ⇒ A⁺" data Pat⁺ : LCtx -> Pos -> Set where Px : {x : Atom} -> Pat⁺ [ HP x ] (X⁺ x) Pu : {A⁻ : Neg} -> Pat⁺ [ HN A⁻ ] (↓ A⁻) P<> : Pat⁺ [] 1⁺ Ppair : {Δ1 : LCtx} { Δ2 : LCtx } {A : Pos} {B : Pos} -> Pat⁺ Δ1 A -> Pat⁺ Δ2 B -> Pat⁺ (Δ1 ++ Δ2) (A * B) Pinl : {Δ : LCtx} {A B : Pos} -> Pat⁺ Δ A -> Pat⁺ Δ (A + B) Pinr : {Δ : LCtx} {A B : Pos} -> Pat⁺ Δ B -> Pat⁺ Δ (A + B) Ptt : Pat⁺ [] 2⁺ Pff : Pat⁺ [] 2⁺ Pz : Pat⁺ [] ℕ Ps : {Δ : LCtx } -> Pat⁺ Δ ℕ -> Pat⁺ Δ ℕ -- Pat⁻ Δ A⁻ c = linear entailment "Δ ; A⁻ ⇒ c" data Pat⁻ : LCtx -> Neg -> Conc -> Set where Dx : forall {x} -> Pat⁻ [] (X⁻ x) (CN x) D_ : forall {A⁺} -> Pat⁻ [] (↑ A⁺) (CP A⁺) Dapp : {Δ1 : LCtx } {Δ2 : LCtx} {A⁺ : Pos} {B⁻ : Neg} {c : Conc} -> Pat⁺ Δ1 A⁺ -> Pat⁻ Δ2 B⁻ c -> Pat⁻ (Δ2 ++ Δ1) (A⁺ → B⁻) c Dfst : {Δ : LCtx} {A⁻ : Neg} {B⁻ : Neg} {c : Conc} -> Pat⁻ Δ A⁻ c -> Pat⁻ Δ (A⁻ & B⁻) c Dsnd : {Δ : LCtx} {A⁻ : Neg} {B⁻ : Neg} {c : Conc} -> Pat⁻ Δ B⁻ c -> Pat⁻ Δ (A⁻ & B⁻) c Dhd : {Δ : LCtx} {A⁻ : Neg} {c : Conc} -> Pat⁻ Δ A⁻ c -> Pat⁻ Δ (Stream A⁻) c Dtl : {Δ : LCtx} {A⁻ : Neg} {c : Conc} -> Pat⁻ Δ (Stream A⁻) c -> Pat⁻ Δ (Stream A⁻) c -- Finally, we define the judgments of the focused sequent calculus -- as an iterated inductive definition, by reference to pattern-typing. module Logic where open Patterns public mutual -- RFoc Γ A⁺ = right-focus "Γ ⊢ [A⁺]" -- a.k.a. "positive value" data RFoc : UCtx -> Pos -> Set where Val⁺ : forall {Γ A⁺ Δ} -> Pat⁺ Δ A⁺ -> SatCtx Γ Δ -> RFoc Γ A⁺ -- LInv Γ c₀ c = left-inversion "Γ ; c₀ ⊢ c" -- a.k.a. "positive continuation" data LInv : UCtx -> Conc -> Conc -> Set where IdX⁻ : forall {Γ X⁻ } -> LInv Γ (CN X⁻) (CN X⁻) Con⁺ : forall {Γ A⁺ c} -> ({Δ : LCtx} -> Pat⁺ Δ A⁺ -> UnFoc (Δ :: Γ) c) -> LInv Γ (CP A⁺) c -- RInv Γ h = right-inversion "Γ ⊢ h;" -- a.k.a. "negative value" data RInv : UCtx -> Hyp -> Set where Val⁻ : forall {Γ A⁻ } -> ({Δ : LCtx} {c : Conc} -> Pat⁻ Δ A⁻ c -> UnFoc (Δ :: Γ) c) -> RInv Γ (HN A⁻) IdX⁺ : forall {Γ X⁺ } -> ((HP X⁺) ∈∈ Γ) -> RInv Γ (HP X⁺) Fix : forall {Γ h} -> RInv ([ h ] :: Γ) h -> RInv Γ h -- LFoc Γ A⁻ c = left-focus "Γ ; [A⁻] ⊢ c" -- a.k.a. "negative continuation" data LFoc : UCtx -> Neg -> Conc -> Set where Con⁻ : forall {Δ A⁻ c0 c Γ} -> Pat⁻ Δ A⁻ c0 -> SatCtx Γ Δ -> LInv Γ c0 c -> LFoc Γ A⁻ c -- UnFoc Γ c = unfocused "Γ ⊢ c" -- a.k.a. "expression" data UnFoc : UCtx -> Conc -> Set where Ret : forall {Γ A⁺ } -> RFoc Γ A⁺ -> UnFoc Γ (CP A⁺) App : forall {Γ A⁻ c} -> ((HN A⁻) ∈∈ Γ) -> LFoc Γ A⁻ c -> UnFoc Γ c -- SatCtx Γ Δ = conjoined inversion "Γ ⊢ Δ;" -- a.k.a. "substitution" data SatCtx : UCtx -> LCtx -> Set where Sub : forall {Γ Δ} -> ({h : Hyp} -> (h ∈ Δ) -> (RInv Γ h)) -> SatCtx Γ Δ -- Because of the uniform presentation of the sequent calculus -- through pattern-typing, we can define both identity and -- cut-elimination procedures in a completely modular way! These -- procedures might not necessarily terminate, however, due to the -- presence of recursive types. Here we define the identity -- (i.e. eta-expansion) procedure, which type-checks but does not -- pass Agda's termination checker. See one of the papers above for -- the modular cut-elimination procedure. module Theorems where open Logic mutual Id⁺ : {Γ : UCtx} {c : Conc} -> LInv Γ c c Id⁺ {_} {CN _} = IdX⁻ Id⁺ {_} {CP A⁺} = Con⁺ (\p -> Ret (Val⁺ p (IdSub (\x -> s0 x)))) Id⁻ : {Γ : UCtx} {h : Hyp} -> (h ∈∈ Γ) -> RInv Γ h Id⁻ {_} {HP _} x = IdX⁺ x Id⁻ {_} {HN _} u = Val⁻ (\d -> App (weak u) (Con⁻ d (IdSub (\x -> s0 x)) Id⁺)) where weak : {Γ : UCtx} {h : Hyp} {Δ : LCtx} -> (h ∈∈ Γ) -> (h ∈∈ (Δ :: Γ)) weak u = sS u IdSub : {Γ : UCtx} {Δ : LCtx} -> ({h : Hyp} -> (h ∈ Δ) -> (h ∈∈ Γ)) -> SatCtx Γ Δ IdSub f = Sub (\x -> Id⁻ (f x)) -- And now some examples! module Examples where open Logic open Theorems -- The empty substitution NilSub : {Γ : UCtx} -> SatCtx Γ [] NilSub = Sub f where f : {h : Hyp} -> h ∈ [] -> RInv _ h f () -- The values true and false tt : {Γ : UCtx} -> RFoc Γ 2⁺ tt = Val⁺ Ptt NilSub ff : {Γ : UCtx} -> RFoc Γ 2⁺ ff = Val⁺ Pff NilSub -- Boolean negation not : (Γ : UCtx) -> RInv Γ (HN (2⁺ → ↑ 2⁺)) not Γ = Val⁻ not* where not* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c not* (Dapp Ptt D_) = Ret ff not* (Dapp Pff D_) = Ret tt -- Boolean conjunction and : (Γ : UCtx) -> RInv Γ (HN (2⁺ → 2⁺ → ↑ 2⁺)) and Γ = Val⁻ and* where and* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (2⁺ → 2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c and* (Dapp Ptt (Dapp Ptt D_)) = Ret tt and* (Dapp Ptt (Dapp Pff D_)) = Ret ff and* (Dapp Pff (Dapp Ptt D_)) = Ret ff and* (Dapp Pff (Dapp Pff D_)) = Ret ff -- As Conor McBride pointed out during the talk, we can also define -- boolean conjunction using "short-circuit evaluation" and' : (Γ : UCtx) -> RInv Γ (HN (2⁺ → 2⁺ → ↑ 2⁺)) and' Γ = Val⁻ and'* where and'* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (2⁺ → 2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c and'* (Dapp Ptt (Dapp Ptt D_)) = Ret tt and'* (Dapp _ (Dapp _ D_)) = Ret ff -- Some syntactic sugar for applying a function of type A → ↑ B App1 : {Γ : UCtx} {A⁺ B⁺ : Pos} {c : Conc} -> (HN (A⁺ → ↑ B⁺) ∈∈ Γ) -> (RFoc Γ A⁺) -> (LInv Γ (CP B⁺) c) -> UnFoc Γ c App1 u (Val⁺ p σ) F = App u (Con⁻ (Dapp p D_) σ F) -- A little lemma stating that every boolean pattern is closed ⌊_⌋ : {Δ : LCtx} -> Pat⁺ Δ 2⁺ -> Pat⁺ [] 2⁺ ⌊_⌋ Ptt = Ptt ⌊_⌋ Pff = Pff -- A function computing the truth table of a unary boolean operation table1 : (Γ : UCtx) -> RInv Γ (HN (↓(2⁺ → ↑ 2⁺) → ↑ (2⁺ * 2⁺))) table1 Γ = Val⁻ table1* where table1* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (↓(2⁺ → ↑ 2⁺) → ↑ (2⁺ * 2⁺)) c -> UnFoc (Δ :: Γ) c table1* (Dapp Pu D_) = App1 (s0 f0) tt (Con⁺ (\b1 -> App1 (sS (s0 f0)) ff (Con⁺ (\b2 -> Ret (Val⁺ (Ppair ⌊ b1 ⌋ ⌊ b2 ⌋) NilSub))))) -- The predecessor function on natural numbers pred : (Γ : UCtx) -> RInv Γ (HN (ℕ → ↑ ℕ)) pred Γ = Val⁻ pred* where pred* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (ℕ → ↑ ℕ) c -> UnFoc (Δ :: Γ) c pred* (Dapp Pz D_) = Ret (Val⁺ Pz NilSub) pred* (Dapp (Ps n) D_) = Ret (Val⁺ n (IdSub (\x -> s0 x))) -- here we used IdSub, though we could also have used NilSub -- after first proving a lemma that every natural number -- pattern is closed -- An infinite stream of zeros zeros : (Γ : UCtx) -> RInv Γ (HN (Stream (↑ ℕ))) zeros Γ = Fix (Val⁻ zeros*) where zeros* : {Δ : LCtx} {c : Conc} -> Pat⁻ Δ (Stream (↑ ℕ)) c -> UnFoc (Δ :: [ HN (Stream (↑ ℕ)) ] :: Γ) c zeros* (Dhd D_) = Ret (Val⁺ Pz NilSub) zeros* (Dtl d) = App (sS (s0 f0)) (Con⁻ d (IdSub (\x -> s0 x)) Id⁺)