-
-
Save hardentoo/b19a78df4f685a320c3624492e4b881d to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- | |
| 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 ⟧⊢ γ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment