Description
Use type derivations to answer the questions below. For every step of your derivation, you are required to write the acronym for the rule you are applying next to the corresponding horizontal bar. Acronyms can be found in the type-checking rules sheet. 1. Show that the following expression: (x + 2 > 3) && y Has type bool in the environment Γ = { x:int, y:bool }. 2. Show that the following expression: fn f => fn x => if x then f true else 19 Has type (bool->int)->bool->int in the environment Γ = { }. 3. Show that the following expression: let fun f x = 5 < x in fn y => (f 3) || y end Has type bool->bool in the environment Γ = { }. Infer the types of each of the expressions below, and all their subexpressions. For every step of your derivation, you are required to write the acronym for the rule you are applying next to the corresponding horizontal bar. You are also required to write the constraint generated by each rule application (if any) as a footnote. For every step of unification, you are required to write the operation you apply in each step. If the expression contains a type error, show where unification fails. 4. fn x => if x then x + 1 else x(1) 5. let fun fact x = if x = 0 then 1 else fact (x – 1) in fact end Submission Instructions Put all your solutions in one PDF file and submit it via Moodle. The file should be named “.pdf” where is your AUBnet ID (e.g., abc01.pdf). Do not submit any other files or compressed folders.
