`refold :: Functor s => (a -> s a, a) -> (s b -> b) -> b` as a morphism between universal types

Question

Various recursion scheme boil down to specific instantiation of refold

refold :: Functor s => (s b -> b) -> (a -> s a) -> a -> b
refold f g = go where go a = f (fmap go (g a))

What is the meaningful interpretation of refold ?

The data type data Nu f = forall a. Nu (a -> f a) a and newtype Mu f = Mu {unMu :: forall b. (f b -> b) -> b} can be seen as the colimit and limit of the forget functor from coalgebras and algebras, and refold is a morphism between those, but does it shed light on refold ?

refold' :: forall s. Functor s => Nu s -> Mu s
refold' (Nu g (a :: a)) = Mu mu where

  mu :: forall b. (s b -> b) -> b
  mu f = go a where

    go :: a -> b
    go a = f (fmap go (g a))

Gory

Non-termination might play a tricky role here. Consider f a = Either () a. Now Mu f is the type of (finite) natural numbers, while Nu f also adds an "infinity" value to naturals. Yet, we have isos isoNu :: f (Nu f) -> Nu f and isoMu :: Mu f -> f (Mu f), which give us refold isoNu isoMu :: Nu f -> Mu f. I believe this has to diverge on the "infinity" value. – Toilette

@Toilette another argument : let's take s = identity. the type suggest it has to diverge – Gory

Answer 1

I guess it depends what you mean by "meaningful interpretation".

If s is a base functor for a recursive data type and a corecursive codata type, like the following functor s ~ ListF e for the recursive list data type [e] (which, in Haskell, is also a corecursive stream codata type):

{-# LANGUAGE DeriveFunctor #-}
data ListF e b = Nil | Cons e b deriving (Show, Functor)

then an s-coalgebra of type a -> s a together with a starting seed a can generate a value of codata type [e] by unfolding from that seed, while an s-algebra of type s b -> b can consume a value of data type [e] by folding into a value of type b. The refold function just combines the operation of unfolding from a and folding into b, without actually creating an intermediate codata/data type.

For example, you can generate the (finite) codata stream [10,9..1] by unfolding from an Integer seed using the starting value / coalgebra pair (a,g) as follows:

a :: Integer
a = 10

g :: Integer -> (ListF Integer) Integer
g 0 = Nil
g n = Cons n (n-1)

and fold a list to calculate its Int length using the algebra:

f :: (ListF Integer) Int -> Int
f Nil = 0
f (Cons _ b) = 1 + b

The refold function just combines these operations:

main = print $ refold f g a

In this particular case, it calculates the length 10 of the stream/list [1..10] without actually creating any intermediate stream/list.

I guess the intuition is that if an operation can be imagined as an F-recursion applied to an F-corecursion for the same functor F, then it's a refold. Or, maybe more practically, if an algorithm has an internal recursive structure that matches the functor F, it can be expressed as a refold. The documentation for refold in recursion-schemes gives the example of quicksort having a recursive structure that matches a binary tree, though you've presumably already seen that example.

Note: What follows is wrong or at best imprecise, but I'll try to think a little more about it.

In practice, refold isn't only used as a morphism between universal data types, but if you have a final s-coalgebra for a codata type C associated with the functor s:

eatC :: C -> ListF Integer C

and an initial s-algebra for a data type D also associated with the functor s:

makeD :: ListF Integer D -> D

then refold makeD eatC should be a natural morphism from codata type C to data type D. That is, it should be the unique morphism satsifying:

fmap h . refold makeD eatC = refold makeD eatC . fmap h

I'm not sure that aspect is tremendously interesting...

Tempestuous

Answer 2

A few remarks (which I imagine to be valid - don't hesitate to correct - I am not an expert on semantic) :

• non termination allow to write anything, as @chi suggested. take s the identity functor and refold reads refold :: (b -> b) -> (a -> a) -> a -> b which certainly looks like a paradox. So for any haskell type to be read "logically", we might need hidden, side conditions.

We don't even need recursion to encounter paradox / non termination

-- N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In LICS, pages 30–36. IEEE Computer Society, 1987
data T a = C (T a -> ())

p :: T a -> (T a ->() )
p (C f) = f

w :: T a -> ()
w x = (p x) x

• initial algebra, like monads, and other concepts, happens on two level, one in the semantic of a language, and another explicitly in the program that we write. For instance the semantic of data ListInt = [] | Int * ListInt is an initial algebra. and, in haskell, also, semantically, a final coalgebra. This is "Mu = Nu" that you might hear,and this equation, which is paradoxical, happens is in the semantic of haskell. Mu here has nothing to do with data Mu f = ... The same happen when we write type ListInt = Fix ListIntF where data Fix f = Fix (f (Fix f)) we are emulating that semantic in our program, but this itself is subject to the semantic of Haskell (and indeed, this (initial algebra) is the same as the semantic Mu and Nu and equal to both because haskell equates them). In a way by writing data Mu f = ... and data Nu f = .. we are "stealing" (and obliged to do so) part of haskell semantic, as well as mixing it with our own (properly expressing the universal co-cone Nu f and the universal cone Mu f), attempting at providing an embedding for recursion (just like we do with HOAS where we steal bindings from Haskell). But we can't get away with no paradox, as we are obliged to steal that "Mu = Nu".

  This leads to very useful and yet very "illogical" function like refold

• By writing fold : Functor s => (f a -> a) -> Fix s -> a we are pretending the initial algebra of f always exists, which might translate to non-termination

Categorically we can view refold in two different ways. It's a bit of a mouthful but here we go :

• refold can be seen as a proper function refold :: Functor s => (s b -> b) -> (a -> s a) -> a -> b to be detailed later

• refold' can be seen as the carrier refold' :: forall s. Functor s => Nu s -> Mu s of an algebra in Twisted(Hask), whose objects are morphisms in Hask. So refold' is an object, not a morphism, of this category. Now every functor s on a category C (here Hask) induces a functor s' on Twisted(C) by applying to arrows. In the end the morphism in Twisted

               `s' refold' -(out,in)-> refold'`
  

  is the initial s' algebra, where out is the "final" coalgebra Nu s -> s (Nu s) and in is the "initial" algebra Mu s -> s (Mu s)

Now the action of the function refold is, given a coalgebra and an algebra (here in Hask but could be elsewhere), to return the unique morphism from the carrier of the coalgebra, followed by refold', followed by the unique morphism from the initial algebra. This is a proper function that comes from selecting the components of the universal (co)cone at the given components.

This explains why when we feed the final coalgebra out and the initial algebra in to refold, we get back refold' itself. the unique morphism to pre and post compose refold' with are the identities.

It's a bit hard to see what's what because we work in Hask where everything is a function. Some morphisms are really about the category we work in (could be other things than Hask) and some morphism really are functions would be even if we chose another category.

Because of non termination the solution to knowing what really is refold has to being truthful to the semantic of haskell, and use complete partial order (or to restrict s in some way).

So I imagine the real meaning of refold can be deduced from the real meaning of refold' which is just a initial algebra, with all the standard caveat coming from haskell semantic threaded.

Gory

It seems to me that a function of type forall s. Functor s => Nu s -> Mu s cannot possibly be always terminating. Because Nu s could be infinite, it cannot be correctly mapped into Mu s and so refold must be a partial function. – Undressed