Can local FuncDefn's capture values from outside?

[acl-cqc]

Are local FuncDefn's "just" for scoping/namespacing? Or, are they closures?

I think the spec allows them to capture values (via non-local Ext or even Dom edges entering the local FuncDefn from the outside), in that it does nothing to exclude such edges. However, this may be an accident (i.e. we just didn't think of it when we allowed Scoped Definitions)...?

Current implementation of local FuncDefns is that they may not use the enclosing function's type parameters (the compiler should add/repeat any that are required as extra TypeParams to the local FuncDefn, and pass them in as extra TypeArgs at each use) - anything else raised many extra/subtle difficulties. The spec is somewhat out of date here (i.e. the spec is not up-to-date wrt. #285).

Putting these two together gives the situation where an Ext edge could enter a local FuncDefn, where the type of the Ext edge refers to a TypeParam defined in the outer (Source) scope but where the target has no type for what's on the edge. This is clearly nonsense and has to be prevented, somehow.

We could rule out such edges (a bit of a special case for Dom/Ext); require they do not use the outer function's TypeParams (a strange restriction!); make some complex requirement about type variables used in the type of such edge (e.g. the inner function must repeat the outer function's TypeParams before adding its own, so preserving same-index-for-"same"-TypeParam); etc. etc. - there are options here. (But, they all add complexity, somewhere/somehow!)

[acl-cqc]

@mark-koch if we do allow local FuncDefns to capture, does that simplify Guppy's handling? That is, I recall Guppy has to do some insertion-of-extra-parameters for nested functions, but would this shift that burden out of Guppy and onto Hugr ?

[mark-koch]

Exactly. At the moment, Guppy turns captured values into extra arguments that are supplied via a Tierkreis partial application node. Allowing non-local edges into FuncDefns would make this redundant.

However, if we make exceptions (e.g. no parametric values on non-local edges), then Guppy would need to handle those cases separately, which probably ends up being more work

[doug-q]

I think that with type args in the picture, the only sensible thing to do is forbid closures (i.e. non-local edges into FuncDefns). I question the need for scoped definitions at all.

[acl-cqc]

#1061 said they can't, closing.