Type Inference We extend the MicroCaml programming language in Assignment 5 with an additional construct called Pair. A pair {u1,u2} consists of two elements u1 and u2, each of which may have a different type. type op = Add | Sub | .. type var = string type expr = I Int of int Bool of bool String of string I 10 of var I Fun of var * expr Not of expr Binop of op * expr * expr I If of expr * expr * expr | Functioncall of expr * expr | Let of var * bool * expr * expr | Pair of exper * expr (* Extend MicroCaml with pair *) type typeScheme = | TNum | TBool | TStr| T of string. | TFun of typeScheme * typeScheme | TPair of typeScheme * typeScheme (* Add pair types *) We assume the parser has also been extended so it can parse a pair in the syntax {u1,u2} as an abstract syntax tree Pair (u1,u2). For example, the extended MicroCaml language allows you to write a program as follows: letrecfxy=ifxthen{fy,y}else{y,fx} We also extended typeScheme to support pair types. A pair type for Pair (u1,u2) is in the shape of {t1t2} where t1 is the type of u1 and t2 is the type of u2. For example, the type the expression {T, "hello"\} is \{int * string \} or TPair (TNum, TStr). (a) (1 point) Provide a typing rule in a similar style as in the Assignment 5 description for pairs {u1,u2}. (b) (1 point) Consider the unify implementation in Assignment 5. What would you put in place for the blank such that unify can be applied for type inference of MicroCarnl prograrns with pairs? let rec unify (constraints: (typescheme * typescheme) list) : substitutions - match constraints with [ [] >[] ( x,y)::xs> let t2 - unify xs in let t1 - unify_one (apply t2 x ) (apply t2 y) in t 1 i 2 and unify_one (t1: typeScheme) (t2: typeScheme) : substitutions - match t1,t2 with | TNum, TNum | TBool, TBool | TStr, TStr - [] T(x),zz,T(x)>[(x,z)] T Trun (a,b),TFun(x,y)x unify [(a,x);(b,y)] (x Fili in the blank to complete shify for pairs *) TPair (a, b), TPair (x,y)> |_-> raise (failwith "mismatched types') (c) (1 point) Wite down the type of letrecfxyifxthen{fy,y}else{y,fx} (d) (1 point) Consider the following prograrn: let f - fun x>x in let y=f1 in f hello Is the type inference algorithrn, as inplemented in Assignment 5, capable of deducing the type of this program? If your response is negative, provide a rationale for your