* 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 𝓔 3. A locally posetal double profunctor Tm : 𝓒 o-* Eff