Relations, Functions and Automata

The usual named functions can be defined in a style of logical relations:

sqrdist(x: num, y: num): num = x*x + y*y
sqrdist(x: num)(y:num): num = x*x + y*y
sqrdist
    : num -> num -> num
    = fn x y => x*x + y*y

apply42{t: Type}(f: num -> t): t = f 42

Lambdas are values:

fn x => x + 1
fn(x: num): num => x + 1

Priority of => is above = and below :