To create the context for dealing with this extension, we first change the type declaration for representing types to the following:

 type ty = BoolTy | IntTy | FunTy of ty * ty 

What we have done here is include a new case to represent function types. Thus the type written as int -> int in OCaml will be represented by (FunTy (IntTy,IntTy)) using this data type.

We next include two new cases in the collection of expressions we considered earlier, one for forming a function and the other for permitting the application of one expression to another:

 type expr' = | Id' of string (* for identifiers *) | Int' of int (* for integer values *) | True' (* for the boolean value true *) | False' (* for the boolean value false *) | Plus' of expr' * expr' (* for exp1 + exp2 *) | Minus' of expr' * expr' (* for exp1 - exp2 *) | Lss' of expr' * expr' (* for exp1 < exp2 *) | Gtr' of expr' * expr' (* for exp1 > exp2 *) | And' of expr' * expr' (* for exp1 && exp2 *) | Or' of expr' * expr' (* for exp1 || exp2 *) | Cond' of expr' * expr' * expr' (* for if exp1 then exp2 else exp3 *) | Fun' of string * ty * expr' (* for fun (x:ty) -> exp *) | App' of expr' * expr' (* for (exp1 exp2) *) 

We have changed the names of the type and the constructors used in the lab slightly, adding a "prime" at the end of each. It is important that you stick to this convention to avoid confusion with the type and constructors we will use in the next problem. Ignoring this "cosmetic" change, the only difference between the definition in the lab and the one above is in the addition of the last two cases.

Let us understand what the additions mean. The Fun' constructor allows us to represent function expressions in OCaml. For example, the expression we would write as (fun (x:int) -> x + 1) in OCaml would be represented using the type shown as

 Fun' ("x",IntTy,Plus' (Id' "x",Int' 1)) 

Note that although OCaml allows us to write function expressions without indicating the type of the argument, we do not permit that here so as to keep the problem manageable: we will focus on type checking and will not try our hand at type inference.

The second new constructor, App', allows us to represent function application. For example, if we want to represent the OCaml expression ((fun (x:int) -> x + 1) 5), we would use the following in our encoding:

 App' (Fun' ("x",IntTy, Plus' (Id' "x", Int' 1)), Int' 5). 

Of course, some OCaml expressions that we represent may be ill-typed. For example, the expression ((fun (x:int) -> x + 1) true) is not well-typed. The objective in this problem is to write an OCaml function that will give us the type of well-typed expressions and will tell us when an expression is ill-typed for the collection of expression forms included in the type declaration above.

1. Let us first make sure you have understood the representation described above. Present the representations of the following OCaml expressions

a. (fun (x:int) -> (fun (y:bool) -> if y then (x+1) else x-5))

b. (fun (x:int) -> ((fun (y:int) -> x + y) x)) 5

These representations must be contained in your hw2.ml file in the form of two let bindings that look like the following:

 let exp1' = ... let exp2' = ... 

where the ... part is filled in with the relevant representation. Make sure to use the prime in the name to avoid confusion with the next part.

2. When trying to type check the body of a function, you have to do it in a context that tells you what the type of the function argument is. We will represent such a context as a list of identifier name and type pairs. Assuming such a representation, define the function

 typeof_aux : expr' -> (string * ty) list -> ty option 

that takes an expression and a list of identifier name and type associations and returns the result None if the expression is not typeable or the result (Some Ty) if the expression is typeable and Ty is a representation of its type. Some example uses of this function:

 # typeof_aux (Plus' (Id' "x",Int' 5)) [("x",IntTy)];; - : ty option = Some IntTy # typeof_aux (And' (Id' "x",True')) [("x",IntTy)];; - : ty option = None # typeof_aux (Fun' ("x", BoolTy, And' (Id' "x",True'))) [("x",IntTy)];; - : ty option = Some (FunTy (BoolTy, BoolTy)) # typeof_aux (App' (Fun' ("x",IntTy, Plus' (Id' "x", Int' 1)), Int' 5)) [];; - : ty option = Some IntTy # typeof_aux (Cond' (True', True', False')) [];; - : ty option = Some BoolTy # typeof_aux (Cond' (True', Fun' ("x",IntTy,Id' "x"), Fun' ("y",IntTy,Int' 5))) [];; - : ty option = Some (FunTy (IntTy, IntTy)) # 

Looking at the third example here, you should see that when a context contains multiple type bindings for the same identifier, the one occurring closest to the expression is the one that dominates. Looking at the last two examples, you should see that the then and else branches for an if-then-else can be of arbitrary type, the only requirement is that their types have to be identical.

A question that might concern you: What if the expression that is input as the first argument contains identifiers that are not bound by a Fun and also do not have an entry in the second (list) argument? Assume that this will never happen, i.e. we will call this function only after we have checked that an expression is well-formed in the way discussed in class.

3. Using the typeof_aux function, define the function

 typeof : expr' -> ty option 

that takes a representation of an expression and returns None if the expression is not typeable or (Some Ty) where Ty if the expression is typeable and Ty is a representation of its type.

Language: Ocaml