How to use Functor instances with Fix types

Question

Let's say I want to have a very generic ListF data type:

{-# LANGUAGE GADTs, DataKinds #-}

data ListF :: * -> * -> * where
  Nil  ::           List a b
  Cons :: a -> b -> List a b

Now I can use this data type with Data.Fix to build an f-algebra

import qualified Data.Fix as Fx

instance Functor (ListF a :: * -> *) where
  fmap f (Cons x y) = Cons x (f y)
  fmap _ Nil        = Nil

sumOfNums = Fx.cata f (Fx.Fix $ Cons 2 (Fx.Fix $ Cons 3 (Fx.Fix $ Cons 5 (Fx.Fix Nil))))
  where
    f (Cons x y) = x + y
    f Nil        = 0

But how I can use this very generic data type ListF to create what I consider the default Functor instance for recursive lists (mapping over each value in the list)

I guess I could use a Bifunctor (mapping over the first value, traversing the second), but I don't know how that could ever work with Data.Fix.Fix?

Skirr

Answer 1

Quite right to construct a recursive functor by taking the fixpoint of a bifunctor, because 1 + 1 = 2. The list node structure is given as a container with 2 sorts of substructure: "elements" and "sublists".

It can be troubling that we need a whole other notion of Functor (which captures a rather specific variety of functor, despite its rather general name), to construct a Functor as a fixpoint. We can, however (as a bit of a stunt), shift to a slightly more general notion of functor which is closed under fixpoints.

type p -:> q = forall i. p i -> q i

class FunctorIx (f :: (i -> *) -> (o -> *)) where
  mapIx :: (p -:> q) -> f p -:> f q

These are the functors on indexed sets, so the names are not just gratuitous homages to Goscinny and Uderzo. You can think of o as "sorts of structure" and i as "sorts of substructure". Here's an example, based on the fact that 1 + 1 = 2.

data ListF :: (Either () () -> *) -> (() -> *) where
  Nil  :: ListF p '()
  Cons :: p (Left '()) -> p (Right '()) -> ListF p '()

instance FunctorIx ListF where
  mapIx f Nil        = Nil
  mapIx f (Cons a b) = Cons (f a) (f b)

To exploit the choice of substructure sort, we'll need a kind of type-level case analysis. We can't get away with a type function, as

1. we need it to be partially applied, and that's not allowed;
2. we need a bit at run time to tell us which sort is present.

data Case :: (i -> *) -> (j -> *) -> (Either i j -> *)  where
  CaseL :: p i -> Case p q (Left i)
  CaseR :: q j -> Case p q (Right j)

caseMap :: (p -:> p') -> (q -:> q') -> Case p q -:> Case p' q'
caseMap f g (CaseL p) = CaseL (f p)
caseMap f g (CaseR q) = CaseR (g q)

And now we can take the fixpoint:

data Mu :: ((Either i j -> *) -> (j -> *)) ->
           ((i -> *) -> (j -> *)) where
  In :: f (Case p (Mu f p)) j -> Mu f p j

In each substructure position, we do a case split to see whether we should have a p-element or a Mu f p substructure. And we get its functoriality.

instance FunctorIx f => FunctorIx (Mu f) where
  mapIx f (In fpr) = In (mapIx (caseMap f (mapIx f)) fpr)

To build lists from these things, we need to juggle between * and () -> *.

newtype K a i = K {unK :: a}

type List a = Mu ListF (K a) '()
pattern NilP :: List a
pattern NilP       = In Nil
pattern ConsP :: a -> List a -> List a
pattern ConsP a as = In (Cons (CaseL (K a)) (CaseR as))

Now, for lists, we get

map' :: (a -> b) -> List a -> List b
map' f = mapIx (K . f . unK)

Hightension

I don't really understand what makes Mu a fixpoint operator. Can you maybe explain that? I'm also struggling to see how this mechanism improves (theoretically) over the (admittedly rather annoying) profusion of Functor, Bifunctor, Trifunctor, etc., classes. This probably just reflects the limits of my own understanding of these abstract notions, but I'm probably not the only one who doesn't quite get it. – Flagstaff

Also, do you think you could offer a less trivial example, such as expressing the free indexed monad using Mu? Or is that an absurd notion for some reason? – Flagstaff

Hrm... Actually, I seem to have gotten a free indexed monad, but it's rather messy. data FreeF :: ((s -> *) -> (s -> *)) -> (Either s s -> *) -> (s -> *) where PureF :: p ('Left s) -> FreeF f p s FreeF :: f (Compose p 'Right) s -> FreeF f p s where the Compose in question has kind (k -> *) -> (s -> k) -> (s -> *), and then the free indexed monad seems to be Free f = Mu (FreeF f). But maybe there's a better way one could find if one understood these ideas better. – Flagstaff

Then there's the question of what to do about structures that don't look like lists.... – Flagstaff

@Flagstaff More later, but a handy hint for now. (Either i j -> *) -> (j -> *) is, by coproducty goodness, an isotope of (i -> *, j -> *) -> (j -> *). And that curries out to (i -> *) -> (j -> *) -> (j -> *). We're really making a fixpoint on j -> * parametrized by some i -> *, just like in the usual Bifunctor fixpoint. – Hightension

Yes, I thought about that curried version a bit. But the final result ... doesn't really look very fixpointy, either in kind or in structure. And there's the rather strange apparent redundancy in information provided by the base functor and that provided by Case. – Flagstaff

It's a whole lot cleaner in languages with proper higher-order type-level programming. – Hightension

Answer 2

I guess I could use a Bifunctor (mapping over the first value, traversing the second), but I don't know how that could ever work with Data.Fix.Fix?

You hit the nail on the head.

The bifunctors package contains a "Fix-for-bifunctors" type which looks like this:

newtype Fix f a = In { out :: f (Fix f a) a }

Fix f is a Functor whenever f is a Bifunctor. fmap recursively fmaps f's first parameter and maps the second.

instance Bifunctor f => Functor (Fix f) where
    fmap f = In . bimap (fmap f) f . out

So your List example would look like this:

data ListF r a = Nil | Cons r a

type List = Fix ListF

map :: (a -> b) -> List a -> List b
map = fmap

Oceania

Something to keep in mind: Due the the argument order of Fix, the "regular" Bifoldable instance will produce toList @List in reverse.. – Leucippus