`func.bind` and iso-recursion

[titzer]

I am having trouble wrapping my head around the intended type rules for func.bind. Currently, func.bind includes a type annotation (call this $ft) that should reference a signature type. The result of the instruction should be ref $ft. The top of the stack should contain a function reference (let's suppose its type is ref null $et). The difference in parameter arity between $et and $ft is the number of arguments that will be bound by this instruction (call this diff).

I am trying to understand how to relate the "residual" type ($et - diff) to $ft.

Suppose diff != 0

Issues come to mind:

• the residual type is not part of a recursion group, so I am not sure how to canonicalize it
• it doesn't have an explicit supertype chain--should it have a supertype chain of similar residual types?

[rossberg]

func.bind is no longer included in this proposal (now in Post-MVP), but roughly, you'd take the difference after unrolling both types.

If we opt for explicit type annotations, then func.bind would actually have 2 annotations and a typing rule as follows:

func.bind $t $t' : [t0* (ref null $t)] -> [(ref $t')]`
    - iff `unroll($t) = func [t0* t1*] -> [t2*]`
    - and `unroll($t') = func [t1'*] -> [t2'*]`
    - and `t1'* <: t1*`
    - and `t2* <: t2'*`

I just updated the rule in Post-MVP.md to mirror this.

Without full type annotations, $t would be inferred from the operand.

[rossberg]

Closing as answered. Feel free to reopen if there are further questions.