import set
Common functional programming languages such as Haskell use recursion schemes to generalize folding/unfolding patterns. This typically requires infinitely recursive types and some notion of functor instancing. Today I want to showcase an effectful implementation of recursion schemes that instead makes use of refunctionalizing data structures to effects and handlers.
In fact, this post is much more about showcasing effects and handlers than it is about recursion schemes themselves:
This is an interactive blog, you are encouraged to experiment with the code!
Let’s start by constructing some basic lambda terms as the running example data structure.
type Term {
Sym(name: String)
Lam(name: String, body: Term)
App(function: Term, argument: Term)
}
For example, the identity function λx.x is encoded as the following
term:
Lam("x", Sym("x")).show
In Effekt, we can traverse these terms by matching and recursively
calling the traversing function. For example, in order to use a custom
show implementation instead of the default one:
def pretty(t: Term): String = t match {
case Sym(x) => x.show
case Lam(x, b) => s"λ${x}.${b.pretty}"
case App(f, a) => s"(${f.pretty} ${a.pretty})"
}
App(Lam("x", Lam("y", Sym("x"))), Lam("x", Sym("x"))).pretty
In fact, this would be a great use for a fold function on terms. The
catamorphism recursion scheme generalizes folds. Instead of calling
pretty on a b: Term, the body that’s matched upon is already the
result of the recursive call, i.e. b: String. Optimally, the
catamorphic version of pretty would look something like the following:
def pretty?(t: Term): String = <{"something with cata"}> {
case Sym(x) => x.show
case Lam(x, b) => s"λ${x}.${b}"
case App(f, a) => s"(${f} ${a})"
}
Catamorphism
Traditionally, you would then have a separate, parametrized TermF,
where all recursive occurrences of Term are replaced by a type
variable. The previous type Term then becomes
TermF (TermF (TermF ...)), i.e. it has an infinitely recursive type.
Effekt does not support infinite types though!
What Effekt does support, however, is effects and handlers. You can
learn more about Effekt’s use of effects in our tour.
The refunctionalized variant of Term is then defined by the following
interface:
interface TermF[T, R] {
def sym(name: String): R
def lam(name: String, body: T): R
def app(function: T, argument: T): R
}
For example, a call to sym could be handled like the following: (note
how it now requires the do-prefix, as it is an effect)
try do sym("x") with TermF[String, String] {
def sym(x) = s"got ${x}!"
def lam(x, b) = <{"not implemented"}>
def app(f, a) = <{"not implemented"}>
}
Trick question: Try replacing do sym("x") with
do lam("x", do sym("x")). Why does this not give a "not implemented"
error?
Answer: Once do sym("x") is handled, the entire term
do lam("x", do sym("x")) has become "got x!". In order to provide
the string as a return value to the call do sym("x"), one must give
back the desired value via resume.
try do lam("x", do sym("x")) with TermF[String, String] {
def sym(x) = resume(x)
def lam(x, b) = resume(s"λ${x}.${b}")
def app(f, a) = resume(s"(${f} ${a})")
}
An effectful implementation of a catamorphism is merely a generalization
of this Term → TermF[A] pattern. cata has TermF[A] in the effect
signature, as these effects must be handled by a calling context:
def cata[A](t: Term): A / TermF[A, A] = t match {
case Sym(x) => do sym(x)
case Lam(x, b) => do lam(x, b.cata)
case App(f, a) => do app(f.cata, a.cata)
}
We can rewrite the pretty function from before as a catamorphism:
def pretty!(t: Term) = try t.cata with TermF[String, String] {
def sym(x) = resume(x)
def lam(x, b) = resume(s"λ${x}.${b}")
def app(f, a) = resume(s"(${f} ${a})")
}
App(Lam("x", Lam("y", Sym("x"))), Lam("x", Sym("x"))).pretty!
Similarly, we can use cata to count the constructors of a lambda term
– without explicit recursion!
def size(t: Term) = try t.cata with TermF[Int, Int] {
def sym(x) = resume(1)
def lam(_, b) = resume(1 + b)
def app(f, a) = resume(1 + f + a)
}
App(Lam("x", Lam("y", Sym("x"))), Lam("x", Sym("x"))).size
Or return all free variables in a term:
def free(t: Term) = try t.cata with TermF[Set[String], Set[String]] {
def sym(x) = resume(x.singletonGeneric)
def lam(x, b) = resume(b.difference(x.singletonGeneric))
def app(f, a) = resume(f.union(a))
}.toList
def freeIn(x: String, t: Term) = t.free.contains(x) { (a, b) => a == b }
App(Lam("x", Lam("y", Sym("x"))), Lam("x", Sym("z"))).free
Paramorphism
Compared to cata, para also passes the original data structure to
the handler. This can be implemented by extending cata to pass a tuple
to the handler with the original term:
def para[A](t: Term): A / TermF[(Term, A), A] = t match {
case Sym(x) => do sym(x)
case Lam(x, b) => do lam(x, (b, b.para))
case App(f, a) => do app((f, f.para), (a, a.para))
}
In substitutions t[x/r], for example, this can be used to prevent
recursion into the term t that is being substituted, if it also binds
the variable s:
def substitute(t: Term, x: String, r: Term) = try t.para with TermF[(Term, Term), Term] {
def sym(y) = resume(if (x == y) r else Sym(y))
def lam(y, b) = resume(
if (x == y) Lam(y, b.first) // shadowing!
else if (y.freeIn(r)) <> // alpha-renaming (omitted)
else Lam(y, b.second))
def app(f, a) = resume(App(f.second, a.second))
}
App(Lam("x", Lam("y", Sym("x"))), Lam("x", Sym("z"))).substitute("z", Sym("foo"))
Anamorphism
Anamorphisms are all about unfolding structures from a single seed. They are dual to catamorphisms, which fold structures into a single value.
Consider the following program that emits every natural number using the
emit effect from the standard library.
def nats(s: Int): Unit / emit[Int] = { do emit(s); nats(s + 1) }
list::collect[Int] { limit[Int](10) { nats(0) } }
Here, the seed of the unfold is s, where the recursive calls provide
the seed for the next iteration. The emitted values of the unfolding are
then collected using the collect function.
We can generalize this to an ana function for list construction, using
a cons effect to provide the next seed directly in its second field:
effect cons[S, R](hd: R, tl: S): List[R]
def ana[S, R](s: S) { coalg: S => List[R] / { cons[S, R], stop } }: List[R] = try coalg(s)
with cons[S, R] { (hd, tl) => resume(Cons(hd, tl.ana{coalg})) }
with stop { Nil[R]() }
This definition also allows for the stop effect in order to forcefully
stop the unfolding. For example, to print the fibonacci series until
n:
def fib(n: Int) = ana[(Int, Int, Int), Int]((0, 0, 1)) { case (i, a, b) =>
if (i == n) do stop()
else do cons(a, (i + 1, b, a + b))
}
fib(10)
For lambda terms, we may now construct a very similar function. Here,
the parametrization over R is not required, as Termss can only
contain Terms:
def ana[S](s: S) { coalg: S => Term / TermF[S, Term] }: Term = try coalg(s) with TermF[S, Term] {
def sym(x) = resume(Sym(x))
def lam(x, b) = resume(Lam(x, b.ana{coalg}))
def app(f, a) = resume(App(f.ana{coalg}, a.ana{coalg}))
}
If you compare this definition to cata from above, you may note how it
is indeed perfectly dual – instead of executing effects, we now handle
effects!
We can use this for all kinds of seeds. For example, say we want to
convert lambda terms that use de Bruijn
indices (DTerm) to the
previous Term. Then, starting from an empty environment and the de
Bruijn indexed term (the seed), we can increasingly fill the environment
while the DTerm gets smaller and the Term emerges from the effectful
construction:
type DTerm {
DIdx(index: Int)
DLam(body: DTerm)
DApp(function: DTerm, argument: DTerm)
}
effect fresh(): String
def freshener[R] { prog: => R / fresh } = {
var x = 0
try prog() with fresh {
x = x + 1
resume(s"x${x.show}")
}
}
def fromDeBruijn(t: DTerm) =
with on[OutOfBounds].panic()
with freshener
ana((t, Nil[String]())) {
case (DIdx(i), env) => do sym(env.get(i))
case (DLam(b), env) => val x = do fresh(); do lam(x, (b, Cons(x, env)))
case (DApp(f, a), env) => do app((f, env), (a, env))
}
fromDeBruijn(DApp(DLam(DLam(DIdx(1))), DLam(DIdx(0)))).pretty
Hylomorphism
The hylomorphism combines the catamorphism and anamorphism. As in the anamorphism, we start from a seed that starts to unfold. Then, as in the catamorphism, the unfolded structure gets folded back into a value. To remind you, we have defined them both as the following: (are you seeing the symmetry?)
def cata[A](t: Term): A / TermF[A, A] = t match {
case Sym(x) => do sym(x)
case Lam(x, b) => do lam(x, b.cata)
case App(f, a) => do app(f.cata, a.cata)
}
def ana[S](s: S) { coalg: S => Term / TermF[S, Term] }: Term = try coalg(s) with TermF[S, Term] {
def sym(x) = resume(Sym(x))
def lam(x, b) = resume(Lam(x, b.ana{coalg}))
def app(f, a) = resume(App(f.ana{coalg}, a.ana{coalg}))
}
Combining the two definitions yields a naive hylo:
def hyloNaive[S, A](s: S) { coalg: S => Term / TermF[S, Term] }: A / TermF[A, A] =
s.ana{coalg}.cata
We could already now do the following, combining pretty! and
fromDeBruijn into one self-contained call to hyloNaive:
val t = DApp(DLam(DLam(DIdx(1))), DLam(DIdx(0)))
with on[OutOfBounds].panic()
with freshener
try hyloNaive[(DTerm, List[String]), String]((t, Nil[String]())) {
case (DIdx(i), env) => do sym(env.get(i))
case (DLam(b), env) => val x = do fresh(); do lam(x, (b, Cons(x, env)))
case (DApp(f, a), env) => do app((f, env), (a, env))
} with TermF[String, String] {
def sym(x) = resume(x)
def lam(x, b) = resume(s"λ${x}.${b}")
def app(f, a) = resume(s"(${f} ${a})")
}
The problem with hyloNaive is that it first constructs the terms
recursively only to directly deconstruct them again. Instead, hylo can
also be written in such a way that no additional Terms are
constructed. Here is a version that fuses cata and ana:
def hylo[S, A](s: S) { coalg: S => A / TermF[S, A] }: A / TermF[A, A] =
try coalg(s) with TermF[S, A] {
def sym(x) = resume(do sym(x))
def lam(x, b) = resume(do lam(x, b.hylo{coalg}))
def app(f, a) = resume(do app(f.hylo{coalg}, a.hylo{coalg}))
}
Note how Term has gone completely in this final variant!
Your Turn!
Now it’s your turn to experiment further with this construction of recursion schemes. How could you implement a factorial via a paramorphism or hylomorphism? How could a histomorphism and futumorphism be defined in Effekt? Do you have other fun ideas for Effekt code?
Here’s a link to our interactive playground, a language tour, and the installation instructions. Have fun!