coqdoc for interp.v and sem_type_formers.v

theories/interp.v

 From tutorial_popl20 Require Export sem_type_formers types.
 
+(** * Here we use semantic type formers to define semantics of syntactic types.
+
+    This is done by a straightforward induction on the syntactic type.  *)
+
 Reserved Notation "⟦ τ ⟧".
 Fixpoint interp `{heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
   match τ return _ with

theories/sem_type_formers.v

 From tutorial_popl20 Require Export sem_types.
 
-(** The definitions of the type formers *)
+(** * The definitions of the semantic type formers
+
+    These type formers correspond to those of syntactic types, e.g., a
+    product former that given two semantic types [A] and [B], gives
+    the semantic type of the product [A * B], i.e., values that are
+    pairs where the first component belongs to [A] and the second
+    component to [B]. *)
 Section types.
   Context `{heapG Σ}.
 
@@ -25,17 +31,76 @@ Section types.
   (* REMOVE *) Definition sem_ty_sum (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
     (∃ w1, ⌜w = InjLV w1⌝ ∧ A1 w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ A2 w2))%I.
 
+  (** The value interpretation for function types is as follows: *)
   Definition sem_ty_arr (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
     □ ∀ v, A1 v -∗ WP App w v {{ A2 }})%I.
+  (** This definition is very close to the usual way of defining the
+      value interpretation of the function type [A1 → A2] in ordinary
+      logical relations: it expresses that arguments of semantic type
+      [A1] are mapped to results of semantic type [A2] . The only Iris
+      specific feature one has to take into account is the [□]
+      modality. Recall that the value interpretation should be a
+      persistent predicate; however, even if both [P] and [Q] are
+      persistent propositions, the magic wand [P -∗ Q] is not
+      necessarily persistent. Hence, we use the [□] modality to make
+      the magic wand persistent. *)
+
+
 
+  (** The value interpretation for type variables, universal types,
+      and existential types is: *)
   Definition sem_ty_forall (C : sem_ty Σ → sem_ty Σ) : sem_ty Σ := SemTy (λ w,
     □ ∀ A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
   Definition sem_ty_exist (C : sem_ty Σ → sem_ty Σ) : sem_ty Σ := SemTy (λ w,
     ∃ A : sem_ty Σ, C A w)%I.
+  (** The interpretations of these types are fairly straightforward.
+      Given a higher-order type former [C] that maps semantic types to
+      semantic types, we define the universal type [sem_ty_forall A]
+      using the universal quantification in Iris. That is, a value [w]
+      is considered a polymorphic value if for any semantic type [A],
+      when [w] is specialized to the type [A] (written as [w #()] as
+      (semantic) types never appear in terms in our untyped syntax)
+      the _resulting expression_ is an expression in the semantics of
+      the type [C A] (defined using WP).
+
+      Similarly, given a higher-order type former [C] that maps
+      semantic types to semantic types, we define the existential type
+      [sem_ty_exist A] using the existential quantification in Iris.
+
+      Notice how the impredicative nature of Iris propositions and
+      predicates allows us to quantify over Iris predicates to define
+      an Iris predicate. This is crucial for giving semantics to
+      parametric polymorphism, i.e., universal and existential types.
 
+      Remark: notice that for technical reasons (related to the value
+      restriction problem in ML-like languages) universally quantified
+      expressions are not evaluated until they are applied to a
+      specific type. *)
+
+  (** The value interpretation of reference types is as follows: *)
   Definition tyN := nroot .@ "ty".
   Definition sem_ty_ref (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
     ∃ l : loc, ⌜w = #l⌝ ∧ inv (tyN .@ l) (∃ v, l ↦ v ∗ A v))%I.
+  (** Intuitively, values of the reference type [sem_ty_ref A] should
+     be locations l that hold a value [w] in the semantic type [A] at
+     all times. In order to express this intuition in a formal way, we
+     make use of two features of Iris:
+
+     - The points-to connective l ↦ v (from vanilla separation logic)
+       provides exclusive ownership of the location l with value
+       v. The points-to connective is an ephemeral proposition, and
+       necessarily not a persistent proposition.
+
+     - The invariant assertion [inv N P] expresses that a (typically
+       ephemeral) proposition [P] holds at all times -- i.e., [P] is
+       invariant. The invariant assertion is persistent. *)
+
+  (** Remark: Iris is also capable giving semantics to recursive
+   types. However, for the sake of simplicity we did not consider
+   recursive types for this tutorial. In particular, to give the
+   semantics of recursive types one needs to use Iris's guarded
+   fixpoints which in turn requires us to enforce that semantics types,
+   in addition to being persistent, are also non-expansive. *)
 End types.
 
 (** We introduce nicely looking notations for our semantic types. This allows