Inference.lpts

> language f;
From B. C. Pierce and D. N. Turner, Local Type Inference, POPL 1998:
"Bidirectional propagation of type information allows the types of parameters of
anonymous functions to be inferred. When an anonymous function appears as an
argument to another function, the expected domain type is used as the expected
type for the anonymous abstraction, allowing the type annotations on its
parameters to be omitted."

> assert (lambda f : Int -> Int . f 1) (lambda x : _ . add 1 x) = 2;

> assert (lambda f : Int -> Int -> Int . f 2 3) (lambda (x : _) (y : _) . add x y) = 5;

This should be the same type for both x and y. But I am not so sure this is
actually guaranteed since there is no unification.
> assert (lambda f : Int -> Int -> Int . f 2 3) (lambda (x y : _) . add x y) = 5;

There is syntactic sugar:
> assert (lambda f : Int -> Int . f 1) (lambda x . add 1 x) = 2;

> assert (lambda f : Int -> Int -> Int . f 2 3) (lambda x y . add x y) = 5;

> double (X : *) (f : X -> X) (x : X) = f (f x);

> add1Twice = double Int (lambda x : _ . add 1 x);

Since the second half of the Pierce paper is not currently implemented, this will not work:

  add1Twice2 = double _ (lambda x : Int . add 1 x);


This:
> foo : Int -> Int
>  = lambda x : _ . x;
should be the same as this:
> foo2 : Int -> Int
>  = lambda x : Int . x;
> assert foo = foo2;