STLC.agda

{-

Dependently typed metaprogramming (in Agda)
Conor McBride, 2013

Dependently typed programming
Conor McBride, 2011

-}

module STLC where


{----------------------------------------------------------------------------

1. Equipment

-}


record One : Set where
  constructor <>
open One public


record Σ (S : Set) (T : S → Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Σ public

_×_ : Set → Set → Set
S × T = Σ S \_ → T


data 𝐍 : Set where
  zero : 𝐍
  succ : 𝐍 → 𝐍
{-# BUILTIN NATURAL 𝐍 #-}


{----------------------------------------------------------------------------

2.1. Syntax

-}


infixr 5 _⊃_
infixl 4 _,_
infix 3 _∈_
infix 3 _⊢_


-- Types, including a base type, closed under function spaces.

data Ty : Set where
  ι   : Ty
  _⊃_ : Ty → Ty → Ty


-- Contexts, as snoc-lists.

data Cx (X : Set) : Set where
  ε   : Cx X
  _,_ : Cx X → X → Cx X


-- Typed de Bruijn indices to be context membership evidence.

data _∈_ (τ : Ty) : Cx Ty → Set where
  zero : ∀{Γ}           → τ ∈ Γ , τ
  succ : ∀{Γ σ} → τ ∈ Γ → τ ∈ Γ , σ


-- Well-typed terms, by writing syntax-directed rules for the typing judgment.

data _⊢_ (Γ : Cx Ty) : Ty → Set where
  var : ∀{τ}   → τ ∈ Γ
               → Γ ⊢ τ
  lam : ∀{σ τ} → Γ , σ ⊢ τ
               → Γ ⊢ σ ⊃ τ
  app : ∀{σ τ} → Γ ⊢ σ ⊃ τ → Γ ⊢ σ
               → Γ ⊢ τ


{----------------------------------------------------------------------------

2.2. Semantics

-}


⟦_⟧Ty : Ty → Set
⟦ ι ⟧Ty     = 𝐍
⟦ σ ⊃ τ ⟧Ty = ⟦ σ ⟧Ty → ⟦ τ ⟧Ty


⟦_⟧Cx : Cx Ty → (Ty → Set) → Set
⟦ ε ⟧Cx     V = One
⟦ Γ , σ ⟧Cx V = ⟦ Γ ⟧Cx V × V σ


⟦_⟧∈ : ∀{τ Γ V} → τ ∈ Γ → ⟦ Γ ⟧Cx V → V τ
⟦ zero ⟧∈   (γ , t) = t
⟦ succ i ⟧∈ (γ , s) = ⟦ i ⟧∈ γ


⟦_⟧⊢ : ∀{Γ τ} → Γ ⊢ τ → ⟦ Γ ⟧Cx ⟦_⟧Ty → ⟦ τ ⟧Ty
⟦ var i ⟧⊢   γ = ⟦ i ⟧∈ γ
⟦ lam t ⟧⊢   γ = \s → ⟦ t ⟧⊢ ( γ , s )
⟦ app f s ⟧⊢ γ = ⟦ f ⟧⊢ γ (⟦ s ⟧⊢ γ)