Mercurial > cpdt > repo
changeset 75:ec2c1830a7a1
Type-checking example, with discussion
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 03 Oct 2008 15:10:30 -0400 |
parents | a21447f76aad |
children | 82a2189fa283 |
files | src/Subset.v |
diffstat | 1 files changed, 141 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Subset.v Fri Oct 03 14:29:21 2008 -0400 +++ b/src/Subset.v Fri Oct 03 15:10:30 2008 -0400 @@ -516,12 +516,16 @@ (** * A Type-Checking Example *) +(** We can apply these specification types to build a certified type-checker for a simple expression language. *) + Inductive exp : Set := | Nat : nat -> exp | Plus : exp -> exp -> exp | Bool : bool -> exp | And : exp -> exp -> exp. +(** We define a simple language of types and its typing rules, in the style introduced in Chapter 4. *) + Inductive type : Set := TNat | TBool. Inductive hasType : exp -> type -> Prop := @@ -538,13 +542,19 @@ -> hasType e2 TBool -> hasType (And e1 e2) TBool. -Definition eq_type_dec : forall (t1 t2 : type), {t1 = t2} + {t1 <> t2}. +(** It will be helpful to have a function for comparing two types. We build one using [decide equality]. *) + +Definition eq_type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}. decide equality. Defined. +(** Another notation complements the monadic notation for [maybe] that we defined earlier. Sometimes we want to be to include "assertions" in our procedures. That is, we want to run a decision procedure and fail if it fails; otherwise, we want to continue, with the proof that it produced made available to us. This infix notation captures that, for a procedure that returns an arbitrary two-constructor type. *) + Notation "e1 ;; e2" := (if e1 then e2 else ??) (right associativity, at level 60). +(** With that notation defined, we can implement a [typeCheck] function, whose code is only more complex than what we would write in ML because it needs to include some extra type annotations. Every [[[e]]] expression adds a [hasType] proof obligation, and [crush] makes short work of them when we add [hasType]'s constructors as hints. *) + Definition typeCheck (e : exp) : {{t | hasType e t}}. Hint Constructors hasType. @@ -567,14 +577,111 @@ end); crush. Defined. +(** Despite manipulating proofs, our type checker is easy to run. *) + Eval simpl in typeCheck (Nat 0). +(** [[ + + = [[TNat]] + : {{t | hasType (Nat 0) t}} + ]] *) + Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)). +(** [[ + + = [[TNat]] + : {{t | hasType (Plus (Nat 1) (Nat 2)) t}} + ]] *) + Eval simpl in typeCheck (Plus (Nat 1) (Bool false)). +(** [[ + + = ?? + : {{t | hasType (Plus (Nat 1) (Bool false)) t}} + ]] *) + +(** The type-checker also extracts to some reasonable OCaml code. *) + +Extraction typeCheck. + +(** %\begin{verbatim} +(** val typeCheck : exp -> type0 maybe **) + +let rec typeCheck = function + | Nat n -> Found TNat + | Plus (e1, e2) -> + (match typeCheck e1 with + | Unknown -> Unknown + | Found t1 -> + (match typeCheck e2 with + | Unknown -> Unknown + | Found t2 -> + (match eq_type_dec t1 TNat with + | true -> + (match eq_type_dec t2 TNat with + | true -> Found TNat + | false -> Unknown) + | false -> Unknown))) + | Bool b -> Found TBool + | And (e1, e2) -> + (match typeCheck e1 with + | Unknown -> Unknown + | Found t1 -> + (match typeCheck e2 with + | Unknown -> Unknown + | Found t2 -> + (match eq_type_dec t1 TBool with + | true -> + (match eq_type_dec t2 TBool with + | true -> Found TBool + | false -> Unknown) + | false -> Unknown))) +\end{verbatim}% + +#<pre> +(** val typeCheck : exp -> type0 maybe **) + +let rec typeCheck = function + | Nat n -> Found TNat + | Plus (e1, e2) -> + (match typeCheck e1 with + | Unknown -> Unknown + | Found t1 -> + (match typeCheck e2 with + | Unknown -> Unknown + | Found t2 -> + (match eq_type_dec t1 TNat with + | true -> + (match eq_type_dec t2 TNat with + | true -> Found TNat + | false -> Unknown) + | false -> Unknown))) + | Bool b -> Found TBool + | And (e1, e2) -> + (match typeCheck e1 with + | Unknown -> Unknown + | Found t1 -> + (match typeCheck e2 with + | Unknown -> Unknown + | Found t2 -> + (match eq_type_dec t1 TBool with + | true -> + (match eq_type_dec t2 TBool with + | true -> Found TBool + | false -> Unknown) + | false -> Unknown))) +</pre># *) + +(** %\smallskip% + +We can adapt this implementation to use [sumor], so that we know our type-checker only fails on ill-typed inputs. First, we define an analogue to the "assertion" notation. *) Notation "e1 ;;; e2" := (if e1 then e2 else !!) (right associativity, at level 60). -Theorem hasType_det : forall e t1, +(** Next, we prove a helpful lemma, which states that a given expression can have at most one type. *) + +Lemma hasType_det : forall e t1, hasType e t1 -> forall t2, hasType e t2 @@ -582,10 +689,16 @@ induction 1; inversion 1; crush. Qed. +(** Now we can define the type-checker. Its type expresses that it only fails on untypable expressions. *) + Definition typeCheck' (e : exp) : {t : type | hasType e t} + {forall t, ~hasType e t}. Hint Constructors hasType. + (** We register all of the typing rules as hints. *) + Hint Resolve hasType_det. + (** [hasType_det] will also be useful for proving proof obligations with contradictory contexts. Since its statement includes [forall]-bound variables that do not appear in its conclusion, only [eauto] will apply this hint. *) + (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *) refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~hasType e t} := match e return {t : type | hasType e t} + {forall t, ~hasType e t} with | Nat _ => [[[TNat]]] @@ -603,8 +716,34 @@ eq_type_dec t2 TBool;;; [[[TBool]]] end); clear F; crush' tt hasType; eauto. + + (** We clear [F], the local name for the recursive function, to avoid strange proofs that refer to recursive calls that we never make. The [crush] variant [crush'] helps us by performing automatic inversion on instances of the predicates specified in its second argument. Once we throw in [eauto] to apply [hasType_det] for us, we have discharged all the subgoals. *) Defined. +(** The short implementation here hides just how time-saving automation is. Every use of one of the notations adds a proof obligation, giving us 12 in total. Most of these obligations require multiple inversions and either uses of [hasType_det] or applications of [hasType] rules. + +The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *) + Eval simpl in typeCheck' (Nat 0). +(** [[ + + = [[[TNat]]] + : {t : type | hasType (Nat 0) t} + + {(forall t : type, ~ hasType (Nat 0) t)} + ]] *) + Eval simpl in typeCheck' (Plus (Nat 1) (Nat 2)). +(** [[ + + = [[[TNat]]] + : {t : type | hasType (Plus (Nat 1) (Nat 2)) t} + + {(forall t : type, ~ hasType (Plus (Nat 1) (Nat 2)) t)} + ]] *) + Eval simpl in typeCheck' (Plus (Nat 1) (Bool false)). +(** [[ + + = !! + : {t : type | hasType (Plus (Nat 1) (Bool false)) t} + + {(forall t : type, ~ hasType (Plus (Nat 1) (Bool false)) t)} + ]] *)