OCaml Program
Checking:
Static
Dynamic
Hybrid
 
contract f = ({u | true} -> {v | u=v} -> {w | true}) -> {x | true} -> {y | y=x} -> {z | true} let f g (x:int) (y:int) = g (x+1) (y+1) contract unzip = {x | true} -> ({a | true} -> {b | b = a} -> {c | true}) -> {z | z = k x x} let rec unzip (x:int) (k:int-> int-> int) = if x=0 then k 0 0 else unzip (x-1) (f k) contract zip = {x | true} -> {y | y = x} -> {z | z = x} let rec zip x y = if x=0 then (if y=0 then 0 else failwith "zip") else (if y=0 then failwith "zip" else 1+zip(x-1)(y-1)) contract t1 = {n | n >=0} -> {z | z=n} let t1 n = unzip n zip