optimize recursion on existential types

[johnynek]

Since we don't have existential types, we encode them with a callback approach, for instance (from #1046 )

enum Eval[a]:
    Pure(a: a)
    FlatMap(use: forall x. (forall y. (Eval[y], y -> Eval[a]) -> x) -> x)

def done(a: a) -> Eval[a]: Pure(a)

def flat_map[a, b](e: Eval[a], fn: a -> Eval[b]) -> Eval[b]:
    FlatMap(cb -> cb(e, fn))

All the use function ever does is directly call on two arguments closed over. So later when it is used:

              case RunEval(FlatMap(use), stack):
                  use((prev, fn) -> run(balance, RunEval(prev, push_stack(fn, stack)))) 

here note all we do is call use((prev, fn) -> ...) but we know that use is just going to pass two argument in:

#for some type t
prev: Eval[t] = ...
fn: t -> Eval[a] = ...
run(balance, RunEval(prev, push_stack(fn, stack)))

if the code were written that way, it would be tail recursive, but inside the use function it isn't.

It seems like we should be able to see that the only instance of FlatMap is created by a function that just passes two values in (which would be common for such existential recursion examples). So, it would be nice to be able to rewrite the TypedExpr to remove the nesting inside use).

It isn't obvious though. Maybe if we had existential types after type checking, at the TypedExpr layer, we could rewrite functions like use((prev, fn) -> ... to (prev, fn): exists t. (Eval[t], t -> Eval[a]) = use((prev, fn) -> (prev, fn)) then see that we can eliminate the exists t. from what comes next in a way that prevents t from escaping.

[johnynek]

One way we could solve this could be if we see that:

1. the type constructor is not exported
2. the only construction of the type constructor is a lambda that applies.

Then we could possibly rewrite at the Matchless layer since we know that the type is really holding a let binding that is going to be used. Possibly we could also have existential types at the TypedExpr layer but only after type-checking, so then we could normalize this kind of code into a binding for an existential type.

It could be possible to be more general here and if we can see that constructors are only created in one way, we could leverage that information to inline better.

[johnynek]

related to #651

[johnynek]

Another idea would be to basically dynamically check patterns that look like this to see if they are "apply lambdas". So, an apply lambda (or perhaps "forwarder") is something like: f -> f(a, b, ...) So, if we are going to call someLambda(f) we could instead dynamically rewrite into: let (a, b, ...) = ... in f(a, b, ...) which could be a tail call.

But I guess that gets pretty deep into jit territory, since for it to be useful as a tail call you also have to have two implementations of the function, one with a loop and the tail call, and with a direct recursion which may consume stack.

I guess optimizing the case where we know statically that there is a single constructor for an enum is maybe the more tractable approach.

[johnynek]

see this discussion of rules for equivalence in existential and universally quantified propositions:

https://www.csd.uwo.ca/~lkari/prenex.pdf

[johnynek]

closed by #1066