Commit 3ad58265 authored by Robbert Krebbers's avatar Robbert Krebbers

Comments for polymorphism.

parent 22e65b3e
From tutorial_popl20 Require Export language.
(** * Polymorphic functions in HeapLang *)
(** We model type-level lambdas and applications as thunks since heap_lang does
not have them. *)
(** * Polymorphism and existential types in HeapLang *)
(** Since HeapLang is an untyped language, it does not have constructs for
polymorphic functions (i.e. type-level lambdas and application), and for
existential types (i.e. pack and unpack). *)
(** We retrofit type-level lambdas and application on HeapLang by defining them
as mere thunks, and ordinary application, respectively. This ensures that
polymorphic programs satisfy a **value condition**, which is needed to obtain
type safety in the presence of mutable state. *)
Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing) : expr_scope.
Notation "Λ: e" := (λ: <>, e)%V (at level 200, only parsing) : val_scope.
Notation "e '<_>'" := (App e%E #()) (at level 10, only parsing) : expr_scope.
(** We wrap [pack] and [unpack] into an explicitly function so that we can have
a nice notation for it. *)
(** We also use ordinary lambdas and application to retrofit [pack] and
[unpack] on HeapLang. This time we first define some helper functions so that
we can have a nice notation for these constructs. *)
Definition exist_pack : val := λ: "x", "x".
Definition exist_unpack : val := λ: "x" "y", "x" "y".
......@@ -23,11 +30,14 @@ Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (LamV x%binder e2%E) e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'unpack:' x := '[' e1 ']' 'in' '/' e2 ']'") : val_scope.
(** ** Exercise (swap_poly, easy) *)
(** Below we define a polymorphic version of the [swap] function. *)
Definition swap_poly : val := Λ: λ: "l1" "l2",
let: "x" := !"l1" in
"l1" <- !"l2";;
"l2" <- "x".
(** Prove the following specification. *)
Lemma wp_swap_poly `{!heapG Σ} l1 l2 v1 v2 :
l1 v1 -
l2 v2 -
......@@ -35,12 +45,7 @@ Lemma wp_swap_poly `{!heapG Σ} l1 l2 v1 v2 :
(* REMOVE *) Proof.
iIntros "Hl1 Hl2".
rewrite /swap_poly.
wp_pures.
wp_load.
(* wp_pures is performed implicitly, so not needed *)
wp_load.
wp_store.
wp_store.
iFrame.
auto.
do 2 wp_load.
do 2 wp_store.
by iFrame.
Qed.
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