(** * MoreStlc: More on the Simply Typed Lambda-Calculus *) (* Version of 7/8/2010 *) Require Export Stlc. Require Import Relations. (* ###################################################################### *) (** * Typechecking for STLC *) (** The [has_type] relation defines what it means for a term to belong to a type (in some context). But it doesn't, by itself, tell us how to _check_ whether or not a term is well typed. Fortunately, the rules defining [has_type] are _syntax directed_ -- they exactly follow the shape of the term. This makes it straightforward to translate the typing rules into clauses of a typechecking _function_ that takes a term and a context and either returns the term's type or else signals that the term is not typable. *) Module STLCChecker. Import STLC. (* ###################################################################### *) (** ** Comparing Types *) (** First, we need a function to compare two types for equality... *) Fixpoint beq_ty (T1 T2:ty) : bool := match T1,T2 with | ty_base i, ty_base i' => beq_id i i' | ty_arrow T11 T12, ty_arrow T21 T22 => andb (beq_ty T11 T21) (beq_ty T12 T22) | _,_ => false end. (** ... and we need to establish the usual two-way connection between the boolean result returned by [beq_ty] and the logical proposition that its inputs are equal. *) Lemma beq_ty_refl : forall T1, beq_ty T1 T1 = true. Proof. intros T1. induction T1; simpl. symmetry. apply beq_id_refl. rewrite IHT1_1. rewrite IHT1_2. reflexivity. Qed. Lemma beq_ty__eq : forall T1 T2, beq_ty T1 T2 = true -> T1 = T2. Proof with auto. intros T1. induction T1; intros T2 Hbeq; destruct T2; inversion Hbeq. Case "T1=ty_base i". symmetry in H0. apply beq_id_eq in H0. subst... Case "T1=ty_arrow T1_1 T1_2". apply andb_true in H0. destruct H0 as [Hbeq1 Hbeq2]. apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed. (* ###################################################################### *) (** ** The Typechecker *) (** Now here's the typechecker. It works by walking over the structure of the given term, returning either [Some T] or [None]. Each time we make a recursive call to find out the types of the subterms, we need to pattern-match on the results to make sure that they are not [None]. Also, in the [tm_app] case, we use pattern matching to extract the left- and right-hand sides of the function's arrow type (and fail if the type of the function is not [ty_arrow T11 T12] for some [T1] and [T2]). *) Fixpoint type_check (Gamma:context) (t:tm) : option ty := match t with | tm_var x => Gamma x | tm_abs x T11 t12 => match type_check (extend Gamma x T11) t12 with | Some T12 => Some (ty_arrow T11 T12) | _ => None end | tm_app t1 t2 => match type_check Gamma t1, type_check Gamma t2 with | Some (ty_arrow T11 T12),Some T2 => if beq_ty T11 T2 then Some T12 else None | _,_ => None end end. (* ###################################################################### *) (** ** Properties *) (** To verify that this typechecking algorithm is the correct one, we show that it is _sound_ and _complete_ for the original [has_type] relation -- that is, [type_check] and [has_type] define the same partial function. *) Theorem type_checking_sound : forall Gamma t T, type_check Gamma t = Some T -> has_type Gamma t T. Proof with eauto. intros Gamma t. generalize dependent Gamma. (tm_cases (induction t) Case); intros Gamma T Htc; inversion Htc. Case "tm_var"... Case "tm_app". remember (type_check Gamma t1) as TO1. remember (type_check Gamma t2) as TO2. destruct TO1 as [T1|]; try solve by inversion; destruct T1 as [|T11 T12]; try solve by inversion. destruct TO2 as [T2|]; try solve by inversion. remember (beq_ty T11 T2) as b. destruct b; try solve by inversion. symmetry in Heqb. apply beq_ty__eq in Heqb. inversion H0; subst... Case "tm_abs". rename i into y. rename t into T1. remember (extend Gamma y T1) as G'. remember (type_check G' t0) as TO2. destruct TO2; try solve by inversion. inversion H0; subst... Qed. Theorem type_checking_complete : forall Gamma t T, has_type Gamma t T -> type_check Gamma t = Some T. Proof with auto. intros Gamma t T Hty. (typing_cases (induction Hty) Case); simpl. Case "T_Var"... Case "T_Abs". rewrite IHHty... Case "T_App". rewrite IHHty1. rewrite IHHty2. rewrite (beq_ty_refl T11)... Qed. End STLCChecker. (* ###################################################################### *) (** * Simple Extensions to STLC *) (** The simply typed lambda-calculus has enough structure to make its theoretical properties interesting, but it is not yet much of a programming language. In this chapter, we begin to close the gap with more familiar languages by introducing a number of familiar features that have straightforward treatments at the level of typing. *) (** *** Numbers and Booleans *) (** Adding types, constants, and primitive operations for numbers and booleans is easy -- just a matter of combining the two halves of the Stlc.v chapter. *) (** *** The [Unit] Type *) (** Another useful base type, found especially in languages in the ML family, is the singleton type [Unit]. In contrast to the uninterpreted base types of the simply typed lambda-calculus, this type _is_ interpreted, in the simplest possible way: we explicitly introduce a single element---the term constant [unit] (with a small [u])---and a typing rule making [unit] an element of [Unit]. We also add [unit] to the set of possible result values of computations---indeed, [unit] is the _only_ possible result of evaluating an expression of type [Unit]. << t ::= Terms: | ... (other terms same as before) | unit unit value v ::= Values: | ... | unit unit T ::= Types: | ... | Unit Unit type >> *) (** *** [let]-bindings *) (** When writing a complex expression, it is often useful---both for avoiding repetition and for increasing readability---to give names to some of its subexpressions. Most languages provide one or more ways of doing this. In OCaml, for example, we can write [let x=t1 in t2] to mean ``evaluate the expression [t1] and bind the name [x] to the resulting value while evaluating [t2].'' Our [let]-binder follows ML's in choosing a call-by-value evaluation order, where the [let]-bound term must be fully evaluated before evaluation of the [let]-body can begin. The typing rule [T_Let] tells us that the type of a [let] can be calculated by calculating the type of the [let]-bound term, extending the context with a binding with this type, and in this enriched context calculating the type of the body, which is then the type of the whole [let] expression. At this point in the course, it's probably just as easy to simply look at the rules defining this new feature as to wade through a lot of english text conveying the same information. Here they are: Syntax: << t ::= Terms: | ... | let x=t in t let-binding >> Reduction: [[[ t1 --> t1' ---------------------------------- (ST_Let1) let x=t1 in t2 --> let x=t1' in t2 ---------------------------- (ST_LetValue) let x=v1 in t2 --> [v1/x] t2 ]]] Typing: [[[ Gamma |- t1 : T1 Gamma, x:T1 |- t2 : T2 -------------------------------------------- (T_Let) Gamma |- let x=t1 in t2 : T2 ]]] *) (** *** Pairs *) (** Our functional programming examples have made frequent use of _pairs_ of values. The type of such pairs is called a _product type_. The formalization of pairs is almost too simple to be worth discussing---by this point in the book, it should be about as easy to read a set of inference rules (or a formal [Inductive] definition) as to wade through a description in English conveying the same information. However, let's look briefly at the various parts of the definition to emphasize the common pattern. In Coq, the primitive way of extracting the components of a pair is _pattern matching_. An alternative style is to take [fst] and [snd] -- the first- and second-projection operators -- as primitives. Just for fun, let's do our products this way. For example, here's how we'd write a function that takes a pair of numbers and returns the pair of their sum and product: << \x:nat*nat. let sum = x.fst + x.snd in let prod = x.fst * x.snd in (sum,prod) >> Adding pairs to the simply typed lambda-calculus, then, involves adding two new forms of term---pairing, written [(t1,t2)], and projection, written [t.fst] for the first projection from [t] and [t.snd] for the second projection---plus one new type constructor, [T1*T2], called the _product_ of [T1] and [T2]. Syntax: << t ::= Terms: | ... | (t,t) pair | t.fst first projection | t.snd second projection v ::= Values: | ... | (v,v) pair value T ::= Types: | ... | T * T product type >> For evaluation, we need several new rules specifying how pairs and projection behave. [[[ t1 --> t1' -------------------- (ST_Pair1) (t1,t2) --> (t1',t2) t2 --> t2' -------------------- (ST_Pair2) (v1,t2) --> (v1,t2') t1 --> t1' ------------------ (ST_Fst1) t1.fst --> t1'.fst ------------------ (ST_FstPair) (v1,v2).fst --> v1 t1 --> t1' ------------------ (ST_Snd1) t1.snd --> t1'.snd ------------------ (ST_SndPair) (v1,v2).snd --> v2 ]]] Rules [ST_FstPair] and [ST_SndPair] specify that, when a fully evaluated pair meets a first or second projection, the result is the appropriate component. The congruence rules [ST_Fst1] and [ST_Snd1] allow reduction to proceed under projections, when the term being projected from has not yet been fully evaluated. [ST_Pair1] and [ST_Pair2] evaluate the parts of pairs: first the left part, and then---when a value appears on the left---the right part. The ordering arising from the use of the metavariables [v] and [t] in these rules enforces a left-to-right evaluation strategy for pairs. (Note the implicit convention that metavariables like [v] and [v1] can only denote values.) We've also added a clause to the definition of values, above, specifying that [(v1,v2)] is a value. The fact that the components of a pair value must themselves be values ensures that a pair passed as an argument to a function will be fully evaluated before the function body starts executing. The typing rules for pairs and projections are straightforward. The rule, [T_Pair], says that [(t1,t2)] has type [T1*T2] if [t1] has type [T1] and [t2] has type [T2]. Conversely, the rules [T_Fst] and [T_Snd] tell us that, if [t1] has a product type [T11*T12] (i.e., if it will evaluate to a pair), then the types of the projections from this pair are [T11] and [T12]. [[[ Gamma |- t1 : T1 Gamma |- t2 : T2 --------------------------------------- (T_Pair) Gamma |- (t1,t2) : T1*T2 Gamma |- t1 : T11*1T2 --------------------- (T_Fst) Gamma |- t1.fst : T11 Gamma |- t1 : T11*T12 --------------------- (T_Snd) Gamma |- t1.snd : T12 ]]] *) (* ###################################################################### *) (** *** Records *) (** Another familiar structure from everyday programming languages is _records_. Intuitively, records can be obtained from pairs by two kinds of generalization: they are n-ary products (rather than just binary) and their fields are accessed by _label_ (rather than position). Syntax: << t ::= Terms: | ... | {i1=t1, ..., in=tn} record | t.i projection v ::= Values: | ... | {i1=v1, ..., in=vn} record value T ::= Types: | ... | {i1:T1, ..., in:Tn} record type >> Intuitively, the generalization is pretty obvious. But it's worth noticing that what we've actually written is rather informal: in particular, we've written "[...]" in several places to mean "any number of these," and we've omitted explicit mention of the usual side-condition that the labels of a record should not contain repetitions. It is possible to devise informal notations that are more precise, but these tend to be quite heavy and to obscure the main points of the definitions. So we'll leave these a bit loose here (they are informal anyway, after all) and do the work of tightening things up elsewhere (in [Records.v]). Reduction: [[[ ti --> ti' -------------------------------------------------------------------- (ST_Rcd) {i1=v1, ..., im=vm, in=ti, ...} --> {i1=v1, ..., im=vm, in=ti', ...} t1 --> t1' -------------- (ST_Proj1) t1.i --> t1'.i ------------------------- (ST_ProjRcd) {..., i=vi, ...}.i --> vi ]]] Again, these rules are a bit informal. For example, the first rule is intended to be read "if [ti] is the leftmost field that is not a value and if [ti] steps to [ti'], then the whole record steps..." In the last rule, the intention is that there should only be one field called i, and that all the other fields must contain values. Typing: [[[ Gamma |- t1 : T1 ... Gamma |- tn : Tn -------------------------------------------------- (T_Rcd) Gamma |- {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn} Gamma |- t : {..., i:Ti, ...} ----------------------------- (T_Proj) Gamma |- t.i : Ti ]]] *) (* ###################################################################### *) (** *** Encoding Records *) (** There are several ways to make the above definitions precise. - We can directly formalize the syntactic forms and inference rules, staying as close as possible to the form we've given them above. This is conceptually straightforward, and it's probably what we'd want to do if we were building a real compiler -- in particular, it will allow is to print error messages in the form that programmers will find easy to understand. But the formal versions of the rules will not be pretty at all! - We could look for a smoother way of presenting records -- for example, a binary presentation with one constructor for the empty record and another constructor for adding a single field to an existing record, instead of a single monolithic constructor that builds a whole record at once. This is the right way to go if we are primarily interested in studying the metatheory of the calculi with records, since it leads to clean and elegant definitions and proofs. The file [Records.v] shows how this can be done. - Alternatively, if we like, we can avoid formalizing records altogether, by stipulating that record notations are just informal shorthands for more complex expressions involving pairs and product types. We sketch this approach here. First, observe that we can encode arbitrary-size tuples using nested pairs and the [unit] value. To avoid overloading the pair notation [(t1,t2)], we'll use curly braces without labels to write down tuples, so [{}] is the empty tuple, [{5}] is a singleton tuple, [{5,6}] is a 2-tuple (morally the same as a pair), [{5,6,7}] is a triple, etc. << {} ----> unit {t1, t2, ..., tn} ----> (t1, trest) where {t2, ..., tn} ----> trest >> Similarly, we can encode tuple types using nested product types: << {} ----> Unit {T1, T2, ..., Tn} ----> T1 * TRest where {T2, ..., Tn} ----> TRest >> The operation of projecting a field from a tuple can be encoded using a sequence of second projections followed by a first projection: << t.0 ----> t.fst t.(n+1) ----> (t.snd).n >> Next, suppose that there is some total ordering on record labels, so that we can associate each label with a unique natural number. This number is called the _position_ of the label. For example, we might assign positions like this: << LABEL POSITION a 0 b 1 c 2 ... ... foo 1004 ... ... bar 10562 ... ... >> We use these positions to encode record values as tuples (i.e., as nested pairs) by sorting the fields according to their positions. For example: << {a=5, b=6} ----> {5,6} {a=5, c=7} ----> {5,unit,7} {c=7, a=5} ----> {5,unit,7} {c=5, b=3} ----> {unit,3,5} {f=8,c=5,a=7} ----> {7,unit,5,unit,unit,8} {f=8,c=5} ----> {unit,unit,5,unit,unit,8} >> Note that each field appears in the position associated with its label, that the size of the tuple is determined by the label with the highest position, and that we fill in unused positions with [unit]. We do exactly the same thing with record types: << {a:Nat, b:Nat} ----> {Nat,Nat} {c:Nat, a:Nat} ----> {Nat,Unit,Nat} {f:Nat,c:Nat} ----> {Unit,Unit,Nat,Unit,Unit,Nat} >> Finally, record projection is encoded as a tuple projection from the appropriate position: << t.l ----> t.(position of l) >> It is not hard to check that all the typing rules for the original "direct" presentation of records are validated by this encoding. (The reduction rules are "almost validated" -- not quite, because the encoding reorders fields.) *) (** Of course, this encoding will not be very efficient if we happen to use a record with label [bar]! But things are not actually as bad as they might seem: for example, if we assume that our compiler can see the whole program at the same time, we can _choose_ the numbering of labels so that we assign small positions to the most frequently used labels. Indeed, there are industrial compilers that essentially do this! *) (** *** Sums *) (** Many programs need to deal with values that can take two distinct forms. For example, we might identify employees in an accounting application using using _either_ their name _or_ their id number. A search function might return _either_ a matching value _or_ an error code. These are specific examples of a binary _sum type_, which describes a set of values drawn from exactly two given types, e.g. [Value = Nat + Bool] We create elements of these types by _tagging_ elements of the component types. For example, if [n] is a [Nat] then [inl v] is an [Value]; similarly, if [b] is a [Bool] then [inr b] is an [Value]. The names of the tags [inl] and [inr] arise from thinking of them as functions << inl : Nat -> Nat + Bool inr : Bool -> Nat + Bool >> that "inject" elements of [Nat] or [Bool] into the left and right components of the sum type [Value]. But note that we don't actually treat them as functions. In general, the elements of a type [T1 + T2] consist of the elements of [T1] tagged with the token [inl], plus the elements of [T2] tagged with [inr]. To _use_ elements of sum types, we introduce a [case] construct (a very simplified form of Coq's [match]) to destruct them. For example, the following procedure converts an [Value] into a [Nat]: << getNat : \x:Value. case x of inl n => n inl b => if b then 1 else 0 >> More formally... Syntax: << t ::= Terms: | ... | inl t tagging (left) | inr t tagging (right) | case t of case inl x => t | inr x => t v ::= Values: | ... | inl v tagged value (left) | inr v tagged value (right) T ::= Types: | ... | T + T sum type >> Evaluation: [[[ t1 --> t1' -------------------- (ST_Inl) inl t1 --> inl t1' t1 --> t1' -------------------- (ST_Inr) inr t1 --> inr t1' t0 --> t0' ------------------------------------------- (ST_Case) case t0 of inl x1 => t1 | inl x2 => t2 --> case t0' of inl x1 => t1 | inl x2 => t2 ------------------------------------------------------------ (ST_CaseInl) case (inl v0) of inl x1 => t1 | inl x2 => t2 --> [v0/x1] t1 ------------------------------------------------------------- (ST_CaseInr) case (inr v0) of inl x1 => t1 | inl x2 => t2 --> [v0/x2] t2 ]]] Typing: [[[ Gamma |- t1 : T1 ------------------------- (T_Inl) Gamma |- inl t1 : T1 + T2 Gamma |- t1 : T2 ------------------------- (T_Inr) Gamma |- inr t1 : T1 + T2 Gamma |- t0 : T1+T2 Gamma,x1:T1 |- t1 : T Gamma, x2:T2 |- t2 : T --------------------------------------------------- (T_Case) Gamma |- case t0 of inl x1 => t1 | inr x2 => t2 : T ]]] Note that one important feature of our other STLC type extensions _fails_ for this one, namely uniqueness of types. The problem arises from the rules for [inl] and [inr]. For example, the [T_Inl] rule says that once we have shown that [t1] is an element of type [T1], we can derive that [inl t1] is an element of [T1 + T2] for _any_ type T2. For example, we can derive both [inl 5 : Nat + Nat] and [inl 5 : Nat + Bool] (and infinitely many other types). The failure of uniqueness of types means that we cannot build a typechecking algorithm simply by "reading the rules from bottom to top" as we could for all the other features seen so far. This problem could be remedied in various ways. The most direct is to require that the programmer annotate each use of [inl] and [inr] with the full sum type [T1 + T2] that is intended. But this is rather heavyweight, so we'll just ignore the problem in the remainder of this chapter, since we don't need to build a typechecker. *) (** *** Variants *) (** Just as products can be generalized to records, sums can be generalized to n-ary labeled types called _variants_. Instead of [T1+T2], we can write something like [] where [l1],[l2],... are field labels which are used both to construct instances and as case arm labels. *) (** *** Lists *) (** The typing features we have seen can be classified into _base types_ like [Bool], and _type constructors_ like [->] and [*] that build new types from old ones. Another useful type constructor is [list]. For every type [T], the type [list T] describes finite-length lists whose elements are drawn from [T]. In principle, we could develop lists given facilities for defining variants and for defining _recursive_ types. But we've skipped the details of the former, and giving semantics to the latter is quite non-trivial. Instead, we'll just discuss the special case of lists directly. Below we give the syntax, semantics, and typing rules for lists. Except for the fact that explicit type annotations are mandatory on [nil] and cannot appear on [cons], these lists are essentially identical to those we built in Coq. We use [lcase] to destruct lists, to avoid dealing with questions like "what is the [head] of the empty list?" So, for example, here is a function that calculates the sum of the first two elements of a list of numbers: << \x:list nat. lcase x of nil -> 0 | a::x' -> lcase x' of nil -> a | b::x'' -> a+b >> While we say that [cons v1 v2] is a value, we really mean that [v2] should also be a list -- we'll have to enforce this in the formal definition of value. *) (** Syntax: << t ::= Terms: | ... | nil T | cons t t | lcase t of nil -> t | x::x -> t v ::= Values: | ... | nil T nil value | cons v v cons value T ::= Types: | ... | list T list of Ts >> Reduction: [[[ t1 --> t1' -------------------------- (ST_Cons1) cons t1 t2 --> cons t1' t2 t2 --> t2' -------------------------- (ST_Cons2) cons v1 t2 --> cons v1 t2' t1 --> t1' -------------------------------------------- (ST_Lcase1) (lcase t1 of nil -> t2 | h::t -> t3) --> (lcase t1' of nil -> t2 | h::t -> t3) --------------------------------------------- (ST_LcaseNil) (lcase nil T of nil -> t2 | h::t -> t3) --> t2 ------------------------------------------------------------------ (ST_LcaseCons) (lcase (cons vh vt) of nil -> t2 | h::t -> t3) --> [vh/h,vt/t]t3 ]]] Typing: [[[ ----------------------- (T_Nil) Gamma |- nil T : list T Gamma |- t1 : T Gamma |- t2 : list T ----------------------------------------- (T_Cons) Gamma |- cons t1 t2: list T Gamma |- t1 : list T1 Gamma |- t2 : T Gamma, h:T1, t:list T1 |- t3 : T -------------------------------------------------------------------------------------- (T_Lcase) Gamma |- (lcase t1 of nil -> t2 | h::t -> t3) : T ]]] *) (** *** General Recursion *) (** Another facility found in most programming languages (including Coq) is the ability to define recursive functions. For example, we might like to be able to define the factorial function like this: << fact = \x:nat. if x=0 then 1 else x * (fact (pred x))) >> But this would be require quite a bit of work to formalize: we'd have to introduce a notion of "function definitions" and carry around an "environment" of such definitions in the definition of the [step] relation. Here is another way that is straightforward to formalize: instead of writing recursive definitions where the right-hand side can contain the identifier being defined, we can define a _fixed-point operator_ that performs the "unfolding" of the recursive definition in the right-hand side lazily during reduction. << fact = fix (\f:nat->nat. \x:nat. if x=0 then 1 else x * (f (pred x))) >> The intuition is that the higher-order function [f] passed to [fix] is a _generator_ for the [fact] function: if [f] is applied to a function that approximates the desired behavior of [fact] up to some number [n] (that is, a function that returns correct results on inputs less than or equal to [n]), then it returns a better approximation to [fact]---a function that returns correct results for inputs up to [n+1]. Applying [fix] to this generator returns its fixed point---a function that gives the desired behavior for all inputs [n]. Syntax: << t ::= Terms: | ... | fix t fixed-point operator >> Reduction: [[[ t1 --> t1' ------------------ (ST_Fix1) fix t1 --> fix t1' ------------------------------------------- (ST_FixAbs) fix (\x:T1.t2) --> [(fix(\x:T1.t2)) / x] t2 ]]] Typing: [[[ Gamma |- t1 : T1->T1 -------------------- (T_Fix) Gamma |- fix t1 : T1 ]]] *) (** **** Exercise: 1 star (halve_fix) *) (** Translate this recursive definition into one using [fix]: << halve = \x:nat. if x=0 then 0 else if (pred x)=0 then 0 else 1 + (halve (pred (pred x)))) >> (* FILL IN HERE *) [] *) (** **** Exercise: 1 star (fact_steps) *) (** Write down the sequence of steps that the term [fact 1] goes through to reduce to a normal form (assuming the usual reduction rules for arithmetic operations). (* FILL IN HERE *) [] *) (** The ability to form the fixed point of a function of type [T->T] for any [T] has some surprising consequences. In particular, it implies that _every_ type is inhabited by some term. To see this, observe that, for every type [T], we can define the term [[ fix (\x:T.x) ]] By [T-Fix] and [T-Abs], this term has type [T]. By [ST-FixAbs] it reduces to itself, over and over again. Thus it is an _undefined element_ of [T]. *) (* ###################################################################### *) (** * Formalizing the Extensions *) (** **** Exercise: 4 stars (STLC_extensions) *) (** Formalizing the extensions is left to you. We've provided the necessary extensions to the syntax of terms and types, and we've included a few examples that you can test your definitions with to make sure they are working as expected. You'll fill in the rest of the definitions and extend all the proofs accordingly. (A good strategy is to work on the extensions one at a time, in multiple passes, rather than trying to work through the file from start to finish in a single pass.) *) Module STLCExtended. (* ###################################################################### *) (** *** Syntax and Operational Semantics *) Inductive ty : Type := | ty_base : id -> ty | ty_arrow : ty -> ty -> ty | ty_unit : ty | ty_pair : ty -> ty -> ty | ty_sum : ty -> ty -> ty | ty_list : ty -> ty | ty_nat : ty. Tactic Notation "ty_cases" tactic(first) tactic(c) := first; [ c "ty_base" | c "ty_arrow" | c "ty_unit" | c "ty_pair" | c "ty_sum" | c "ty_list" | c "ty_nat" ]. Inductive tm : Type := (* pure STLC *) | tm_var : id -> tm | tm_app : tm -> tm -> tm | tm_abs : id -> ty -> tm -> tm (* unit *) | tm_unit : tm (* pairs *) | tm_pair : tm -> tm -> tm | tm_fst : tm -> tm | tm_snd : tm -> tm (* sums *) | tm_inl : tm -> tm | tm_inr : tm -> tm | tm_case : tm -> id -> tm -> id -> tm -> tm (* i.e., [case t0 of inl x1 => t1 | inr x2 => t2] *) (* lists *) | tm_nil : ty -> tm | tm_cons : tm -> tm -> tm | tm_lcase : tm -> tm -> id -> id -> tm -> tm (* i.e., [lcase t1 of | nil -> t2 | x::y -> t3] *) (* numbers *) | tm_nat : nat -> tm | tm_succ : tm -> tm | tm_pred : tm -> tm | tm_mult : tm -> tm -> tm | tm_if0 : tm -> tm -> tm -> tm (* let *) | tm_let : id -> tm -> tm -> tm (* i.e., [let x = t1 in t2] *) (* fix *) | tm_fix : tm -> tm. (** Note that, for brevity, we've chosen a compressed version of the numeric operations, with a single [if0] form combining a zero test and a conditional. *) Tactic Notation "tm_cases" tactic(first) tactic(c) := first; [ c "tm_var" | c "tm_app" | c "tm_abs" | c "tm_unit" | c "tm_pair" | c "tm_fst" | c "tm_snd" | c "tm_inl" | c "tm_inr" | c "tm_case" | c "tm_nil" | c "tm_cons" | c "tm_lcase" | c "tm_nat" | c "tm_succ" | c "tm_pred" | c "tm_mult" | c "tm_if0" | c "tm_let" | c "tm_fix" ]. (** Some variables, for use in examples... *) Notation a := (Id 0). Notation f := (Id 1). Notation g := (Id 2). Notation l := (Id 3). Notation A := (ty_base (Id 4)). Notation B := (ty_base (Id 5)). Notation k := (Id 6). Notation i1 := (Id 7). Notation i2 := (Id 8). (* ###################################################################### *) (** *** Substitution *) Fixpoint subst (x:id) (s:tm) (t:tm) : tm := match t with | tm_var y => if beq_id x y then s else t | tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1)) | tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2) (* FILL IN HERE *) | _ => t (* ... and delete this line *) end. (* ###################################################################### *) (** *** Reduction *) (** Next we define the values of our language. *) Inductive value : tm -> Prop := | v_abs : forall x T11 t12, value (tm_abs x T11 t12) (* FILL IN HERE *) . Hint Constructors value. Reserved Notation "t1 '-->' t2" (at level 40). Inductive step : tm -> tm -> Prop := | ST_AppAbs : forall x T11 t12 v2, value v2 -> (tm_app (tm_abs x T11 t12) v2) --> (subst x v2 t12) | ST_App1 : forall t1 t1' t2, t1 --> t1' -> (tm_app t1 t2) --> (tm_app t1' t2) | ST_App2 : forall v1 t2 t2', value v1 -> t2 --> t2' -> (tm_app v1 t2) --> (tm_app v1 t2') (* FILL IN HERE *) where "t1 '-->' t2" := (step t1 t2). Tactic Notation "step_cases" tactic(first) tactic(c) := first; [ c "ST_AppAbs" | c "ST_App1" | c "ST_App2" | (* FILL IN HERE *) ]. Notation stepmany := (refl_step_closure step). Notation "t1 '-->*' t2" := (stepmany t1 t2) (at level 40). Hint Constructors step. (* ###################################################################### *) (** *** Typing *) Definition context := partial_map ty. (** Next we define the typing rules. These are nearly direct transcriptions of the inference rules shown above. *) Inductive has_type : context -> tm -> ty -> Prop := (* Typing rules for proper terms *) | T_Var : forall Gamma x T, Gamma x = Some T -> has_type Gamma (tm_var x) T | T_Abs : forall Gamma x T11 T12 t12, has_type (extend Gamma x T11) t12 T12 -> has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12) | T_App : forall T1 T2 Gamma t1 t2, has_type Gamma t1 (ty_arrow T1 T2) -> has_type Gamma t2 T1 -> has_type Gamma (tm_app t1 t2) T2 (* FILL IN HERE *) . Hint Constructors has_type. Tactic Notation "has_type_cases" tactic(first) tactic(c) := first; [ c "T_Var" | c "T_Abs" | c "T_App" (* FILL IN HERE *) ]. (* ###################################################################### *) (** ** Examples *) (** **** Exercise: 2 stars (examples) *) (** Finish the proofs. *) (* fact := fix (\f:nat->nat. \a:nat. if a=0 then 1 else a * (f (pred a))) *) Definition fact := tm_fix (tm_abs f (ty_arrow ty_nat ty_nat) (tm_abs a ty_nat (tm_if0 (tm_var a) (tm_nat 1) (tm_mult (tm_var a) (tm_app (tm_var f) (tm_pred (tm_var a))))))). (** (Warning: you may be able to typecheck [fact] but still have some rules wrong!) *) (* These hints improve the automation for [has_type]. It says that whenever [auto] arrives at a goal of the form [(has_type G (tm_app e1 e1) T)], it should consider [eapply T_App], leaving an existential variable for the middle type T1, and similar for [lcase]. That variable will then be filled in during the search for type derivations for [e1] and [e2]. We also include a hint to "try harder" when solving equality goals; this is useful to automate uses of T_Var (which includes an equality as a precondition). *) Hint Extern 2 (has_type _ (tm_app _ _) _) => eapply T_App; auto. (** << (* Uncomment this once you've defined the [T_Lcase] constructor for the typing relation: *) Hint Extern 2 (has_type _ (tm_lcase _ _ _ _ _) _) => eapply T_Lcase; auto. >> *) Hint Extern 2 (_ = _) => compute; reflexivity. Example fact_typechecks : has_type (@empty ty) fact (ty_arrow ty_nat ty_nat). Proof with auto. (* FILL IN HERE *) Admitted. Example fact_example: (tm_app fact (tm_nat 4)) -->* (tm_nat 24). Proof. (* FILL IN HERE *) Admitted. (* map := \g:nat->nat. fix (\f:[nat]->[nat]. \l:[nat]. case l of | [] -> [] | x::l -> (g x)::(f l)) *) Definition map := tm_abs g (ty_arrow ty_nat ty_nat) (tm_fix (tm_abs f (ty_arrow (ty_list ty_nat) (ty_list ty_nat)) (tm_abs l (ty_list ty_nat) (tm_lcase (tm_var l) (tm_nil ty_nat) a l (tm_cons (tm_app (tm_var g) (tm_var a)) (tm_app (tm_var f) (tm_var l))))))). Example map_typechecks : has_type empty map (ty_arrow (ty_arrow ty_nat ty_nat) (ty_arrow (ty_list ty_nat) (ty_list ty_nat))). Proof with auto. (* FILL IN HERE *) Admitted. Example map_example : tm_app (tm_app map (tm_abs a ty_nat (tm_succ (tm_var a)))) (tm_cons (tm_nat 1) (tm_cons (tm_nat 2) (tm_nil ty_nat))) -->* (tm_cons (tm_nat 2) (tm_cons (tm_nat 3) (tm_nil ty_nat))). Proof with auto. (* FILL IN HERE *) Admitted. (** [] *) (* ###################################################################### *) (** ** Properties of Typing *) (** The proofs of progress and preservation for this system are essentially the same (though of course somewhat longer) as for the pure simply typed lambda-calculus. *) (* ###################################################################### *) (** *** Progress *) Theorem progress : forall t T, has_type empty t T -> value t \/ exists t', t --> t'. Proof with eauto. (* Theorem: Suppose empty |- t : T. Then either 1. t is a value, or 2. t --> t' for some t'. Proof: By induction on the given typing derivation. *) intros t T Ht. remember (@empty ty) as Gamma. generalize dependent HeqGamma. (has_type_cases (induction Ht) Case); intros HeqGamma; subst. Case "T_Var". (* The final rule in the given typing derivation cannot be [T_Var], since it can never be the case that [empty |- x : T] (since the context is empty). *) inversion H. Case "T_Abs". (* If the [T_Abs] rule was the last used, then [t = tm_abs x T11 t12], which is a value. *) left... Case "T_App". (* If the last rule applied was T_App, then [t = t1 t2], and we know from the form of the rule that [empty |- t1 : T1 -> T2] [empty |- t2 : T1] By the induction hypothesis, each of t1 and t2 either is a value or can take a step. *) right. destruct IHHt1; subst... SCase "t1 is a value". destruct IHHt2; subst... SSCase "t2 is a value". (* If both [t1] and [t2] are values, then we know that [t1 = tm_abs x T11 t12], since abstractions are the only values that can have an arrow type. But [(tm_abs x T11 t12) t2 --> subst x t2 t12] by [ST_AppAbs]. *) inversion H; subst; try (solve by inversion). exists (subst x t2 t12)... SSCase "t2 steps". (* If [t1] is a value and [t2 --> t2'], then [t1 t2 --> t1 t2'] by [ST_App2]. *) destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')... SCase "t1 steps". (* Finally, If [t1 --> t1'], then [t1 t2 --> t1' t2] by [ST_App1]. *) destruct H as [t1' Hstp]. exists (tm_app t1' t2)... (* FILL IN HERE *) Qed. (* ###################################################################### *) (** *** Context Invariance *) Inductive appears_free_in : id -> tm -> Prop := | afi_var : forall x, appears_free_in x (tm_var x) | afi_app1 : forall x t1 t2, appears_free_in x t1 -> appears_free_in x (tm_app t1 t2) | afi_app2 : forall x t1 t2, appears_free_in x t2 -> appears_free_in x (tm_app t1 t2) | afi_abs : forall x y T11 t12, y <> x -> appears_free_in x t12 -> appears_free_in x (tm_abs y T11 t12) (* FILL IN HERE *) . Hint Constructors appears_free_in. Lemma context_invariance : forall Gamma Gamma' t S, has_type Gamma t S -> (forall x, appears_free_in x t -> Gamma x = Gamma' x) -> has_type Gamma' t S. Proof with eauto. intros. generalize dependent Gamma'. (has_type_cases (induction H) Case); intros Gamma' Heqv... Case "T_Var". apply T_Var... rewrite <- Heqv... Case "T_Abs". apply T_Abs... apply IHhas_type. intros y Hafi. unfold extend. remember (beq_id x y) as e. destruct e... (* FILL IN HERE *) Qed. Lemma free_in_context : forall x t T Gamma, appears_free_in x t -> has_type Gamma t T -> exists T', Gamma x = Some T'. Proof with eauto. intros x t T Gamma Hafi Htyp. (has_type_cases (induction Htyp) Case); inversion Hafi; subst... Case "T_Abs". destruct IHHtyp as [T' Hctx]... exists T'. unfold extend in Hctx. apply not_eq_beq_id_false in H2. rewrite H2 in Hctx... (* FILL IN HERE *) Qed. (* ###################################################################### *) (** *** Preservation *) Lemma substitution_preserves_typing : forall Gamma x U v t S, has_type (extend Gamma x U) t S -> has_type empty v U -> has_type Gamma (subst x v t) S. Proof with eauto. (* Theorem: If Gamma,x:U |- t : S and empty |- v : U, then Gamma |- (subst x v t) S. *) intros Gamma x U v t S Htypt Htypv. generalize dependent Gamma. generalize dependent S. (* Proof: By induction on the term t. Most cases follow directly from the IH, with the exception of tm_var and tm_abs. The former aren't automatic because we must reason about how the variables interact. *) (tm_cases (induction t) Case); intros S Gamma Htypt; simpl; inversion Htypt; subst... Case "tm_var". simpl. rename i into y. (* If t = y, we know that [empty |- v : U] and [Gamma,x:U |- y : S] and, by inversion, [extend Gamma x U y = Some S]. We want to show that [Gamma |- subst x v y : S]. There are two cases to consider: either [x=y] or [x<>y]. *) remember (beq_id x y) as e. destruct e. SCase "x=y". (* If [x = y], then we know that [U = S], and that [subst x v y = v]. So what we really must show is that if [empty |- v : U] then [Gamma |- v : U]. We have already proven a more general version of this theorem, called context invariance. *) apply beq_id_eq in Heqe. subst. unfold extend in H1. rewrite <- beq_id_refl in H1. inversion H1; subst. clear H1. eapply context_invariance... intros x Hcontra. destruct (free_in_context _ _ S empty Hcontra) as [T' HT']... inversion HT'. SCase "x<>y". (* If [x <> y], then [Gamma y = Some S] and the substitution has no effect. We can show that [Gamma |- y : S] by [T_Var]. *) apply T_Var... unfold extend in H1. rewrite <- Heqe in H1... Case "tm_abs". rename i into y. rename t into T11. (* If [t = tm_abs y T11 t0], then we know that [Gamma,x:U |- tm_abs y T11 t0 : T11->T12] [Gamma,x:U,y:T11 |- t0 : T12] [empty |- v : U] As our IH, we know that forall S Gamma, [Gamma,x:U |- t0 : S -> Gamma |- subst x v t0 S]. We can calculate that subst x v t = tm_abs y T11 (if beq_id x y then t0 else subst x v t0) And we must show that [Gamma |- subst x v t : T11->T12]. We know we will do so using [T_Abs], so it remains to be shown that: [Gamma,y:T11 |- if beq_id x y then t0 else subst x v t0 : T12] We consider two cases: [x = y] and [x <> y]. *) apply T_Abs... remember (beq_id x y) as e. destruct e. SCase "x=y". (* If [x = y], then the substitution has no effect. Context invariance shows that [Gamma,y:U,y:T11] and [Gamma,y:T11] are equivalent. Since the former context shows that [t0 : T12], so does the latter. *) eapply context_invariance... apply beq_id_eq in Heqe. subst. intros x Hafi. unfold extend. destruct (beq_id y x)... SCase "x<>y". (* If [x <> y], then the IH and context invariance allow us to show that [Gamma,x:U,y:T11 |- t0 : T12] => [Gamma,y:T11,x:U |- t0 : T12] => [Gamma,y:T11 |- subst x v t0 : T12] *) apply IHt. eapply context_invariance... intros z Hafi. unfold extend. remember (beq_id y z) as e0. destruct e0... apply beq_id_eq in Heqe0. subst. rewrite <- Heqe... (* FILL IN HERE *) Qed. Theorem preservation : forall t t' T, has_type empty t T -> t --> t' -> has_type empty t' T. Proof with eauto. intros t t' T HT. (* Theorem: If [empty |- t : T] and [t --> t'], then [empty |- t' : T]. *) remember (@empty ty) as Gamma. generalize dependent HeqGamma. generalize dependent t'. (* Proof: By induction on the given typing derivation. Many cases are contradictory ([T_Var], [T_Abs]). We show just the interesting ones. *) (has_type_cases (induction HT) Case); intros t' HeqGamma HE; subst; inversion HE; subst... Case "T_App". (* If the last rule used was [T_App], then [t = t1 t2], and three rules could have been used to show [t --> t']: [ST_App1], [ST_App2], and [ST_AppAbs]. In the first two cases, the result follows directly from the IH. *) inversion HE; subst... SCase "ST_AppAbs". (* For the third case, suppose [t1 = tm_abs x T11 t12] and [t2 = v2]. We must show that [empty |- subst x v2 t12 : T2]. We know by assumption that [empty |- tm_abs x T11 t12 : T1->T2] and by inversion [x:T1 |- t12 : T2] We have already proven that substitution_preserves_typing and [empty |- v2 : T1] by assumption, so we are done. *) apply substitution_preserves_typing with T1... inversion HT1... (* FILL IN HERE *) Qed. (** [] *) End STLCExtended.