Re: [Caml-list] Calling a single function on every member of a GADT?

[Malcolm Matalka <mmatalka@gmail.com>]

Thank you for the explanation Ivan.  I have two questions inline.

Ivan Gotovchits <ivg@ieee.org> writes:

> It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1
> polymorphism enabled for functions, we could apply it to the function
>
>      let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) ->
> f x, f y

Small thing, but wouldn't the faux type be the following, based on your
usage (making sure I'm following):

fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c

> as
>
>    let x,y : string * int = map2 (bad_id ()) "hello", 42
>
> and will get a segmentation fault, as `y` will now have type int but hold a
> string.
>
> And here comes the syntax as a savior as it lets us specify functions that
> are guaranteed to be syntactic values. Indeed, all three solutions
> syntactically guarantee that the provided argument is a function, not a
> closure. Indeed, let's introduce the universal identity via a record,
>
>    type id = { f : 'a. 'a -> 'a}
>
> and we can see that our `bad_id` is not accepted due to the value
> restriction, while good_id, defined as,
>
>    let good_id x = x
>
> is perfectly fine, e.g.,
>
>   let id1 = {f = good_id} (*accepted *)
>   let id2 = {f = bad_id}   (* rejected *)
>
> moreover, even a fine, but not syntactic, identity is also rejected
>
>   let fine_id () x = x
>   let id3 = {f = fine_id ()} (* rejected *)
>
> with the message
>
>   This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a
>

Why is type checking creating a record different than type checking a
function argument?

If we had the syntax (or something like it):

let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c)

Why would the type checker not be able to see that

map2 good_id ("hi", 42)

is valid but

map2 (fine_id ()) ("hi", 32)

is not, using the same logic that is verifying creating the "id" record
is not valid?