func.bind has a dynamic number of stack arguments?

[fgmccabe]

The way that the func.bind instruction is specified, the literal type operand specifies the result type of the bind:

func.bind $t' : [t1^n (ref $t)] -> [(ref $t')]

That seems to suggest that the implementation has to look at the actual function, decide how many extra arguments to bind by diffing the actual function type (which is on the argument stack) and the target function type.

This could be resolved by either limiting bind to one free variable or by adding an additional operand.

Or am I reading this incorrectly?

[rossberg]

Yes, the t1^n are the params in the diff, see the side condition to the rule. The n is simply the difference in arity, which is trivial to compute.

An additional type annotation for the source type (or the bound param types) wouldn't help, since the validator would still need to compute the diff (and check that the non-diff part is compatible). It would only add more checking work.

Only having single-parameter bind would be too limiting.

[fgmccabe]

Yes, but, as noted, the way it is specified, you have to do the check on the actual function supplied. That makes it dynamic in an unfortunate way.

[rossberg]

@fgmccabe, ??? The type of the source function is statically known regardless.

[rossberg]

Func.bind has been dropped from the proposal.