stlc-model1.agda

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

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.

Thanks! Yeah I called it Base in the theory for this reason, and even interpret it as Nat later. Not sure why I called it unit there.On Nov 16, 2023, at 05:49, Jacques Carette ***@***.***> wrote:Re: ***@***.*** commented on this gist.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.—Reply to this email directly, view it on GitHub or unsubscribe.You are receiving this email because you authored the thread.Triage notifications on the go with GitHub Mobile for iOS or Android.