lambda-buffers icon indicating copy to clipboard operation
lambda-buffers copied to clipboard

Plutarch codegen: Recursive data type support

Open bladyjoker opened this issue 1 year ago • 0 comments

One does not simply recurse in Plutarch.

My raw lambda calculus skills are not at the level where I'm just popping out fixpoint based terms so let's get back to the drawing board:

For a canonical recursive data type example and some mutually recursive ones:

sum List a = Cons a (List a) | Nil
sum F a = Rec (G a) | Nil
sum G a = Rec (F a) | Nil

What we do eventually is invoke some polymorphic class method on the constituents of each constructor (if it's a sum type, but also for products and records). This is where the problem happens right? How would we use pfix in this situation?

(let's imagine we have an annotation that tells us whether a type is infinite or not).

pfix :: Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))

fib :: Term s (PInteger :--> PInteger)
fib = phoistAcyclic $
  pfix #$ plam $ \self n ->
    pif
      (n #== 0)
      0
      $ pif
        (n #== 1)
        1
        $ self # (n - 1) + self # (n - 2)

Main question is: How do we generate code in a uniform manner such that we can recurse properly?

bladyjoker avatar Nov 06 '23 20:11 bladyjoker