what-is-an-intensional-model.org

Term Model

CBPV

A judgmental cbpv model is

1. A cartesian category 𝓒 of “pure functions”
2. A subset of the objects of 𝓒 called the “value types”
3. A 𝓟𝓒-enriched category 𝓔 of “linear functions”, whose objects are “computation types”
4. 𝓟𝓒-enriched presheaf W on 𝓔

Type structure:

1. 𝓒 has product types if the value types are closed under products
2. 𝓒 has pure function types if the vtypes are closed under exponentials
3. 𝓒 has sum types if the value types are closed under distributive coproducts
4. 𝓒 has a ▹ type if for every A ∈ VType, the presheaf P(Γ) = ▹ (𝓒 [ Γ , A ]) is representable
5. 𝓒 has linear function types if every Hom_𝓔(B,B’) is representable
6. 𝓒 has thunks if every W B is representable

Similarly:

1. 𝓔 has function types if it has powers of 𝓒-types
2. 𝓔 has returners if for every vtype A, the enriched covariant presheaf Q(B)_Γ = W B (Γ × A) is (enriched) representable
3. 𝓔 has product types if it has enriched products
4. 𝓔 has

This isn’t quite right tho, because W needs to respect the powers…

Alt

A judgmental cbpv model is

1. A cartesian category 𝓒 of “pure functions”
2. A distinguished subset of 𝓒 objects called “value types”
3. A 𝓟 𝓒-enriched category 𝓔 of “linear functions”
4. A distinguished object W ∈ 𝓔 of “machines”
5. A distinguished subset of 𝓔 objects called “computation types”

CBV/CBN

Special cases:

1. a judgmental cbv model is
   • A cartesian category 𝓒
   • A subset of types, which determines a 𝓟𝓒-enriched category 𝓣
   • A 𝓟𝓒-enriched presheaf 𝓔 on 𝓣
   • A 𝓟𝓒-enriched promonad structure on 𝓣 with underlying profunctor: (𝓛 A B) Γ = 𝓔 B (Γ × A)

   From this data, we can generate a cbpv model with 𝓒 as the cartesian category and defining a “Kleisli” category whose objects are 𝓣 + 1 with (𝓔 (inl A) B) Γ = 𝓛 A B Γ (𝓔 (inr *) B) Γ = 𝓔 Γ B

   This can be generated for instance from

   • A cartesian category 𝓒 and a strong monad T on 𝓒
2. a judgmental cbn model is
   • A cartesian category 𝓒
   • a subset of types determining a wide subcategory 𝓣
   • A subcategory? 𝓛 of 𝓣 of “linear” functions or should it be a procomonad?

   This can be generated for instance from a cartesian category 𝓒 and a (strong?) comonad W on 𝓒

3. A cartesian category 𝓒 of contexts and “pure functions”
4. Chosen subsets of the objects of 𝓒 called “types”
5. For each type A ∈ Types, a presheaf Eff A ∈ 𝓟 𝓒
   1. A natural element ret ∈ Y A ⇒ Eff A
   2. A natural transformation bind ∈ (Y A ⇒ Eff B) ⇒ Eff A ⇒ Eff B
   3. satisfying …

Relational Model

To get a “relational” model, take the above and do it all internal to Cat. To make it more like relations, we should require it to be 2-posetal (i.e. at most one 2-cell) and be fibrant (i.e., functions induce relations).

This is all in the internal language of the topos of trees.

An intensional cbv λ model with relations consists of:

1. A double category 𝓒 that is cartesian, locally posetal and fibrant.
2. A chosen subset of objects of 𝓒 called types.
3. For each type A ∈ Types, a double presheaf that is locally posetal and fibrant

1. A cartesian locally posetal double category 𝓒.

   Locally posetal means that there is at most one two cell of any given framing.

   Cartesian means it has finite products

2. A locally posetal double category of types and effectful morphisms 𝓔

1. A locally posetal double profunctor Tm : 𝓒 o-* Eff