Skip to content

Plutarch codegen: Recursive data type support #131

Open
@bladyjoker

Description

@bladyjoker

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?

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    Status

    Todo

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions