haskellshowrecursive-datastructuresfixpoint-combinators

How to write a Show instance for Mu recursive types


I want to write an instance of Show for lists of the following type:

newtype Mu f = Mu (forall a. (f a -> a) -> a)
data ListF a r = Nil | Cons a r deriving (Show)
type List a = Mu (ListF a)

Module Data.Functor.Foldable defines it, but it converting it to Fix, something I want to avoid.

How can I define this Show instance?


Solution

  • The slogan, "Follow the types!", works for us here, fulltime.

    From your code, with some renaming for easier comprehension,

    {-# LANGUAGE RankNTypes #-}
    
    data ListF a r = Nil | Cons a r deriving (Show)
    newtype List a = Mu {runMu :: forall r. (ListF a r -> r) -> r}
    

    So that we can have

    fromList :: [a] -> List a
    fromList (x:xs) = Mu $ \g -> g   -- g :: ListF a r -> r
                                   (Cons x $                 -- just make all types fit
                                      runMu (fromList xs) g)
    fromList []     = Mu $ \g -> g Nil
    
    {-   or, equationally,
    runMu (fromList (x:xs)) g = g (Cons x $ runMu (fromList xs) g)
    runMu (fromList [])     g = g Nil 
    
         such that (thanks, @dfeuer!)
    runMu (fromList [1,2,3]) g = g (Cons 1 (g (Cons 2 (g (Cons 3 (g Nil))))))
    -}
    

    and we want

    instance (Show a) => Show (List a) where
     -- show :: List a -> String
     show (Mu f) = "(" ++ f showListF ++ ")"            -- again, just make the types fit
    

    ... we must produce a string; we can only call f; what could be its argument? According to its type,

      where
      showListF :: Show a => ListF a String -> String   -- so that, f showListF :: String !
      showListF Nil        = ...
      showListF (Cons x s) = ...
    

    There doesn't seen to be any other way to connect the wires here.

    With this, print $ fromList [1..5] prints (1 2 3 4 5 ).

    Indeed this turned out to be a verbose version of chi's answer.

    edit: g is for "algebra" (thanks, @chi!) and f (in Mu f) is for "folding". Now the meaning of this type becomes clearer: given an "algebra" (a reduction function), a Mu f value will use it in the folding of its "inherent list" represented by this "folding function". It represents the folding of a list with one-step reduction semantics, using it on each step of the folding.