Type former tweaks.

exercises/sem_type_formers.v

@@ -45,7 +45,9 @@ former for the function type [A1 → A2] in traditional logical relations: it
 expresses that arguments of semantic type [A1] are mapped to results of
 semantic type [A2]. The definition makes two of two features of Iris:
 
-- The weakest precondition [WP e {{ Φ }}].
+- The weakest precondition [WP e {{ Φ }}]. We have already seen weakest
+  preconditions before (in the file [language.v]). We use them in the semantics
+  of functions to talk about the result of the expression [v w].
 - The persistence modality [□]. Recall that semantic types are persistent Iris
   predicates. However, even if both [P] and [Q] are persistent propositions,
   the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
@@ -54,58 +56,53 @@ semantic type [A2]. The definition makes two of two features of Iris:
 
 (** * Polymorphism and existentials *)
 Definition sem_ty_forall `{!heapG Σ} (C : sem_ty Σ → sem_ty Σ) : sem_ty Σ := SemTy (λ w,
-  □ ∀ A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
+  □ ∀ 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 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 quantifier of
+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 <_>] (see the
+file [polymorphism.v]) 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.
+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 quantifier of 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.
+Notice how the impredicative nature of Iris propositions and predicates allow
+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. *)
+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. *)
 
 (** * References *)
 Definition tyN := nroot .@ "ty".
 Definition sem_ty_ref `{!heapG Σ} (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.
+(** 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 require some additional bookkeeping related to
-contractiveness. *)
+(** 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 require some additional bookkeeping related
+to contractiveness. *)
 
 (** We introduce nicely looking notations for our semantic types. This allows
 us to write lemmas, for example, the compatibility lemmas, in a readable way. *)

solutions/sem_type_formers.v

@@ -45,7 +45,9 @@ former for the function type [A1 → A2] in traditional logical relations: it
 expresses that arguments of semantic type [A1] are mapped to results of
 semantic type [A2]. The definition makes two of two features of Iris:
 
-- The weakest precondition [WP e {{ Φ }}].
+- The weakest precondition [WP e {{ Φ }}]. We have already seen weakest
+  preconditions before (in the file [language.v]). We use them in the semantics
+  of functions to talk about the result of the expression [v w].
 - The persistence modality [□]. Recall that semantic types are persistent Iris
   predicates. However, even if both [P] and [Q] are persistent propositions,
   the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
@@ -54,58 +56,53 @@ semantic type [A2]. The definition makes two of two features of Iris:
 
 (** * Polymorphism and existentials *)
 Definition sem_ty_forall `{!heapG Σ} (C : sem_ty Σ → sem_ty Σ) : sem_ty Σ := SemTy (λ w,
-  □ ∀ A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
+  □ ∀ 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 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 quantifier of
+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 <_>] (see the
+file [polymorphism.v]) 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.
+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 quantifier of 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.
+Notice how the impredicative nature of Iris propositions and predicates allow
+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. *)
+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. *)
 
 (** * References *)
 Definition tyN := nroot .@ "ty".
 Definition sem_ty_ref `{!heapG Σ} (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.
+(** 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 require some additional bookkeeping related to
-contractiveness. *)
+(** 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 require some additional bookkeeping related
+to contractiveness. *)
 
 (** We introduce nicely looking notations for our semantic types. This allows
 us to write lemmas, for example, the compatibility lemmas, in a readable way. *)