Commit baeb2210 authored by Robbert Krebbers's avatar Robbert Krebbers

More comments.

parent db309714
......@@ -23,7 +23,7 @@ Section types.
(** The value interpretation for product type is as one would expect: *)
Definition sem_ty_prod (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
w1 w2, w = PairV w1 w2 A1 w1 A2 w2)%I.
w1 w2, w = (w1, w2)%V A1 w1 A2 w2)%I.
(** Values of the product type over [A1] and [A2] should be tuples [(w1, w2)],
where [w1] and [w2] should be in the interpretation of [A1] and [A2],
respectively. *)
......
......@@ -2,50 +2,64 @@ From tutorial_popl20 Require Export polymorphism.
From iris.heap_lang Require Export proofmode.
From iris.base_logic.lib Require Export invariants.
(** * The domain of semantics types. *)
(** Here we define the domain of semantics types as persistent Iris
predicates over values. That is, to capture the semantics of a
type [τ], we need to define what expressions belong to the
semantics of [τ]. We do this in two steps:
(** * Semantics types *)
(** In the file [types.v] we defined types syntactically, i.e. using the
inductive definition [ty] that enumerated the possible types. In semantic
typing, we take a more "extensional" view of typing---we model semantics types
as predicates over values, which describe what values belong to the type. In
this file, we define the type [sem_ty], together with some boilerplate for
various Coq related boilerplate. In the file [sem_type_formers.v] we then define
combinators on [sem_ty] for the various type formers. For example:
- We define what values semantically belong to type [τ]. We do
this in the file [sem_type_formers].
- We define the expressions that semantically belong to [τ]. An
expression [e] semantically belongs to type [τ] if [e] is
_safe_, and whenever it evaluates to a value [v], [v]
semantically belongs to [τ]. We do this in the file [sem_typed].
<<
Definition sem_ty_unit : sem_ty Σ := SemTy (λ w, ⌜ w = #() ⌝)%I.
Definition sem_ty_prod (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
∃ w1 w2, ⌜w = (w1, w2)%V⌝ ∧ A1 w1 ∧ A2 w2)%I.
>>
Here we use Iris predicates as value semantics of types. The power
of Iris's logic then allows us to define many semantic types
including those that we need to interpret syntactic types for
heap_lang, e.g., higher-order references, parametric polymorphism,
etc.
Subsequently, in the file [sem_typed.v] we define the semantic typing judgment
[Γ ⊨ e : τA, in the file [compatibility.v] we prove the semantic typing rules,
i.e. *compatibility lemmas*, in the file [interp.v] we show that any syntactic
type (of Coq type [ty]) can be interpreted as a semantic type, and in the
file [fundamental.v] we prove the **fundamental lemma**, i.e. that syntactic
typing [Γ ⊢ₜ e : τ] implies semantic typing [interp Γ ⊨ e : interp τ].
It is crucial for value semantics of types to be persistent
predicates. This is due to the fact that our type system (as
opposed to substructural type systems, e.g., affine type systems)
allows values to be used multiple times. Hence, the fact that a
value belongs to the semantics of a type must be duplicable which
is guaranteed by persistence. *)
In order to define the type [sem_ty] of semantic types, we use Iris predicates
instead of ordinary Coq predicates. That is, we use [val → iProp Σ] instead of
[val → Prop]. The power of Iris's logic then allows us to define semantic type
formers for e.g., higher-order references and polymorphism, in an elegant way.
(* The domain of semantic types: persistent Iris predicates over values *)
It is crucial for value semantics of types to be **persistent** predicates. This
is due to the fact that our type system (as opposed to substructural type
systems, e.g., affine type systems) allows values to be used multiple times.
Hence, the fact that a value belongs to the semantics of a type must be
duplicable, which is guaranteed by persistence. *)
(** Semantic types are defined using a record, which bundles an Iris predicate
[sem_ty_car : val → iProp Σ] together with a proof of persistence. *)
Record sem_ty Σ := SemTy {
sem_ty_car :> val iProp Σ;
sem_ty_persistent v : Persistent (sem_ty_car v)
}.
Arguments SemTy {_} _%I {_}.
Arguments sem_ty_car {_} _ _ : simpl never.
Bind Scope sem_ty_scope with sem_ty.
Delimit Scope sem_ty_scope with sem_ty.
(** Iris uses the type class [Persistent] to capture which propositions are
persistent. Record fields are not automatically declared as instances, so we
do that by hand. *)
Existing Instance sem_ty_persistent.
(** We show that the domain of semantic types forms a Complete Ordered
Family of Equivalences (COFE). This is necessary mostly for
enabling rewriting equivalent semantic types through Coq's setoid
rewrite system. This part is mostly boilerplate.
*)
(** To obtain nice notations for the semantic types (as we will see in the file
[sem_type_formers.v]), we create a notation scope [sem_ty_scope] for semantic
types, which we bind to the type [sem_ty]. *)
Bind Scope sem_ty_scope with sem_ty.
Delimit Scope sem_ty_scope with sem_ty.
(* The COFE structure on semantic types *)
(** * The COFE structure on semantic types *)
(** We show that semantic types [sem_ty] form a Complete Ordered Family of
Equivalences (COFE). This is necessary mostly for enabling rewriting equivalent
semantic types through Coq's setoid rewrite system. This part is mostly
boilerplate. *)
Section sem_ty_cofe.
Context {Σ : gFunctors}.
......
......@@ -2,7 +2,7 @@ From tutorial_popl20 Require Export language.
(** * Syntactic types for HeapLang *)
(** The inductive type [ty] defines the syntactic types for HeapLang. We make
use of De Bruijn indices to support type-level binding. *)
use of De Bruijn indices to model type-level binding. *)
Inductive ty :=
| TVar : nat ty
| TUnit : ty
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment