meeting notes and agdaize cbpv judgmental structure

code/cbpv.agda

+module CBPV (Σv : Set) (Σc : Set) where
+
+open import Data.Maybe
+open import Relation.Binary.PropositionalEquality
+
+data VType : Set
+data CType : Set
+
+data VType where
+  base : Σv -> VType
+
+data CType where
+  base : Σc -> CType
+
+data Nat : Set where
+  O : Nat
+  S : Nat -> Nat
+
+data Fin : Nat -> Set where
+  fO : ∀ n -> Fin (S n)
+  fS : ∀ n -> Fin n -> Fin (S n)
+
+record Iso (A B : Set) : Set where
+  field
+    to : A -> B
+    fro : B -> A
+    sect : ∀ (a : A) -> fro (to a) ≡ a
+    retr : ∀ (b : B) -> to (fro b) ≡ b
+
+record FinSet : Set₁ where
+  field
+    X : Set
+    card : Nat
+    is-finite : Iso X (Fin card)
+
+VCtx : FinSet -> Set
+VCtx U = FinSet.X U -> VType
+
+record VCCtx (U : FinSet) : Set where
+  constructor _/_
+  field
+    vvars : VCtx U
+    stoup : Maybe CType
+
+ValSig : Set₁
+ValSig = ∀ {U} -> VCtx U -> VType -> Set
+
+CompSig : Set₁
+CompSig = ∀ {U} -> VCCtx U -> CType -> Set
+
+module Terms (Σtmv : ValSig) (Σtmc : CompSig) where
+
+  data _|-v_ {U} (Γ : VCtx U) : VType -> Set₁
+  data _|-c_ {U} : (ΓH : VCCtx U) -> CType -> Set₁
+  val-subst : ∀ U V -> VCtx U -> VCtx V -> Set₁
+  data _|-mayc_ : ∀ {U} -> VCCtx U -> Maybe CType -> Set₁
+  record comp-subst U V (ΓH : VCCtx U) (ΔH : VCCtx V) : Set₁
+
+  data _|-v_ {U} (Γ : VCtx U) where
+    var  : ∀ (u : FinSet.X U) -> Γ |-v (Γ u)
+    base : ∀ V (Δ : VCtx V) A (f : Σtmv {V} Δ A) -> val-subst U V Γ Δ -> Γ |-v A
+  data _|-c_ {U} where
+    hole : ∀ (Γ : VCtx U) B -> (Γ / just B) |-c B
+    base : ∀ (ΓH : VCCtx U) V (ΔH : VCCtx V) B (p : Σtmc {V} ΔH B) -> comp-subst U V ΓH ΔH -> ΓH |-c B
+  val-subst U V Γ Δ    = ∀ (v : FinSet.X V) -> _|-v_ {U} Γ (Δ v)
+  data _|-mayc_ where
+    done : ∀ U (ΓH : VCCtx U)-> ΓH |-mayc nothing
+    one  : ∀ U (ΓH : VCCtx U) B -> ΓH |-c B -> ΓH |-mayc (just B)
+  record comp-subst U V ΓH ΔH where
+    inductive
+    field
+      vsubst : val-subst U V (VCCtx.vvars ΓH) (VCCtx.vvars ΔH)
+      csubst : ΓH |-mayc (VCCtx.stoup ΔH)
+
+  vv-substitute : ∀ U V (Γ : VCtx U)(Δ : VCtx V) A -> val-subst U V Γ Δ -> Δ |-v A -> Γ |-v A
+  vv-compose : ∀ U V W (Γ : VCtx U) (Δ : VCtx V) (E : VCtx W) -> val-subst W V E Δ -> val-subst V U Δ Γ -> val-subst W U E Γ
+  vv-substitute U V Γ Δ .(Δ u) δ (var u) = δ u
+  vv-substitute U V Γ Δ A δ (base V₁ Δ' .A f δ') = base V₁ Δ' A f (vv-compose V₁ V U _ _ _ δ δ')
+  vv-compose U V W Γ Δ E δ γ = λ v → vv-substitute _ _ _ _ _ δ (γ v)

notes/meeting-04-06-2018.org

+* Where We're At
+  - CBN GTT was accepted to FSCD! Need to work on the final draft
+  - LR for CBV GTT is submitted to ICFP
+  - What is CBV GTT?
+    - Current Idea: We have values and terms, and we hvae "value type
+      dynamism" and "term type dynamism"
+    - Term Type Dynamism gives us an ep pair of terms
+    - Value Type Dynamism gives us an ep pair of values
+    - Value Type Dynamism *implies* Term Type Dynamism, return
+      preserves the ep pair
+  - Should we be doing CBPV GTT instead?