Skip to content

Instantly share code, notes, and snippets.

@wilbowma
Created November 16, 2023 02:20
Show Gist options
  • Save wilbowma/abfaa0cec56ff55ed25326497da20582 to your computer and use it in GitHub Desktop.
Save wilbowma/abfaa0cec56ff55ed25326497da20582 to your computer and use it in GitHub Desktop.
open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
-- A notion of model of STLC
-- A Theory for STLC
-- A Syntax (of closed terms) for STLC
record Theory {l k : Level} : Set (lsuc (l ⊔ k)) where
field
-- Terms
Tm : Set k
-- Types
Ty : Set l
-- A typing relation
_∈_ : Tm -> Ty -> Set (l ⊔ k)
-- A representation of False, required if I wish to prove consistency as a logic.
False : Ty
False-uninhabit : ∀ M -> ¬ (M ∈ False)
Base : Ty
base : Tm
app : Tm -> Tm -> Tm
lam : Ty -> (Tm -> Tm) -> Tm
Fun : Ty -> Ty -> Ty
-- Semantic typing of closed terms
Fun-I : ∀ {A f B} ->
(∀ {x} -> (x ∈ A) -> ((f x) ∈ B)) ->
------------------------------
((lam A f) ∈ (Fun A B))
Fun-E : ∀ {M N A B} ->
(M ∈ (Fun A B)) -> (N ∈ A) ->
------------------------------
(app M N) ∈ B
Base-I :
-----------
base ∈ Base
-- should have some equations here if I care about, you know, terms
_≡lc_ : ∀ {e e' A} -> (e ∈ A) -> (e' ∈ A) -> Set (l ⊔ k)
-- equations are actually only about well-typed terms, or derivations, or ..
-- representations of terms?
Fun-β : ∀ {e A B} {f : Tm -> Tm} ->
(Df : (∀ {x : Tm} -> (x ∈ A) -> ((f x) ∈ B))) ->
(Da : (e ∈ A)) ->
---------------------------------
(Fun-E (Fun-I Df) Da) ≡lc (Df Da)
Fun-η : ∀ {e A B} ->
(Df : (e ∈ Fun A B)) ->
---------------------------------
Df ≡lc (Fun-I (λ x -> (Fun-E Df x)))
-- How do we work with this syntax?
-- Well, for an arbirary model...
module Test {l k : Level} (model : Theory {l} {k}) where
open Theory (model)
-- well-typed unit
example1 : base ∈ Base
example1 = Base-I
-- the Base -> Base function
example2 : (lam Base (λ x -> x)) ∈ (Fun Base Base)
example2 = Fun-I (λ x -> x)
-- application of it
example3 : (app (lam Base (λ x -> x)) base) ∈ Base
example3 = Fun-E (Fun-I (λ x -> x)) Base-I
-- Let's build some models.
module Model where
-- I'll represent types as syntactic types...
data STLC-Type : Set where
STLC-False : STLC-Type
STLC-Unit : STLC-Type
STLC-Fun : STLC-Type -> STLC-Type -> STLC-Type
-- And well-typed terms as terms of the corresponding Agda type
El : STLC-Type -> Set
El STLC-False = ⊥
El STLC-Unit = ⊤
El (STLC-Fun A B) = El A -> El B
open Theory {{...}}
instance
-- M is a model of the Theory
M : Theory
-- terms don't matter; only derivations do
-- this is kind of weird.. but kind of not?
Tm {{M}} = ⊤
Ty {{M}} = STLC-Type
-- the typing relation is actually the interpretation of
-- syntactically well-typed terms as terms of the corresponding Agda type
_∈_ ⦃ M ⦄ e = El
False {{M}} = STLC-False
False-uninhabit ⦃ M ⦄ = λ M₁ z → z
Base {{M}} = STLC-Unit
base {{M}} = tt
Base-I {{M}} = tt
Fun {{M}} = STLC-Fun
lam {{M}} A f = tt
app {{M}} e1 e2 = tt
-- Function introduction introduces an Agda function
Fun-I {{M}} Df = λ x -> Df x
-- Function elimination applies the underlying Agda function
Fun-E {{M}} D1 D2 = D1 D2
-- syntactic equality is propositional equality, and validates β/η
_≡lc_ {{M}} = _≡_
Fun-β {{M}} = λ Df Da → refl
Fun-η {{M}} = λ Df → refl
-- Now we compile some of our examples to Agda using this model
module TestAgda = Test M
test1 : ⊤
test1 = TestAgda.example1
test2 : ⊤
test2 = TestAgda.example2 tt
-- A new model where we interpret Base as Nat
El' : STLC-Type -> Set
El' STLC-False = ⊥
El' STLC-Unit = ℕ
El' (STLC-Fun A B) = El' A -> El' B
open Theory {{...}}
instance
M' : Theory
Tm {{M'}} = ⊤
Ty {{M'}} = STLC-Type
_∈_ ⦃ M' ⦄ e = El'
False {{M'}} = STLC-False
False-uninhabit ⦃ M' ⦄ = λ M₁ z → z
Base {{M'}} = STLC-Unit
base {{M'}} = tt
Base-I {{M'}} = 120 -- the base value is an arbitrary natural number
Fun {{M'}} = STLC-Fun
lam {{M'}} A f = tt
app {{M'}} e1 e2 = tt
Fun-I {{M'}} Df = λ x -> Df x
Fun-E {{M'}} D1 D2 = D1 D2
_≡lc_ {{M'}} = _≡_
Fun-β {{M'}} = λ Df Da → refl
Fun-η {{M'}} = λ Df → refl
-- Now we compile some of our examples to Agda using this model
module TestAgda' = Test M'
test1' : ℕ
test1' = TestAgda'.example1
-- interestingly, there are *more* base values in the model than in the theory
test2' : ℕ
test2' = TestAgda'.example2 5
@JacquesCarette
Copy link

Calling it STLC-Unit is misleading, as it is unconstrained to be anything. It is "just a type", and is not constrained to have a single inhabitant by any of your rules as far as I can tell.

@wilbowma
Copy link
Author

wilbowma commented Nov 16, 2023 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment