Support for mutual recursion

[sergefdrv]

Does Libretto somehow support mutual recursion? Is it possible, e.g., to define a linear function a in terms of another linear function e, which itself is defined in terms of a?

NB. I don't have any concrete example in mind, but this question just occurred to me while I was exploring Libretto.

[TomasMikula]

It is possible, although it can get hairy quickly.

Here's an example:

def isEven_(
  isOdd: UInt31 -⚬ Bool,
): UInt31 -⚬ Bool =
  λ { n =>
    switch(UInt31.decrement(n))
      .is { case InR(n0)   => isOdd(n0) }
      .is { case InL(done) => done |> Bool.constTrue }
      .end
  }

def isOdd_(
  isEven: UInt31 -⚬ Bool,
): UInt31 -⚬ Bool =
  λ { n =>
    switch(UInt31.decrement(n))
      .is { case InR(n0)   => isEven(n0) }
      .is { case InL(done) => done |> Bool.constFalse }
      .end
  }

val isEven: UInt31 -⚬ Bool =
  rec { self => isEven_(isOdd_(self)) }

val isOdd: UInt31 -⚬ Bool =
  rec { self => isOdd_(isEven_(self)) }

[TomasMikula]

I have just added this example to tests.

[sergefdrv]

Nice, thanks for clarifying!