Add recursion and mutual recursion

[LighghtEeloo]

Syntax

rec f: <TValue> = <Value>,
    g: <TValue> = <Value>;
<Computation>

Currently we don't support mutual recursion, but it's very easy to add and the syntax is ready.

Type checking

Add the name with it's type to the ctx ahead of time, and check that the actual type meets.

Q: Do we need value or computation for the body of the rec?

Evaluation

Bind the value to the environment before evaluating it.

Q: Do we need to enforce the body to be a thunk?

Implementation

Draft done by @ricky136973

[LighghtEeloo]

When we are testing we find that a dead loop in user code will result in a stack overflow in our evaluation, which is hard to just unwind. We decide not to include them in our major test for now.

Tried multithread to prevent killing by the OS but didn't work.

Is there any way to catch a stack overflow? Can we sort of try to trap the signal or something (?_?)

Or maybe we can just put the evaluator on the heap instead...

Or maybe we can just ignore them...

[maxsnew]

We shouldn't allow arbitrary value recursion. For instance if we had lists in the language, this would allow us to make cyclic lists:

rec cycle : List Num = cons(5, cycle)

which we do not want to allow, at least for the normal definition of List as a datatype.

The simplest thing to do would be to say that you can only do a rec where the right hand side is a thunk.

Do you have an example of the problem with loops?

To define an evaluator that doesn't blow Rust's stack, yes, you need to store the object language's stack on the heap. Basically you need to write it in the style of Levy's stack-based abstract machine semantics. For example, see what I did for the evaluator in compiler's class: https://gitlab.com/eecs-483/starter-code/diamondback/-/blob/master/src/interp.rs#L234 .

[LighghtEeloo]

Recursion has been changed (and re-implemented) in zydeco. Now it has syntax rec (f: U(B)) -> b and itself has type B (basically fix in eecs-490). Also we have a syntactic sugar let rec f: B = b1; b2 which transforms to function flavor.

An add example:

data Nat where | Z() | S(Nat)
let add = {
  rec (add: Comp(Nat -> Nat -> Ret(Nat))) -> (
    fn (x: Nat, y: Nat) -> (
      match x
      | Z -> ret y
      | S(x) -> !add x S(y)
    )
  )
};
!add S(S(Z())) S(Z())

[maxsnew]

This seems complete then?

[LighghtEeloo]

Yeah I think so. @ricky136973 What do you think?

[ricky136973]

LGTM. Actually, it looks pretty much like a "scoped and typed goto". Just to make it safe, is there any good examples to see if our implementation also works well on mutual recursions?

[LighghtEeloo]

I agree that we should push on mutual recursions since it's more convenient and our define declarations would use them.

[maxsnew]

I'm going to consider this done for milestone purposes. I don't think mutual recursion is that important since it can be implemented using single-function recursion by a very simple local transformation.

[LighghtEeloo]

Shall we close the issue if we are satisfied with single-function recursion at the moment?