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?
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:
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).
Main question is: How do we generate code in a uniform manner such that we can recurse properly?