Description
1 STLC In this section, refer to the syntax and typing rules for the Simply-typed λ calculus, given in lecture. Task 1.1 (Written, 12 points). Give the STLC types of the following expressions: (a) λx : unit.x (b) ((), λx : unit.x) (c) λx : unit.(x, x) (d) snd ((),()) 1 Task 1.2 (Written, 9 points). Give a typing derivation for • ` λf : unit → (unit × unit).fst (f ()) : (unit → (unit × unit)) → unit. Updated Apr. 16 : Resulting type was fixed 2 MiniCaml Image Credit: Petr Kratochvil In this section, we will be working with MiniCaml, a language with more features than MicrOCaml from Homeworks 3 and 4, but still not quite all the features of OCaml. The grammar of MiniCaml is shown below. op → + | – | * | / | < | ≤ | > | ≥ | = | <> | && | || | ^ τ → int | string | bool | unit | τ list | τ -> τ | τ * τ e → var | num | string | true | false | () | [] | e op e | fun var -> e | if e then e else e | let pat optannot = e in e | let var pat optannot = e in e | let rec var pat optannot = e in e | let (var , var ) = e in e | e e | match e with [] -> e | var::var -> e | e, e | e::e | e : e pat → var | (var : τ ) optannot → | : τ decl → let pat optannot = e;; | let var pat optannot = e;; | let rec var pat optannot = e;; | e;; prog → decl | decl prog You may notice that you can actually write a pretty large subset of OCaml in MiniCaml without making any changes. In particular, we’ve gotten rid of MicrOCaml’s odd app e to e syntax and replaced it with normal OCaml application. One nice result of this is that, while you can’t necessarily take any OCaml program and run it in MiniCaml, you can run any MiniCaml program through OCaml (ocaml or TryOCaml) to figure out what types it should have or what the result should be. A couple non-obvious restrictions present in MiniCaml: 1. Pattern matching is limited to using let to break apart pairs and using match to match on a list (note that we haven’t defined fst or snd: you have to break apart pairs with pattern matching; you can define them yourself though). 2 2. Functions (both lambdas and let-defined functions) can only take one argument. You can get around this with currying (though that doesn’t work well for recursive functions) or having functions take pairs (see map in examples/rec.ml). 3. As in OCaml, a program consists of one or more top-level declarations, where a declaration can be a let declaration or an expression by itself. Unlike in OCaml, these declarations must be followed by two semicolons (see the midterm for why this makes our lives easier writing the parser). 4. You can’t use type variables in annotations (e.g. let f (x: ’a) : ’a = x. MiniCaml can still infer polymorphic types with type variables though. The type definitions for MiniCaml are given in types.ml and described in the walkthrough video on Blackboard. The file unify.ml contains code to unify two types, which is used in type checking. Unification in MiniCaml works very similarly to unification in STLC, with a couple of extensions. Recall that unification takes two types τ1 and τ2, potentially with unification variables like ?1. These are “holes” that can be unified with anything. Each instance of a particular variable must be filled with the same thing though (for example, if ?1 appears in both types, you must replace ?1 with the same type in both). In class, we considered an imperative version of unification that “magically” updates unification variables. On this homework, we’ll consider a functional unification algorithm that instead returns a substitution, which is a list of pairs (?i , τi) meaning “replace ?i with τi” (Updated 4/14 : Typo fix). As with substituting values for variables, we can write [τi/?i ]τ to mean “τ with all instances of ?i replaced by τi .” For a substitution σ, we’ll write [σ]τ to mean “τ with all the replacements in σ”. So, for example, [[(?0, int); (?1, string)]](?0 -> ?1) = int -> string and [[(?0, ?1 list); (?1, int)]]?0 = int list The OCaml definition for substitutions is given in unify.ml: type substitution = (int * typ) list In that definition, ?0 is represented as just the integer 0. We also include a function sub all : substitution -> typ -> typ,where sub all s t computes [s]t. Here’s the (recursive) unification algorithm: Algorithm: Unify(τ1, τ2) Returns a substitution or an error. 1. If τ1 and τ2 are both the same base type (int, string, bool or unit), return the empty list []. 2. If τ1 = τ2 =?i (i.e., they are the same unification variable), return []. 3. If τ1 =?i , then: (a) If ?i occurs in τ2, then error. (b) Otherwise, return [(?i , τ2)]. 4. If τ2 =?i , then: (a) If ?i occurs in τ1, then error. (b) Otherwise, return [(?i , τ1)]. Updated 4/13 : the return values of these two cases were swapped 5. If τ1 = τ 0 1 list and τ2 = τ 0 2 list, then return Unify(τ 0 1 , τ 0 2 ) 6. If τ1 = τ 0 1 -> τ 00 1 and τ2 = τ 0 2 -> τ 00 2 then let σ = Unify(τ 0 1 , τ 0 2 ) and return σ concatenated with Unify([σ]τ 00 1 , [σ]τ 00 2 ). 3 7. Similar to above for if τ1 = τ 0 1 * τ 00 1 and τ2 = τ 0 2 * τ 00 2 8. Otherwise, error. Case 6 above is worth discussing in more detail. When we unify τ 0 1 and τ 0 2 , we get a substitution σ, which gives us several substitutions we need to perform. We need to perform those substitutions immediately on τ 00 1 and τ 00 2 before unifying them, because σ might tell us something like “replace ?0 with unit”, and τ 00 1 might have ?0 in it. To make this clearer, suppose τ1 = int -> string and τ2 =?0 -> ?0. Then, we have τ 0 1 = int, τ 00 2 =?0, τ 00 1 = string and τ 00 2 =?0. When we unify int and ?0, we get the substitution [(?0, int)]. If we then go ahead and unify string and ?0, we’d get the substitution [(?0, string)]. Now, we have to somehow reconcile these two substitutions, which of course isn’t possible because ?0 can’t be both int and string. Instead, we unify [[(?0, int)]]string = string and [[(?0, int)]]?0 = int, which gives us an error (which is what we want because these two types can’t be unified.) Task 2.1 (Written, 14 points). For each of the following pairs of types, say whether or not the two types can be unified. If they can, give the substitution that results. If not, briefly (in one sentence or so) describe why not. (a) int * ?1 ?2 (b) int * ?1 ?2 * string (c) int * ?1 ?1 * string (d) int -> ?1 string -> ?2 (e) ?1 -> ?2 ?3 * ?4 (f) ?1 list ?2 list list (g) ?1 list ?1 Task 2.2 (Programming, 15 points). Implement the function unify : typ -> typ -> typ in unify.ml, following the algorithm above. The file unify.ml also contains one other function you might want: new type : unit -> typ generates a new type consisting of just a unification variable ?n where ?n hasn’t been used in the program before. This is useful for when we need to “guess” types to unify later. The file typecheck.ml includes code to typecheck MiniCaml programs. It uses the unification function you wrote above. We did most of the work, you just need to implement one small function that infers the types of constants. Task 2.3 (Programming, 5 points). Implement the function type of const : const -> typ in typecheck.ml. The function should return the type of the given constant. You shouldn’t need to do any unification. In the case of Nil, which represents the empty list [], the type is of course τ list for some τ . What’s τ? We have no way of knowing at this point, so you’ll just have to take a guess… You can use new type, as well as any other functions from unify.ml. 2.1 Testing You can write tests using assert in the files you edited, as usual. When you’re done, you can also use make to compile all of the code we gave you, which together makes a typechecker and interpreter for MiniCaml. You can run it using ./miniml Where is a MiniCaml file. We’ve given you several examples in examples, as well as several examples that should not typecheck in examples/error. MiniCaml will read in the file, typecheck all of the declarations, print out their types, and then evaluate them and print out their values (as in the OCaml toplevel, functions will not be printed). For example: 4 $./miniml examples/rec.ml sum: int list -> int length: ’a list -> int map: (’d -> ’c * ’d list) -> ’c list int_to_string: int -> string onetwothree: string list sum = length = map = int_to_string = onetwothree = (one)::((two)::((three)::([]))) $ You can also use MiniCaml like the OCaml toplevel by giving no arguments: $ ./miniml Welcome to MiniCaml. Type #quit;; to exit. # 3;; -: int – = 3 # (3, “Hi!”);; -: int * string – = (3, “Hi!”) # fun x -> x;; -: ’b -> ’b – = # #quit;; 3 Standard Written Questions Task 3.1 (Written, 0 points). How long (approximately, in hours/minutes of actual working time) did you spend on this homework, total? Your honest feedback will help us with future homeworks. Task 3.2 (Written, 0 points). Who, if anyone, did you collaborate with (and in what way), and what outside sources, if any, did you consult in working on this homework? 5
