What is the proper way to type lambdas in Why3ML?

Question

I want to verify a function with a lambda. For instance:

  let map (t : array int) (f : array int -> array int) : array int =
    f t

However, this yields an error:

File "map_reduce.mlw", line 25, characters 4-7: This application instantiates pure type variable 'b with a mutable type array int

Is it possible to use lambda functions in Why3? What is the proper way to type these lambda functions?

Answer 1

Lambda functions in Why3 are pure functions. In particular, their type cannot contain any mutable region. That is why your definition is rejected. Replacing array with a type without region, e.g., set, works fine:

use set.Set
let map (t : set int) (f : set int -> set int) : set int = f t