Semantics of Let Recursion nodes?

[edwardpeters]

I'm unclear on the intended semantics of let recursion nodes, and in particular, what is "Legal".

The example in https://package.elm-lang.org/packages/finos/morphir-elm/latest/Morphir-IR-Value#letRec is:

let
    a =
        b

    b =
        a
in
a

For which I see no clear interpretation. (The web tooling evaluates to a, which makes sense for IR -> IR interpretation, but not if you're expecting an actual data value.)

Checking the elm semantics, this is disallowed in native elm: https://github.com/elm/compiler/blob/master/hints/bad-recursion.md . To paraphrase, elm only allows self-referential cycles - a variable whose RHS refers back to itself through some sequence of bindings - if there is a function invocation in the way. This lets you define self-recursive or mutually recursive functions, but not the problematic example above.

There does exist some grey area between these - some functions have sane evaluation without meeting the "Function indirection" criteria required by elm. For instance

let
  x = if false x else 1
in
 x

Can be reasonable evaluated as 1.

Despite this grey area, I think that - unless I'm missing something - we should go with the elm rule, update the documentation to mention such and specify an example that uses elm-legal recursive functions, and (maybe, time allowing) add a compiler check to reject "Bad recursion" by the elm definition.

Can someone familiar with the definition of the IR and the decisions made there confirm if this is the case, or specify what the intended semantics are?

[AttilaMihaly]

Considering this "Bad recursion" makes sense and we should document it and also have a way to verify. I created this issue to track: finos/morphir-elm#1113