Question about Parameter Syntax and Function Types

[Arthri]

Do these three declarations define the same thing?

let f (x:int) (y:int) : int = x + y
let g (x y: int) : int = x + y
let h : x:int -> y:int -> int = fun x -> fun y -> x + y

[mtzguido]

Hi Arthri, they do.

F* functions always unary (take a single argument) and may possibly return another function, like in most functional languages. All three examples define a "two argument" function (i.e. a function returning a function). The second case is just syntactic sugar for the first case, this syntax only helps avoid repeating the int type.

In the third case, instead of placing the binders of the left of the equal sign, h is defined directly as a lambda term. But the first and second declaration should also desugar to the same thing.

Internally, there is actually a very tiny difference between f/g and h. In the first two the body has an extra int ascription, but this should not matter at all. A way to look at this is running:

$ ./bin/fstar.exe A.fst --dump_module A
Module after type checking:
module A
Declarations: [
let f x y = x + y <: Prims.int
let g x y = x + y <: Prims.int
let h x y = x + y
]

Verified module: A
All verification conditions discharged successfully

[Arthri]

Thank you for the clarification! It took me a while to figure the second one out