typed.v 13.2 KB
Newer Older
1
From solutions Require Export types polymorphism.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
7
8
9
10
11
12
13
14
15
(** * Syntactic typing for HeapLang *)
(** In this file, we define a syntactic type system for HeapLang. We do this
in the conventional way by defining the typing judgment [Γ ⊢ₜ e : τ] using an
inductive relation. *)

(** * Operator typing *)
(** In order to define the typing judgment, we first need some helpers for
operator typing. *)

(** The first helper we define is [ty_unboxed τ], which expresses that values
of [τ] are unboxed, i.e. they fit into one machine word. This helper is needed
to state the typing rules for equality and compare-and-exchange ([CmpXchg]),
which can only be used on unboxed values. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
Inductive ty_unboxed : ty  Prop :=
  | TUnit_unboxed : ty_unboxed TUnit
  | TBool_unboxed : ty_unboxed TBool
  | TInt_unboxed : ty_unboxed TInt
  | TRef_unboxed τ : ty_unboxed (TRef τ).
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24

(** In order to let Coq automatically prove that types are unboxed, we turn
[ty_unboxed] into a type class, and turn the constructors into type class
instances. This is done using the following commands. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
27
Existing Class ty_unboxed.
Existing Instances TUnit_unboxed TBool_unboxed TInt_unboxed TRef_unboxed.

Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
33
34
35
36
37
38
39
40
(** We can now use Coq's type class inference mechanism to automatically
establish that given types are unboxed. This is done by invoking the [apply _]
tactic. *)
Lemma TRef_TRef_TInt_unboxed : ty_unboxed (TRef (TRef TInt)).
Proof. apply _. Qed.

(** The true power of turning [ty_unboxed] into a type class is that whenever a
lemma or definition has a [ty_unboxed] argument, type class inference is called
automatically. *)

(** The relation [ty_un_op op τ σ] expresses that a unary operator [op] with an
argument of type [τ] has result type [σ]. We also turn [ty_un_op] into a type
class. *)
41
42
43
44
45
46
Inductive ty_un_op : un_op  ty  ty  Prop :=
  | Ty_un_op_int op : ty_un_op op TInt TInt
  | Ty_un_op_bool : ty_un_op NegOp TBool TBool.
Existing Class ty_un_op.
Existing Instances Ty_un_op_int Ty_un_op_bool.

Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
(** The relation [ty_bin_op op τ1 τ2 σ] expresses that a binary operator [op]
with arguments of type [τ1] and [τ2] has result type [σ]. In order to avoid
an abundance of rules, we factorize the operators into 4 categories: equality,
arithmetic, comparison, and Boolean operators. For the last 3 categories, we make
use of [TCElemOf x xs], where [x : A] and [xs : list A], which is a type class
version of [x ∈ xs]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
56
57
58
59
60
61
62
63
64
65
66
Inductive ty_bin_op : bin_op  ty  ty  ty  Prop :=
  | Ty_bin_op_eq τ :
     ty_unboxed τ  ty_bin_op EqOp τ τ TBool
  | Ty_bin_op_arith op :
     TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp;
                  AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] 
     ty_bin_op op TInt TInt TInt
  | Ty_bin_op_compare op :
     TCElemOf op [LeOp; LtOp]  ty_bin_op op TInt TInt TBool
  | Ty_bin_op_bool op :
     TCElemOf op [AndOp; OrOp; XorOp]  ty_bin_op op TBool TBool TBool.
Existing Class ty_bin_op.
Existing Instances Ty_bin_op_eq Ty_bin_op_arith Ty_bin_op_compare Ty_bin_op_bool.

Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
(** * The typing judgment *)
(** With the above helpers at hand, we can define the syntactic typing judgment
[Γ ⊢ₜ e : τ]. While most of the typing rules are standard, the definition
involves a number of interesting aspects.

- Since term-level variables in HeapLang are modeled using strings, we represent
  typing contexts [Γ : gmap string ty] as mappings from strings to types. Here,
  [gmap] is the type of generic maps from the std++ library.
- In addition to named binders, HeapLang also features the anonymous binder
  [<>]. This allows one to define [λ: x, e] as [rec: <> x := e]. Binders in
  HeapLang are of type [binder], whose definition is as follows:

  <<
  Inductive binder := BAnon : binder | BNamed : string → binder.
  >>

  As a result, in the typing rules of all constructs that involve binders (i.e.,
  the typing rules [Rec_typed] and [Unpack_typed]) we have to consider two
  cases [BAnon] and [BNamed]. To factorize these typing rules, we make use of
  [binder_insert], which lifts the insert operator [<[_:=_> _] on [gmap] to
  binders.
- The type of values [val] and expressions [expr] of HeapLang are defined in
  a mutually inductive fashion:

  <<
  Inductive expr :=
    (* Values *)
    | Val (v : val)
    (* Base lambda calculus *)
    | Var (x : string)
    | Rec (f x : binder) (e : expr)
    | App (e1 e2 : expr)
    (* Products *)
    | Pair (e1 e2 : expr)
    | Fst (e : expr)
    | Snd (e : expr)
    (* Sums *)
    | InjL (e : expr)
    | InjR (e : expr)
    | Case (e0 : expr) (e1 : expr) (e2 : expr)
    (* Etc. *)
  with val :=
    | LitV (l : base_lit)
    | RecV (f x : binder) (e : expr)
    | PairV (v1 v2 : val)
    | InjLV (v : val)
    | InjRV (v : val).
  >>

  For technical reasons, the only terms that are considered values are those
  that begin with the [Val] expression former. This means that, for example,
  [Pair (Val v1) (Val v2)] is not a value---it reduces to [Val (PairV v1 v2)],
  which is. This leads to some administrative redexes, and to a distinction
  between "value pairs", "value sums", "value closures" and their "expression"
  counterparts.

  However, this also makes values syntactically uniform, which we exploit in the
  definition of substitution ([subst]), which just skips over [Val] terms,
  because values should be closed, and hence not affected by substitution. As a
  consequence, we can entirely avoid talking about "closed terms" in the
  definition of HeapLang.

  As a result of the mutual inductive definition, and the distinction between
  "value pairs", "value sums", "value closures" and their "expression"
  counterparts, we need to define the typing judgment in a mutual inductive
  fashion too. Hence, apart from the judgment [Γ ⊢ₜ e : τ], we have the judgment
  [⊢ᵥ v : τ]. Note that since values are supposed to be closed, the latter
  judgment does not have a context [Γ].
*)

(** We use [Reserved Notation] so we can use the notation already in the
definition of the typing judgment. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
140
141
142
Reserved Notation "⊢ᵥ v : τ" (at level 20, v, τ at next level).

Inductive typed : gmap string ty  expr  ty  Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  (** Variables *)
144
  | Var_typed Γ x τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
     Γ !! x = Some τ 
     Γ  Var x : τ
147
148
  (** Values *)
  | Val_typed Γ v τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
149
      v : τ 
150
     Γ  v : τ
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  (** Products and sums *)
152
  | Pair_typed Γ e1 e2 τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
     Γ  e1 : τ1  Γ  e2 : τ2 
     Γ  Pair e1 e2 : TProd τ1 τ2
155
  | Fst_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
     Γ  e : TProd τ1 τ2 
     Γ  Fst e : τ1
158
  | Snd_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
     Γ  e : TProd τ1 τ2 
     Γ  Snd e : τ2
161
  | InjL_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
     Γ  e : τ1 
     Γ  InjL e : TSum τ1 τ2
164
  | InjR_typed Γ e τ1 τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
     Γ  e : τ2 
     Γ  InjR e : TSum τ1 τ2
167
  | Case_typed Γ e0 e1 e2 τ1 τ2 τ3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
     Γ  e0 : TSum τ1 τ2  Γ  e1 : TArr τ1 τ3  Γ  e2 : TArr τ2 τ3 
     Γ  Case e0 e1 e2 : τ3
170
  (** Functions *)
171
  | Rec_typed Γ f x e τ1 τ2 :
172
173
     binder_insert f (TArr τ1 τ2) (binder_insert x τ1 Γ)  e : τ2 
     Γ  Rec f x e : TArr τ1 τ2
174
  | App_typed Γ e1 e2 τ1 τ2 :
175
176
     Γ  e1 : TArr τ1 τ2  Γ  e2 : τ1 
     Γ  App e1 e2 : τ2
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  (** Polymorphic functions and existentials *)
178
  | TLam_typed Γ e τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
     ty_lift 0 <$> Γ  e : τ 
     Γ  (Λ: e) : TForall τ
181
  | TApp_typed Γ e τ τ' :
Robbert Krebbers's avatar
Robbert Krebbers committed
182
     Γ  e : TForall τ 
183
     Γ  e <_> : ty_subst 0 τ' τ
184
  | Pack_typed Γ e τ τ' :
Robbert Krebbers's avatar
Robbert Krebbers committed
185
     Γ  e : ty_subst 0 τ' τ 
Robbert Krebbers's avatar
Robbert Krebbers committed
186
     Γ  (pack: e) : TExist τ
187
  | Unpack_typed Γ e1 x e2 τ τ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
190
191
     Γ  e1 : TExist τ 
     binder_insert x τ (ty_lift 0 <$> Γ)  e2 : ty_lift 0 τ2 
     Γ  (unpack: x := e1 in e2) : τ2
  (** Heap operations *)
192
  | Alloc_typed Γ e τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
     Γ  e : τ 
     Γ  Alloc e : TRef τ
195
  | Load_typed Γ e τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
     Γ  e : TRef τ 
     Γ  Load e : τ
198
  | Store_typed Γ e1 e2 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
     Γ  e1 : TRef τ  Γ  e2 : τ 
     Γ  Store e1 e2 : TUnit
201
  | FAA_typed Γ e1 e2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
     Γ  e1 : TRef TInt  Γ  e2 : TInt 
     Γ  FAA e1 e2 : TInt
204
  | CmpXchg_typed Γ e1 e2 e3 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
208
     ty_unboxed τ 
     Γ  e1 : TRef τ  Γ  e2 : τ  Γ  e3 : τ 
     Γ  CmpXchg e1 e2 e3 : TProd τ TBool
  (** Operators *)
209
  | UnOp_typed Γ op e τ σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
212
     Γ  e : τ 
     ty_un_op op τ σ 
     Γ  UnOp op e : σ
213
  | BinOp_typed Γ op e1 e2 τ1 τ2 σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
216
     Γ  e1 : τ1  Γ  e2 : τ2 
     ty_bin_op op τ1 τ2 σ 
     Γ  BinOp op e1 e2 : σ
217
  | If_typed Γ e0 e1 e2 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
220
     Γ  e0 : TBool  Γ  e1 : τ  Γ  e2 : τ 
     Γ  If e0 e1 e2 : τ
  (** Fork *)
221
  | Fork_typed Γ e :
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
     Γ  e : TUnit 
     Γ  Fork e : TUnit
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
with val_typed : val  ty  Prop :=
  (** Base types *)
  | UnitV_typed :
      #() : TUnit
  | BoolV_typed (b : bool) :
      #b : TBool
  | IntV_val_typed (i : Z) :
      #i : TInt
  (** Products and sums *)
  | PairV_typed v1 v2 τ1 τ2 :
      v1 : τ1   v2 : τ2 
      PairV v1 v2 : TProd τ1 τ2
  | InjLV_typed v τ1 τ2 :
      v : τ1 
      InjLV v : TSum τ1 τ2
  | InjRV_typed v τ1 τ2 :
      v : τ2 
      InjRV v : TSum τ1 τ2
  (** Functions *)
  | RecV_typed f x e τ1 τ2 :
     binder_insert f (TArr τ1 τ2) (binder_insert x τ1 )  e : τ2 
      RecV f x e : TArr τ1 τ2
246
247
248
  | TLamV_typed e τ :
       e : τ 
      (Λ: e) : TForall τ
249
250
where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
and "⊢ᵥ v : τ" := (val_typed v τ).
Robbert Krebbers's avatar
Robbert Krebbers committed
251

Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
(** * Exercise (suger_typed, easy) *)
(** To make it possible to write programs in a compact way, HeapLang features
the following syntactic sugar:

<<
(λ: x, e)              := (rec: <> x := e)
(let: x := e1 in e2)   := (λ x, e2) e1
(e1 ;; e2)             := (let: <> := e1 in e2)
Skip                   := (λ: <>, #()) #()
>>

Prove the following derived typing rules for the syntactic sugar. Note that
due to the distinction between expressions and values, you have to prove some
of them for both the expression construct and their value counterpart. *)

Robbert Krebbers's avatar
Robbert Krebbers committed
267
Lemma Lam_typed Γ x e τ1 τ2 :
268
  binder_insert x τ1 Γ  e : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
269
  Γ  (λ: x, e) : TArr τ1 τ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
273
274
275
276
277
  intros He.
  apply Rec_typed.
  simpl.
  done.
Qed.

Lemma LamV_typed x e τ1 τ2 :
278
  binder_insert x τ1   e : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
279
   (λ: x, e) : TArr τ1 τ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
282
283
284
285
286
287
  intros He.
  apply RecV_typed.
  simpl.
  done.
Qed.

Lemma Let_typed Γ x e1 e2 τ1 τ2 :
288
289
  Γ  e1 : τ1 
  binder_insert x τ1 Γ  e2 : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  Γ  (let: x := e1 in e2) : τ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
293
294
295
296
297
298
  intros He1 He2.
  apply App_typed with τ1.
  - by apply Lam_typed.
  - done.
Qed.

Lemma Seq_typed Γ e1 e2 τ1 τ2 :
299
300
  Γ  e1 : τ1 
  Γ  e2 : τ2 
Robbert Krebbers's avatar
Robbert Krebbers committed
301
  Γ  (e1;; e2) : τ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
305
306
307
308
  intros He1 He2.
  by apply Let_typed with τ1.
Qed.

Lemma Skip_typed Γ :
  Γ  Skip : ().
Robbert Krebbers's avatar
Robbert Krebbers committed
309
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
311
312
313
314
  apply App_typed with ()%ty.
  - apply Val_typed, RecV_typed. apply Val_typed, UnitV_typed.
  - apply Val_typed, UnitV_typed.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
315
316
317
318
(** * Typing of concrete programs *)
(** ** Exercise (swap_typed, easy) *)
(** Prove that the non-polymorphic swap function [swap] can be given the type
[ref τ → ref τ → ()] for any [τ]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Lemma swap_typed τ :  swap : (ref τ  ref τ  ()).
Robbert Krebbers's avatar
Robbert Krebbers committed
320
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
  rewrite /swap.
Robbert Krebbers's avatar
Robbert Krebbers committed
322
323
324
325
326
327
328
329
330
331
332
333
  apply LamV_typed.
  apply Lam_typed.
  apply Let_typed with τ.
  { apply Load_typed. by apply Var_typed. }
  apply Seq_typed with ()%ty.
  { apply Store_typed with τ.
    - by apply Var_typed.
    - apply Load_typed. by apply Var_typed. }
  apply Store_typed with τ.
  - by apply Var_typed.
  - by apply Var_typed.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
334

Robbert Krebbers's avatar
Robbert Krebbers committed
335
336
337
(** ** Exercise (swap_poly_typed, easy) *)
(** Prove that [swap_poly] can be typed using the polymorphic type
[∀ X, ref X → ref X → ())], i.e. [∀: ref #0 → ref #0 → ())] in De Bruijn style. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Lemma swap_poly_typed :  swap_poly : (∀: ref #0  ref #0  ()).
Robbert Krebbers's avatar
Robbert Krebbers committed
339
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
343
344
345
346
347
348
349
350
351
352
353
  rewrite /swap_poly.
  apply TLamV_typed.
  do 2 apply Lam_typed.
  apply Let_typed with (#0)%ty.
  { apply Load_typed. by apply Var_typed. }
  apply Seq_typed with ()%ty.
  { apply Store_typed with (#0)%ty.
    - by apply Var_typed.
    - apply Load_typed. by apply Var_typed. }
  apply Store_typed with (#0)%ty.
  - by apply Var_typed.
  - by apply Var_typed.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
356
(** ** Exercise (not_typed, easy) *)
(** Prove that the programs [unsafe_pure] and [unsafe_ref] from [language.v]
cannot be typed using the syntactic type system. *)
357
Lemma unsafe_pure_not_typed τ : ¬ ( unsafe_pure : τ).
Robbert Krebbers's avatar
Robbert Krebbers committed
358
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
359
360
361
362
363
364
365
366
  intros Htyped.
  repeat
    match goal with
    | H : _  _ : _ |- _ => inversion H; simplify_eq/=; clear H
    | H :  _ : _ |- _ => inversion H; simplify_eq/=; clear H
    end.
Qed.

367
Lemma unsafe_ref_not_typed τ : ¬ ( unsafe_ref : τ).
Robbert Krebbers's avatar
Robbert Krebbers committed
368
(* REMOVE *) Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
371
372
373
374
375
  intros Htyped.
  repeat
    match goal with
    | H : _  _ : _ |- _ => inversion H; simplify_eq/=; clear H
    | H :  _ : _ |- _ => inversion H; simplify_eq/=; clear H
    end.
Qed.