# Homework 4
- Chiao Lu
- UID: 204848946
- Email: [e-mail]
- Aishni Parab
- UID: 905526328
- Email: [e-mail]

## Problem 1
### (a)
<pre>
function p:((A &and; B) &and; C) &rightarrow;
let a = fst (fst p) in
let b = snd (fst p) in
let c = snd p in
(a, (b, c))
</pre>

### (b)
<pre>
function p:((A &or; B) &or; C) &rightarrow;
match p with
| left aorb &rightarrow;
match aorb with
| left a &rightarrow; left a
| right b &rightarrow; right (left b)
| right c &rightarrow; right (right c)
</pre>

### (c\)
<pre>
function p:((A &or; B) &rightarrow; C) &rightarrow;
(
function p1:A &rightarrow; p (left p1),
function p2:B &rightarrow; p (right p2)
)
</pre>

### (d)
<pre>
function p1:(A &rightarrow; B) &rightarrow;
function p2:(B &rightarrow; False) &rightarrow;
function p3:A &rightarrow;
p2 (p1 p3)
</pre>

## Problem 2
### (a)
Reference: [https://piazza.com/class_profile/get_resource/h82u3exc6351np/h860gvgnm2e1dr](https://piazza.com/class_profile/get_resource/h82u3exc6351np/h860gvgnm2e1dr)

If we have this rule
<pre>
t1 &rightarrow; t1'
------------------------------
while t1 do t2 &rightarrow; while t1' do t2
</pre>

We would also need something like the following

<pre>
------------------------------
while true do t2 &rightarrow; ???
</pre>

This is basically telling us to keep evaluating `t1` until it is `true` or `false`, and then we must either enter an _infinite loop_ or _not enter the loop at all_, which is definitely not the desired behaviour of `while`. We need the `while` loop to keep looking at `t1` until it evaluates to `false`, instead of just once.

### (b)
Online reference above is suggesting something like <code>if t1 then (t2; while t1 do t2) else ()</code>. We convert the sequencing (`;`) to `let` as discussed in the lecture (`t1;t2 --> let x=t1 in t2`). After that, as pointed out in the Campuswire hint by Todd, we can't use `let` so we convert it further to function call (`E-LetSugar`).

<pre>
fresh x
------------------------------
while t1 do t2 &rightarrow;
if t1 then ((function x:True &rightarrow; while t1 do x) t2) else ()
</pre>

### (c\)
<pre>
&Gamma; &RightTee; t1:Bool &Gamma; &RightTee; t2:True
------------------------------
&Gamma; &RightTee; while t1 do t2:True
</pre>

### (d)
<pre>
function whileFun f1:(True &rightarrow; Bool) f2:(True &rightarrow; True) &rightarrow;
let rec loop =
function p1:(True &rightarrow; Bool) p2:(True &rightarrow; True) &rightarrow;
if (p1 ()) then (let x=(p2 ()) in (loop p1 p2)) else ()
in
(loop f1 f2)
</pre>

## Problem 3
### (a)
<pre>
------------------ (I-Var) ------------------ (I-Var)
tinfer({f:X1,x:X2}, f) = &#10112; tinfer({f:X1,x:X2}, x) = &#10113;
-------------------- (I-Var) --------------------------------------------- (I-App)
tinfer({f:X1,x:X2}, f) = &#10114; tinfer({f:X1,x:X2}, f x) = &#10115;
--------------------------------------------------------------------------- (I-App)
tinfer({f:X1,x:X2}, f (f x)) = &#10116;
--------------------------------------------------------------------------- (I-Fun)
tinfer({f:X1}, function x &rightarrow; f (f x)) = &#10117;
--------------------------------------------------------------------------- (I-Fun)
tinfer({}, function f &rightarrow; function x &rightarrow; f (f x)) = &#10118;
</pre>

Where
<pre>
&#10112; = (X3, {X3=X1})
&#10113; = (X4, {X4=X2})
&#10114; = (X5, {X5=X1})
&#10115; = (X6, {X3=X1}&bigcup;{X4=X2}&bigcup;{X3=X4&rightarrow;X6})
&#10116; = (X7, {X5=X1}&bigcup;{X3=X1}⋃{X4=X2}⋃{X3=X4→X6}&bigcup;{X5=X6&rightarrow;X7})
&#10117; = (X8, {X5=X1}&bigcup;{X3=X1}⋃{X4=X2}⋃{X3=X4→X6}&bigcup;{X5=X6&rightarrow;X7}&bigcup;{X8=X2&rightarrow;X7})
&#10118; = (X9, {X5=X1}&bigcup;{X3=X1}⋃{X4=X2}⋃{X3=X4→X6}&bigcup;{X5=X6&rightarrow;X7}&bigcup;{X8=X2&rightarrow;X7}&bigcup;{X9=X1&rightarrow;X8})
</pre>

### (b)

<pre>
x:Int
f:Int&rightarrow;Int

X1=Int&rightarrow;Int
X2=Int
X3=Int&rightarrow;Int
X4=Int
X5=Int&rightarrow;Int
X6=Int
X7=Int
X8=Int&rightarrow;Int
X9=(Int&rightarrow;Int)&rightarrow;Int&rightarrow;Int
</pre>

Putting this into ocaml shell gives

─( 05:13:55 )─< command 0 >────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # function f -> function x -> f (f x);;
- : ('a -> 'a) -> 'a -> 'a = <fun>
─( 05:13:55 )─< command 1 >────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # function (f:int->int) -> function (x:int) -> f (f x);;
- : (int -> int) -> int -> int = <fun>

## Problem 4
<pre>
tinfer(G, s) = (S1, C1)
fresh T2
fresh X
--------------------------- (I-Left)
tinfer(G, left s) = (X, C1 &bigcup; {X=S1&vee;T2})

tinfer(G, s) = (S2, C2)
fresh T1
fresh X
--------------------------- (I-Right)
tinfer(G, right s) = (X, C2 &bigcup; {X=T1&vee;S2})

fresh X
fresh X1
fresh X2
tinfer((G, x1:X1), s1) = (S1, C1)
tinfer((G, x2:X2), s2) = (S2, C2)
tinfer(G, s) = (S, C)
------------------------------------(I-Match)
tinfer(G, match s with left x1&rightarrow;s1 |
right x2&rightarrow;s2)
= (X, C &bigcup; C1 &bigcup; C2 &bigcup; {S=S1&vee;S2, X=S})

</pre>