Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Plutarch codegen: Recursive data type support #131

Open
bladyjoker opened this issue Nov 6, 2023 · 0 comments
Open

Plutarch codegen: Recursive data type support #131

bladyjoker opened this issue Nov 6, 2023 · 0 comments
Labels
codegen plutarch All things Plutarch

Comments

@bladyjoker
Copy link
Contributor

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
codegen plutarch All things Plutarch
Projects
Status: Todo
Development

No branches or pull requests

1 participant