STLC in Agda, but with string variables and shadowing, instead of de Bruijn.

STLC_with_vars.agda

open import Data.String
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Function
open import Data.List
open import Data.Product  
open import Relation.Nullary
open import Data.Unit hiding (_≟_)
open import Data.Empty
open import Data.Bool hiding (_≟_) 
import Level as L

data Type : Set where
  unit : Type
  _⇒_  : Type → Type → Type

Name Cxt : Set
Name = String
Cxt  = List (Name × Type)

infixr 5 _⇒_ _$'_
 
in-scope : Cxt → Name → Bool
in-scope Γ n = foldr (λ x → _∨_ ⌊ proj₁ x ≟ n ⌋) false Γ

lookup : ∀ Γ n → T (in-scope Γ n) → Type
lookup [] n ()
lookup ((n' , τ) ∷ Γ) n p with n' ≟ n 
... | yes _ = τ
... | no  _ = lookup Γ n p

data Term (Γ : Cxt) : Type → Set where
  unit : Term Γ unit
  var  : ∀ n {p} → Term Γ (lookup Γ n p) 
  λ'   : ∀ {a b} n → Term ((n , a) ∷ Γ) b → Term Γ (a ⇒ b)
  _$'_ : ∀ {a b} → Term Γ (a ⇒ b) → Term Γ a → Term Γ b

⟦_⟧ : Type → Set
⟦ unit  ⟧ = ⊤
⟦ a ⇒ b ⟧ = ⟦ a ⟧ → ⟦ b ⟧

⟦_⟧ᶜ : Cxt → Set
⟦ []          ⟧ᶜ = ⊤
⟦ (_ , τ) ∷ Γ ⟧ᶜ = ⟦ Γ ⟧ᶜ × (Name × ⟦ τ ⟧)

⟦_⟧ᵛ : ∀ {Γ}(v : ∃ (T ∘ in-scope Γ)) → ⟦ Γ ⟧ᶜ → ⟦ uncurry (lookup Γ) v ⟧
⟦_⟧ᵛ {[]} (n , ())
⟦_⟧ᵛ {(n' , τ) ∷ Γ} (n , p) with n' ≟ n
... | yes _ = proj₂ ∘ proj₂
... | no  _ = ⟦ n , p ⟧ᵛ ∘ proj₁

⟦_⟧ᵗ : ∀ {Γ τ} → Term Γ τ → (⟦ Γ ⟧ᶜ → ⟦ τ ⟧) 
⟦ unit      ⟧ᵗ = const tt
⟦ var n {p} ⟧ᵗ = ⟦ n , p ⟧ᵛ
⟦ λ' n t    ⟧ᵗ = λ Γ v → ⟦ t ⟧ᵗ (Γ , (n , v))
⟦ f $' x    ⟧ᵗ = ⟦ f ⟧ᵗ ˢ ⟦ x ⟧ᵗ

ID : Term [] (unit ⇒ unit)
ID = λ' "x" (var "x")

AP : Term [] ((unit ⇒ unit) ⇒ unit ⇒ unit)
AP = λ' "f"  $ λ' "x" $ var "f" $' var "x"

-- name shadowing!
CONST : Term [] ((unit ⇒ unit) ⇒ unit ⇒ unit)
CONST = λ' "x" $ λ' "x" $ var "x"