This transcript shows an example of a function that returns the expected result but causes the pretty-printer to fail with the error reference to unknown combinator: #0lib3
.> builtins.merge
There is probably a way to reproduce this issue with less code, but I ran into it while writing some recursion scheme code which I have simplified a bit for this transcript:
structural type Functor f = Functor (∀ g r1 r2. (r1 -> {g} r2) -> f r1 -> {g} f r2)
Functor.map : Functor f -> (∀ g r1 r2. (r1 -> {g} r2) -> f r1 -> {g} f r2)
Functor.map = cases Functor f -> f
structural type ListF a r = Nil | Cons a r
ListF.functor : Functor (ListF a)
ListF.functor = Functor (f -> cases
Nil -> Nil
Cons h t -> Cons h (f t))
hylo : Functor f -> (f b -> {h1} b) -> (a -> {h2} f a) -> a -> {h1, h2} b
hylo f fold unfold =
go start = fold ((Functor.map f) go (unfold start))
go
addNats : ListF Nat Nat -> Nat
addNats = cases
Cons x y -> x + y
Nil -> 0
unfoldNats : Nat -> ListF Nat Nat
unfoldNats n = if n <= 4 then Cons n (Nat.increment n) else Nil
.> add
Running this code will sum 0-4, which returns 10 as expected.
> hylo ListF.functor addNats unfoldNats 0
But if we partially apply the code to get back a Nat
-> Nat
, then we get a runtime error with an unhelpful error message. I believe that this is coming from the pretty-printer when attempting to pretty-print the function.
> let
x : Nat -> Nat
x = hylo ListF.functor addNats unfoldNats
x