RFC: Allow structural recursion without triggering edge cycle limiting

[Keno]

This attempts to fix inference for the case in #29293 (the one
returning Any). It does not fix the cache poisoning part of that
issue, which is a separate concern. The idea here is that we avoid
applying limiting if the argtypes of the frame become strictly simpler
(thus guaranteeing eventual termination). It is important that the
complexity relation be transitive and anti-reflexive.

[jrevels]

argtypes_strictly_less_comples --> argtypes_strictly_less_complex?

[StefanKarpinski]

No, it's the second-person singular present active indicative of the Latin "compleō".

[vtjnash]

This isn't the right way to handle this. But it does seem to be an interesting idea: the conceptual idea here appears that it should give a proof that tail-recursion is convergent, thus permitting a whole new class of problems to be inferred! There's just some remaining effort to be done to demonstrate the expected convergence rates and fix the implementation.

[vtjnash]

0 isn't an overapproximation

[Keno]

Heh, you caught that, did you ;). You're right of course. That was just a quick way to fix the case I was interested in. -1 is the correct approximate fallback.

[vtjnash]

get_argtypes is very slow, and thus is not permitted to be used. It's also only an approximation, so again, not permitted to be used.

[jrevels]

IIUC the result of actually computing get_argtypes should already be cached here, yeah? I don't think we ever construct an InferenceResult instance without immediately computing the argtypes. So it should basically just be a field access by this point.

I did some refactoring in #28955 to make things like this less confusing - after that gets merged, get_argtypes(parent.result) here would just be parent.result.argtypes.

[Keno]

the conceptual idea here appears that it should give a proof that tail-recursion is convergent, thus permitting a whole new class of problems to be inferred!

Correct, basically the simple version of this: http://adam.chlipala.net/cpdt/html/GeneralRec.html (for one particular fixed relation, but for the same reasons).

[Keno]

For my own future reference, a simple testcase that requires this:

Base.Broadcast._bcs($((Base.OneTo(2), Base.OneTo(14), Base.OneTo(512), Base.OneTo(1))), $((Base.OneTo(2), Base.OneTo(1), Base.OneTo(512), Base.OneTo(1))))

[vtjnash]

That result is only different because this PR is incorrect. That particular pattern just runs into intentional heuristics that decide when we should stop running constant-propagation (for inference performance, we disable all constant-propagation when we encounter recursion).

[Keno]

Well, I would like it not do that, because I need that function to infer ;)

[Keno]

Also, this was with aggressive const prop enabled, so that may or may not have made a difference. In general, I'd like an inference mode that infers as much as possible as long as termination is guaranteed. If that needs to be a flag, that'd be ok with me.

[Keno]

I wonder if what we need to do is assign each type a complexity score (e.g. recursively sum up the number of parameters leaves) and then simply assert that the total complexity score of the signature must decrease. That would capture various shifting around of complexity between arguments.

[StefanKarpinski]

That seems like a pretty solid approach. I guess the trick is designing the complexity score.

[StefanKarpinski]

Maybe something like this:

Non-parametric types: 1
Parametric types: 1 + sum of parameters
Tuples: 1 + sum of tuple elements
Unions: 1 + sum of union elements

Not sure about the 1 + parts, maybe should just be a bare sum.

[vtjnash]

Yes, I think we call that size and/or depth. I wrote a couple of blog posts about it.

[Keno]

Sure, but I'm saying combine them into one number for the whole signature

[StefanKarpinski]

It's basically the number of nodes in the "signature tree": top-level nodes are the call arguments, parametric types, tuples and unions are internal nodes, and non-parametric types are leaves.

[Keno]

non-parametric types and non-types, but yes

[Keno]

Ideally, we'd also cache this value in type object, so we don't have to recursively walk it every time.

[vtjnash]

Alright, great. We could even call it size and/or depth:

julia/src/jltypes.c

Lines 1017 to 1036 in b89e88e

	static size_t jl_type_depth(jl_value_t *dt)
	{
	if (jl_is_uniontype(dt)) {
	size_t ad = jl_type_depth(((jl_uniontype_t*)dt)->a);
	size_t bd = jl_type_depth(((jl_uniontype_t*)dt)->b);
	return ad > bd ? ad : bd;
	}
	else if (jl_is_unionall(dt)) {
	jl_unionall_t *ua = (jl_unionall_t*)dt;
	size_t bd = jl_type_depth(ua->body);
	if (ua->var->ub == (jl_value_t*)jl_any_type)
	return bd;
	size_t vd = jl_type_depth(ua->var->ub);
	return vd+1 > bd ? vd+1 : bd;
	}
	else if (jl_is_datatype(dt)) {
	return ((jl_datatype_t*)dt)->depth;
	}
	return 0;
	}

[Keno]

Yes, but that's not quite the correct notion yet. We can probably extend it.

[StefanKarpinski]

The term "depth" for a tree has a well-established meaning—and this is not it. The "size" of a tree is closer to the correct term, but calling this the "size" of a type would be extremely confusing, so please don't use either of those terms for this. Calling this the "tree size" of a type would be ok.

[StefanKarpinski]

The depth of a type's tree also does not have the right property at all: if you take a bunch of types with depth d1, ..., dn and you combine them into a single argument as type parameters or types of the slots in a tuple, then the depth is max(d1, ..., dn) + 1. We want a measure that has the property that it is additive in this case.

[Keno]

We want a measure that has the property that it is additive in this case.

Correct.

[StefanKarpinski]

Unclear to me if we want it to be super-additive or exactly additive. Super-additive would make it legal to take a structure apart but not construct a structure from individual pieces whereas exactly additive would make both legal. It seems like what one wants is some leeway to take k steps at the same level of complexity, so you probably want a counter that resets to k every time the total argument complexity drops and which counts down every time it stays the same or grows, bailing out when the counter reaches zero. Exactly additive seems most permissive, allowing arbitrary juggling.

[StefanKarpinski]

Alternatively, count total argument complexity at the start and bail out if it ever gets larger than a fixed amount above that OR if it takes more than some upper limit on the number of steps.

[chethega]

The term "depth" for a tree has a well-established meaning—and this is not it. The "size" of a tree is closer to the correct term, but calling this the "size" of a type would be extremely confusing, so please don't use either of those terms for this. Calling this the "tree size" of a type would be ok.

Weight sounds nicely additive.

Unclear to me if we want it to be super-additive or exactly additive.

Pure sum of tuple elements makes () and ((),), (((),),) etc have all the same weight, right? That feels wrong and probably allows Turing-completeness within the same weight.

What about: store lowest weight seen so far, and how many steps back this was. When we get something lighter, update lowest_seen and last_seen counter. Bail if we ever see something that is C_gain heavier than lowest_seen or if last_seen is more than N_speed steps ago. In other words, permit juggling that temporarily makes things moderately worse.

Maybe count positive integers with val, and with 1 otherwise; this nicely generalizes NTuples, makes Vector lighter/simpler than Matrix and, very importantly, makes Val{1} et al lighter than Val{2}.

[StefanKarpinski]

Pure sum of tuple elements makes () and ((),), (((),),) etc have all the same weight, right? That feels wrong and probably allows Turing-completeness within the same weight.

Good point: tuples need to have weight one more than their parts. Probably similar for others.