如何为Mu递归类型编写Show实例

use*_*561 0 haskell show recursive-datastructures fixpoint-combinators

我想为Show以下类型的列表编写一个实例:

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)
Run Code Online (Sandbox Code Playgroud)

模块Data.Functor.Foldable定义了它,但将其转换为Fix,我想避免这种情况。

如何定义该Show实例?

Wil*_*ess 5

口号是“跟随类型!” ,全职在这里为我们工作。

从您的代码中进行一些重命名,以便于理解,

{-# LANGUAGE RankNTypes #-}

data ListF a r = Nil | Cons a r deriving (Show)
newtype List a = Mu {runMu :: forall r. (ListF a r -> r) -> r}
Run Code Online (Sandbox Code Playgroud)

这样我们就可以

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))))))
-}
Run Code Online (Sandbox Code Playgroud)

我们想要

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

...我们必须产生一个字符串;我们只能打电话 f ; 它的论点是什么?根据其类型,

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

此处似乎没有其他方法可以连接电线。

以此print $ fromList [1..5]打印(1 2 3 4 5 )

实际上,事实证明这是chi答案的详细版本。

编辑: g是“代数”(谢谢@chi!),f(中Mu f是)是“折叠”。现在,这种类型的含义变得更加清晰:给定一个“代数”(归约函数),一个Mu f值将在该“折叠函数”所表示的“固有列表”的折叠中使用它。它在折叠的一步上使用一步还原语义来表示列表的折叠。