Skip to content

Instantly share code, notes, and snippets.

@ceedubs
Created May 10, 2023 01:29
Show Gist options
  • Save ceedubs/77b29537899c8a5c56bc7968400d815d to your computer and use it in GitHub Desktop.
Save ceedubs/77b29537899c8a5c56bc7968400d815d to your computer and use it in GitHub Desktop.
`reference to unknown combinator` when pretty-printing function

reference to unknown combinator when pretty-printing function

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment