functor-combinators

functor-combinators copied to clipboard

This implements HFix and HCofree. This PR is more a request for feedback than an actual proposal. Much of the contents of this library goes way over my head, and you say explicitly that the goal of the library is not to implement the fixpoint.

That said, we have been using HFix and HCofree pretty successfully, and it might be useful to merge upstream. In particular, we describe programs with a GADT which looks a bit like

data Foo f k where
  Foo :: f k -> Foo ('S k)

HFix Foo makes it a recursive data structure, and the HCofree Foo SNat is that recursive data annotated with witnesses. If you do think that this fits the goal of functor-combinators, let me know and I'll clean this up so it can be merged.

This looks good, actually -- HFix is not too far off from HFree, which is already in the package :) Would be happy to merge this in once cleaned up. Thank you!