Arbitrary acceptance of labelled arguments

Learning
1

Why does the following code compile?

let f = function
  | Some x -> x
  | None -> failwith "is none"
  
let x = f ~why_does_this_work:()

I would expect the compiler to tell me that f does not take a labelled argument why_does_this_work, but instead the type of x is

val x : (why_does_this_work:unit -> 'a) option -> 'a = <fun>

It looks like there’s some implicit function being created here, but I’ve never seen this behavior before.

2 Likes
2

It’s cool! You are passing ~why_does_this_work:() to x, which you unpacked from the option. You guarantee that the option is non-empty by having failwith in the None branch.

1 Like
3

My brain is still twisted. Can someone explain how f ~why_does_this_work:() is desugared?

It seems that the argument ~why_does_this_work:() is interpreted as Some g where g has type (why_does_this_work:unit -> 'a) option -> 'a. I can’t see by what rule it arrives at that?

The closest I got was:

let g = 
function 
  | None -> failwith "" 
  | Some (x:(why_does_this_work:unit -> 'a)) -> ((failwith ""):'a)
 in
f (Some g)

which can’t do anything and is of type

(why_does_this_work:unit -> '_a) option -> '_a = <fun>
4

This is not desugaring. But it would compute the equivalent result.
f ~why_does_this_work:() →
from definition of f:
(function Some x -> x | None -> failwith "is none") ~why_does_this_work:() →
equivalent syntax that will be more convenient later:
(fun z -> match z with Some x -> x | None -> failwith "is none") ~why_does_this_work:() →
eta expansion:
(fun z ~why_does_this_work -> match z with Some x -> x ~why_does_this_work | None -> failwith "is none" ~why_does_this_work) ~why_does_this_work:() →
beta reduction:
fun z -> match z with Some x -> x ~why_does_this_work:() | None -> failwith "is none" ~why_does_this_work:() →
equivalent syntax:
function Some x -> x ~why_does_this_work:() | None -> failwith "is none" ~why_does_this_work:()

3 Likes
5

I guess what is surprising here is that the same example doesn’t work with a non-labelled argument, e.g.

# f ~why_does_this_work:();;
> (why_does_this_work:unit -> 'a) option -> 'a = <fun>

# f ();;
Error: This variant expression is expected to have type 'a option
       There is no constructor () within type option

I didn’t fully realize labelled argument compilation did so much work under the hood.

edit: from a typing perspective, the compiler unifies why_does_this_work:unit -> 'b with 'a option -> 'a. The most general solution is to unify 'a with why_does_this_work:unit -> 'b, which after application of the labelled argument yields the result type.

1 Like
6

This always confuses me too.
I think the rules are in this paper but I don’t really understand it. I remember reading a more understandable explanation of how this worked, but I can’t find it again…

(Then I had the same unification explanation that @igarnier gives)

I think that this is confusing when it happens involuntarily, and I’m not sure in which case it is useful, but I don’t know if it would be possible to have a warning for this, since it does make sense…

Edit: To give an example where this can be misleading, you can mistype a label and get some weird type error down the line.

# let f ~longlabel1 = function | Some x -> longlabel1 x | None -> failwith "is none";;
# f ~longlabel1:((+) 1) (Some 2);;
- : int = 3
# f ~longlabel2:((+) 1) (Some 2);;
- : longlabel1:(int -> longlabel2:(int -> int) -> '_weak1) -> '_weak1 = <fun>
7

This is because the labeled argument can be applied out-of-order. The eta-expansion in my explanation introduces the labeled parameter on the function side so that the labeled argument can be applied even though the non-labeled argument is still missing.

1 Like
8

To rephrase @lukstafi explanation without the inlinling, if we start with an explicit argument x:

let g x = f ~why:() x

it is easier to see that the types align if we commute the label and the non-labelled argument:

let g x = f x ~why:()

Then, if we remove the redundant x in the first version

let g x = f ~why:() x

we get back the original example:

let g = f ~why:()
3 Likes