CODEWITHSUNDEEP
haskelltype-theorycatamorphismsystem-f
Wheat Wizard
Wheat Wizard

Reputation: 4219

Böhm-Beraducci encoding of Fix

I have the fixed point functor defined as follows:

newtype Fix f =
  Fix
    { unfix ::
      f (Fix f)
    }

I would like to define a function which takes a Fix f and gives its Böhm-Beraducci encoding. So that should have the type:

cata :: Fix f -> (forall a. (f a -> a) -> a)

I can easily define a function like this but with the additional constraint that f is a Functor, but I'm struggling without that restriction.

Intuitively I want to take the AST and replace all instances of the Fix constructor with an input function, however in practice that seems to require a Functor instance for F. But to my understanding the Böhm-Beraducci encoding should exist even when f is not a Functor.

I feel like I'm missing something simple here. Is there a definition I'm missing? If Functor is truly required, why? When does the Böhm-Beraducci encoding require additional constraints like this?

Upvotes: 3

Views: 68

Answers (1)

chi
chi

Reputation: 116139

From a quick look at the original paper, it looks like the Böhm-Berarducci encoding represent term algebras using System F types.

Term algebras essentially involve an implicit f which is always a functor.

Haskell goes beyond that and allows type-level fixed points on any f, even those which can not be turned into functors.

A famous example is the negative recursive type newtype R a = R { unR :: R a -> a }. The Haskell type system allows this type definition. Using this R a alone, and with no term-level recursion, we can derive fix :: forall a . (a -> a) -> a (a short but non trivial exercise, by the way).

System F, by contrast, can not be that general. If we had R a in System F, we would also have fix, hence fix id :: forall a . a could be used to inhabit any System F type. But we know System F is consistent, so that can not happen.

Upvotes: 2

Related Questions