module BoundSig where
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Sum
open import Data.Product
open import Relation.Unary
open import Relation.Binary.PropositionalEquality
-- * Worlds
record World (Ctxts : Set)(Types : Set) : Set₁ where
field
_⇒_ : (Γ Δ : Ctxts) → Set
_⊗_ : (Γ Δ : Ctxts) → Ctxts
inl : ∀{Γ Δ} → Γ ⇒ (Γ ⊗ Δ)
inr : ∀{Γ Δ} → Δ ⇒ (Γ ⊗ Δ)
⟦_⟧ : Ctxts → (Types → Set)
⟦_⟧map : ∀{Γ Δ} → Γ ⇒ Δ → ⟦ Γ ⟧ ⊆ ⟦ Δ ⟧
strict-⟦⟧ : ∀{Γ Δ} → ⟦ Γ ⊗ Δ ⟧ ⊆ ⟦ Γ ⟧ ∪ ⟦ Δ ⟧
module MapW {Ctxts : Set}{Types : Set}(w : World Ctxts Types) where
open World w
inl-⟦⟧ : ∀ {Γ} Δ → ⟦ Γ ⟧ ⊆ ⟦ Γ ⊗ Δ ⟧
inl-⟦⟧ Δ = ⟦ inl ⟧map
inr-⟦⟧ : ∀ {Δ} Γ → ⟦ Δ ⟧ ⊆ ⟦ Γ ⊗ Δ ⟧
inr-⟦⟧ Δ = ⟦ inr ⟧map
mapL : ∀{Γ Δ Ω : Ctxts} →
(⟦ Γ ⟧ ⊆ ⟦ Δ ⟧) → ⟦ Γ ⊗ Ω ⟧ ⊆ ⟦ Δ ⊗ Ω ⟧
mapL ρ k = [ inl-⟦⟧ _ ∘ ρ , inr-⟦⟧ _ ]′ (strict-⟦⟧ k)
-- * Presentations
-- A Presentation is a multi-sorted, binding signature :
record Presentation (Ctxts : Set)(Types : Set) : Set₁ where
field
-- Operations:
Op : Types → Set
-- Aritites:
Ar : ∀{T} → Op T → Set
-- Bindings:
Bi : ∀ {T sh} → Ar {T} sh → Ctxts
-- Typings of recursive arguments:
Ty : ∀ {T sh} → Ar {T} sh → Types
-- * Free term algebra
-- From a presentation, we can build the syntax of terms (defined by
-- Tm) with bindings (defined by Scope[_]).
module Terms {Ctxts Types}(w : World Ctxts Types)
(Σ : Presentation Ctxts Types) where
open World w
open Presentation Σ
mutual
-- Term of type I in context W:
data Tm (Γ : Ctxts) : Types → Set where
`var : ∀{T} → ⟦ Γ ⟧ T → Tm Γ T
`op : ∀{T} → (sh : Op T)
(Xs : (pos : Ar sh) → Scope[ Bi pos ] Γ (Ty pos)) → Tm Γ T
-- Binder of Ω-variables :
data Scope[_] (Ω Γ : Ctxts)(T : Types) : Set where
sc : Tm (Γ ⊗ Ω) T → Scope[ Ω ] Γ T
-- Question: According to the ncat lab
-- [http://ncatlab.org/nlab/show/tensorial+strength], having a strong
-- functor equivalent to having an enriched functor. We use the
-- stength only once in 'scopeSub' to build the term:
-- λ v → str mapTm (Data.Sum.map ρ id (mon⟦⟧ v)) : ⟦ Γ ⟧ ⊗ ⟦ Ω ⟧ ⊆ Tm (Δ ⊗ Ω)
-- with ρ : ⟦ Γ ⟧ ⊆ Tm Δ
-- I wonder if adopting an enriched approach could absorb this term.
-- * Substitution structure
module Subst {Ctxts Types}(w : World Ctxts Types)
(Σ : Presentation Ctxts Types) where
open World w
open MapW w
open Presentation Σ
open Terms w Σ
mutual
-- Scope[ Ω ] : W → Set/I is a functor
-- ie. for f ∈ W(Γ, Δ)
-- we have a functorial map
-- mapSc f ∈ Set/I(Scope Γ, Scope Δ)
mapSc : ∀{Ω Γ Δ} →
(⟦ Γ ⟧ ⊆ ⟦ Δ ⟧) → Scope[ Ω ] Γ ⊆ Scope[ Ω ] Δ
mapSc {Ω} ρ (sc tm) = sc (mapTm (mapL {Ω = Ω} ρ) tm)
-- Tm : W → Set/I is a functor
-- ie. for f ∈ W(Γ, Δ),
-- we have a functorial map
-- mapTm f ∈ Set/I(Tm Γ, Tm Δ)
mapTm : ∀{Γ Δ} →
(⟦ Γ ⟧ ⊆ ⟦ Δ ⟧) → Tm Γ ⊆ Tm Δ
mapTm ρ (`var x) = `var (ρ x)
mapTm ρ (`op sh Xs) = `op sh λ pos → mapSc {Bi pos} ρ (Xs pos)
-- Tm is a (relative-)strong:
str : {Γ Δ : Ctxts} → Tm Γ ∪ ⟦ Δ ⟧ ⊆ Tm (Γ ⊗ Δ)
str {Δ = Δ} (inj₁ tm) = mapTm (inl-⟦⟧ Δ) tm
str (inj₂ k) = `var (inr-⟦⟧ _ k)
-- Tm Σ : W → Set/I is a relative monad over ⟦_⟧ : W → Set/I
-- ie.
-- 1. we have a natural transformation
-- return : ∀ Γ. Set/I(⟦ Γ ⟧, Tm Γ)
return : ∀{Γ} → ⟦ Γ ⟧ ⊆ Tm Γ
return = `var
mutual
-- 2. we have a natural transformation
-- bind : ∀ Γ Δ. Set/I(⟦ Γ ⟧, Tm Δ) → Set/I(Tm Γ, Tm Δ)
sub : ∀{Γ Δ} → (⟦ Γ ⟧ ⊆ Tm Δ) → Tm Γ ⊆ Tm Δ
sub ρ (`var x) = ρ x
sub ρ (`op sh Xs) = `op sh (λ pos → scopeSub {Bi pos} ρ (Xs pos))
-- Scope[ Ω ] : W → Set/I is a Tm-module
-- ie. we have a natural transformation
-- scopeSub : ∀ Γ Δ. Set/I(⟦ Γ ⟧, Tm Δ) → Set/I(Scope[ Ω ] Γ, Scope[ Ω ] Δ)
scopeSub : ∀{Ω Γ Δ} → (⟦ Γ ⟧ ⊆ Tm Δ) → Scope[ Ω ] Γ ⊆ Scope[ Ω ] Δ
scopeSub {Ω} ρ (sc tm) = sc (sub (λ v → str (Data.Sum.map ρ id (strict-⟦⟧ v))) tm)
-- * Example: Well-scoped, untyped lambda-calculus
module LC where
-- ** World
monFin : ∀{n m} → Fin (n + m) → Fin m ⊎ Fin n
monFin {zero} xs = inj₁ xs
monFin {suc m} zero = inj₂ zero
monFin {suc m} (suc xs) with monFin {m} xs
monFin {suc m} (suc xs) | inj₁ x = inj₁ x
monFin {suc m} (suc xs) | inj₂ y = inj₂ (suc y)
monFin⁻¹ : ∀{n m} → Fin m ⊎ Fin n → Fin (n + m)
monFin⁻¹ {n}{m} k = [ raise n , inject+ m ]′ k
ℕW : World ℕ ⊤
ℕW = record
{ _⇒_ = λ m n → Fin m → Fin n
; _⊗_ = λ m n → n + m
; inl = λ {Γ}{Δ} → raise Δ
; inr = λ {Γ}{Δ} → inject+ Γ
; ⟦_⟧ = λ n tt → Fin n
; ⟦_⟧map = λ ρ → ρ
; strict-⟦⟧ = monFin
}
-- ** Terms
Σλam : Presentation ℕ ⊤
Σλam = record { Op = λ tt → Bool
; Ar = λ { true → ⊤
; false → Bool }
; Bi = λ { {_} {true} tt → 1
; {_} {false} b → 0 }
; Ty = λ { {_} {true} tt → tt
; {_} {false} a → tt } }
open Terms ℕW Σλam
λam : ℕ → Set
λam n = Tm n tt
var : ∀{n} → Fin n → λam n
var = `var
app : ∀{n} → λam n → λam n → λam n
app f s = `op false (λ { true → sc f
; false → sc s })
abs : ∀{n} → λam (suc n) → λam n
abs b = `op true (λ { tt → sc b })
-- ** Substitution
open Subst ℕW Σλam
subst⊢ : ∀{m n} → λam m → (Fin m → λam n) → λam n
subst⊢ tm ρ = sub ρ tm
-- ** Example
tm1 : λam 0
tm1 = abs (var zero)
tm2 : λam 1
tm2 = abs (app (var (suc zero)) (var zero))
tm3 : λam 0
tm3 = subst⊢ tm2 ρ
where ρ : Fin 1 → λam 0
ρ zero = tm1
ρ (suc ())
-- * Example: well-typed lambda-calculus
module STLC where
data Typ : Set where
`■ : Typ
_`⇒_ : (A B : Typ) → Typ
-- ** World
data Ctxt : Set where
ε : Ctxt
_▹_ : Ctxt → Typ → Ctxt
data _`∈_ (T : Typ) : (Γ : Ctxt) → Set where
ze : ∀{Γ} → T `∈ (Γ ▹ T)
suc : ∀{Γ T'} → T `∈ Γ → T `∈ (Γ ▹ T')
_∷_ : Ctxt → Ctxt → Ctxt
Γ ∷ ε = Γ
Γ ∷ (Ω ▹ S) = (Γ ∷ Ω) ▹ S
monW : ∀{Ω Γ T} → T `∈ (Γ ∷ Ω) → T `∈ Γ ⊎ T `∈ Ω
monW {ε} k = inj₁ k
monW {Ω ▹ T} ze = inj₂ ze
monW {Ω ▹ x} (suc k) with monW {Ω} k
monW {Ω ▹ x₁} (suc k) | inj₁ x = inj₁ x
monW {Ω ▹ x} (suc k) | inj₂ y = inj₂ (suc y)
raiseW : ∀ {Γ} Δ → ∀{T} → T `∈ Γ → T `∈ (Γ ∷ Δ)
raiseW ε k = k
raiseW (Δ ▹ x) k = suc (raiseW Δ k)
injectW : ∀ {Γ} Δ → ∀{T} → T `∈ Γ → T `∈ (Δ ∷ Γ)
injectW Δ ze = ze
injectW Δ (suc k) = suc (injectW Δ k)
monW⁻¹ : ∀{Ω Γ T} → T `∈ Γ ⊎ T `∈ Ω → T `∈ (Γ ∷ Ω)
monW⁻¹ {Ω}{Γ} = [ raiseW Ω , injectW Γ ]′
CtxtW : World Ctxt Typ
CtxtW = record
{ _⇒_ = λ Γ Δ → ∀ {T} → T `∈ Γ → T `∈ Δ
; _⊗_ = _∷_
; inl = λ {Γ}{Δ} → raiseW {Γ} Δ
; inr = λ {Γ}{Δ} → injectW {Δ} Γ
; ⟦_⟧ = λ Γ T → T `∈ Γ
; ⟦_⟧map = λ ρ → ρ
; strict-⟦⟧ = monW
}
-- ** Terms
Σλam : Presentation Ctxt Typ
Σλam = record { Op = λ T → Typ ⊎ (Σ[ A ∈ Typ ] Σ[ B ∈ Typ ] T ≡ A `⇒ B)
; Ar = λ { (inj₁ S) → Bool
; (inj₂ (A , B , q)) → ⊤ }
; Bi = λ {T} → λ { {sh = inj₁ S} x → ε
; {sh = inj₂ (A , B , q)} tt → ε ▹ A }
; Ty = λ {T} → λ { {sh = inj₁ S} true → S `⇒ T
; {sh = inj₁ S} false → S
; {sh = inj₂ (A , B , q)} tt → B } }
open Terms CtxtW Σλam
_⊢_ : (Γ : Ctxt) → Typ → Set
Γ ⊢ T = Tm Γ T
var : ∀{Γ T} → T `∈ Γ → Γ ⊢ T
var k = `var k
app : ∀{Γ S T} → Γ ⊢ (S `⇒ T) → Γ ⊢ S → Γ ⊢ T
app {S = S} f s = `op (inj₁ S) (λ { true → sc f
; false → sc s })
abs : ∀{Γ S T} → (Γ ▹ S) ⊢ T → Γ ⊢ (S `⇒ T)
abs {S = S}{T = T} b = `op (inj₂ (S , T , refl))
(λ { tt → sc b })
-- ** Substitution
open Subst CtxtW Σλam
subst⊢ : ∀{Γ Δ T} → Γ ⊢ T → (∀{T} → T `∈ Γ → Δ ⊢ T) → Δ ⊢ T
subst⊢ tm ρ = sub ρ tm
-- ** Example
tm1 : ε ⊢ (`■ `⇒ `■)
tm1 = abs (var ze)
tm2 : (ε ▹ (`■ `⇒ `■)) ⊢ (`■ `⇒ `■)
tm2 = abs (app (var (suc ze)) (var ze))
tm3 : ε ⊢ (`■ `⇒ `■)
tm3 = subst⊢ tm2 ρ
where ρ : ∀{T} → T `∈ (ε ▹ (`■ `⇒ `■)) → ε ⊢ T
ρ ze = tm1
ρ (suc ())
-- test : tm3 ≡ abs (app (abs (var ze)) (var ze))
-- test = {!!}
{-
-- * Example: System F
module F where
-- ** World
monFin : ∀{n m} → Fin (n + m) → Fin m ⊎ Fin n
monFin {zero} xs = inj₁ xs
monFin {suc m} zero = inj₂ zero
monFin {suc m} (suc xs) with monFin {m} xs
monFin {suc m} (suc xs) | inj₁ x = inj₁ x
monFin {suc m} (suc xs) | inj₂ y = inj₂ (suc y)
monFin⁻¹ : ∀{n m} → Fin m ⊎ Fin n → Fin (n + m)
monFin⁻¹ {n}{m} k = [ raise n , inject+ m ]′ k
ℕW : World ⊤ ℕ
ℕW = record { ⟦_⟧ = λ n tt → Fin n
; _⊗_ = λ m n → n + m
; mon⟦⟧ = monFin
; mon⟦⟧⁻¹ = monFin⁻¹ }
-- ** Terms
data FTy : Set where
base arrow forll : FTy
ΣFTy : Presentation ℕ ⊤
ΣFTy = record { Op = λ tt → FTy
; Ar = λ { base → ⊥
; arrow → Bool
; forll → ⊤ }
; Bi = λ { {_} {base} b → 0
; {_} {arrow} b → 0
; {_} {forll} b → 1 }
; Ty = λ _ → tt }
module Ty where
open Terms ℕW ΣFTy
Ty : ℕ → Set
Ty n = Tm n tt
tvar : ∀{n} → Fin n → Ty n
tvar = `var
_`⇒_ : ∀{n} → Ty n → Ty n → Ty n
σ `⇒ τ = `op arrow (λ { true → sc σ
; false → sc τ })
`∀ : ∀{n} → Ty (suc n) → Ty n
`∀ τ = `op forll (λ { tt → sc τ })
open Ty
-- ** Substitution
subst⊢ : ∀{m n} → Ty m → (Fin m → Ty n) → Ty n
subst⊢ tm ρ = sub ρ tm
where open Subst ℕW ΣFTy
-- ** Term World
data Ctxt (n : ℕ) : Set where
ε : Ctxt n
_▹_ : Ctxt n → Ty n → Ctxt n
data _`∈_ {n} (T : Ty n) : (Γ : Ctxt n) → Set where
ze : ∀{Γ} → T `∈ (Γ ▹ T)
suc : ∀{Γ T'} → T `∈ Γ → T `∈ (Γ ▹ T')
weakenCtxt : ∀{n} → Ctxt n → Ctxt (1 + n)
weakenCtxt ε = ε
weakenCtxt (Γ ▹ T) = weakenCtxt Γ ▹ mapTm suc T
where open Subst ℕW ΣFTy
∫Γ : Set
∫Γ = Σ[ n ∈ ℕ ] Ctxt n
∫T : Set
∫T = Σ[ n ∈ ℕ ] Ty n
_∷_ : ∫Γ → ∫Γ → ∫Γ
Γ ∷ Δ = {!!}
∫GW : World (Σ ℕ Ty) ∫Γ
∫GW = record { ⟦_⟧ = λ { (n , Γ) (k , T) → Σ[ q ∈ k ≡ n ] subst Ty q T `∈ Γ }
; _⊗_ = _∷_
; mon⟦⟧ = {!!}
; mon⟦⟧⁻¹ = {!!} }
bind : ∀{n} → (σ : Ty n)(τ : Ty (1 + n)) → Ty n
bind σ τ = subst⊢ τ (λ { zero → σ ; (suc k) → tvar k })
data FTm (n : ℕ)(τ' : Ty n) : Set where
`abs : (σ : Ty n)(τ : Ty n)(q : τ' ≡ σ `⇒ τ) → FTm n τ'
`app : (σ : Ty n) → FTm n τ'
`tabs : (τ : Ty (1 + n))(q : τ' ≡ `∀ τ) → FTm n τ'
`tapp : (σ : Ty n)(τ : Ty (1 + n))(q : τ' ≡ bind σ τ) → FTm n τ'
ΣFTm : Presentation ∫Γ ∫T
ΣFTm = record { Op = λ { (n , τ') → FTm n τ' }
; Ar = λ { {(n , τ')} (`abs σ τ q) → ⊤
; {(n , τ)} (`app σ) → Bool
; {(n , τ')} (`tabs τ q) → ⊤
; {(n , τ')} (`tapp σ τ q) → ⊤ }
; Bi = λ { {(n , τ')} {`abs σ τ q} tt → n , (ε ▹ σ)
; {(n , τ)} {`app σ} true → (n , ε)
; {(n , τ)} {`app σ} false → n , ε
; {(n , τ')} {`tabs τ q} tt → 1 + n , ε
; {(n , τ')} {`tapp σ τ q} tt → n , ε }
; Ty = λ { {(n , τ')} {`abs σ τ q} tt → n , τ
; {(n , τ)} {`app σ} true → n , σ `⇒ τ
; {(n , τ)} {`app σ} false → n , σ
; {(n , τ')} {`tabs τ q} tt → 1 + n , τ
; {(n , τ')} {`tapp σ τ q} tt → n , `∀ τ } }
module Tm where
open Terms ∫GW ΣFTm
_⊢_ : {m : ℕ} → Ctxt m → Ty m → Set
_⊢_ {n} Γ T = Tm (n , Γ) (n , T)
var : ∀{n}{Γ : Ctxt n}{τ : Ty n} → τ `∈ Γ → Γ ⊢ τ
var k = `var (refl , k)
lam : ∀{n}{Γ : Ctxt n}{σ τ : Ty n} → (Γ ▹ σ) ⊢ τ → Γ ⊢ (σ `⇒ τ)
lam {σ = σ}{τ = τ} b = `op (`abs σ τ refl) (λ { tt → sc b })
app : ∀{n}{Γ : Ctxt n}{σ τ : Ty n} → Γ ⊢ (σ `⇒ τ) → Γ ⊢ σ → Γ ⊢ τ
app {σ = σ} f s = `op (`app σ) (λ { true → sc f
; false → sc s })
tlam : ∀{n}{Γ : Ctxt n}{τ : Ty (1 + n)} → weakenCtxt Γ ⊢ τ → Γ ⊢ `∀ τ
tlam {τ = τ} f = `op (`tabs τ refl) (λ { tt → sc f })
tapp : ∀{n}{Γ : Ctxt n}{σ : Ty n}{τ : Ty (1 + n)} → Γ ⊢ `∀ τ → Γ ⊢ bind σ τ
tapp {σ = σ}{τ = τ} t = `op (`tapp σ τ refl) (λ { tt → sc t })
open Tm
-- * Outro
-- Local Variables:
-- mode: outline-minor
-- outline-regexp: "-- [*\f]+"
-- outline-level: outline-level
-- End:
-}