参数化高阶抽象语法（PHOAS）的结构图编码

我正在阅读Olivera和Cook（Slides，draft paper.）的论文“Functional Programming with Structured Graphs”，提出了一个优雅的解决方案，在PHOAS中使用递归绑定来编码类图结构中的共享和循环。

AST（流示例）

例如，具有后边缘的流可以被编码为：

-- 'x' is the element type, 'b' is the PHOAS's abstract variable:
data PS0 x b = Var0 b
             | Mu0 (b -> PS0 x b) -- recursive binder
             | Cons0 x  (PS0 x b)
-- Closed terms:
newtype Stream0 x = Stream0 { runS0 :: forall b. PS0 x b }

-- Example : [0, 1, 2, 1, 2, 1, 2, ...
exPS0 = Stream0 $ Cons0 0 (Mu0 $ \x -> Cons0 1 (Cons0 2 $ Var0 x))

折叠（至列表）

AST可以折叠成列表，而不考虑循环：

toListPS0 :: Stream0 x -> [x]
toListPS0 = go . runS0
  where
    go (Var0 x) = x
    go (Mu0 h) = go . h $ [] -- nil
    go (Cons0 x xs) =  x : go xs

-- toListPS0 exPS0 == [0, 1, 2]

或者，通过取递归绑定器的固定点，生成一个无限列表：

toListRecPS0 :: Stream0 x -> [x]
toListRecPS0 = go . runS0
  where
    go (Var0 x) = x
    go (Mu0 h) = fix $ go . h -- fixpoint
    go (Cons0 x xs) = x : go xs

-- toListRecPS0 exPS0 == [0, 1, 2, 1, 2, 1, 2, ...

准一元join

作者指出，编码是一个准单子，既有join，也有return，但没有fmap。

returnPS0 :: b -> PS0 x b
returnPS0 = Var0

joinPS0 :: PS0 x (PS0 x b) -> PS0 x b
joinPS0 (Var0 b) = b
joinPS0 (Mu0 h) = Mu0 $ joinPS0 . h . Var0
joinPS0 (Cons0 x xs) = Cons0 x $ joinPS0 xs

这可以用来展开一个级别的递归绑定：

unrollPS0 :: Stream0 x -> Stream0 x
unrollPS0 s = Stream0 $ joinPS0 . go $ runS0 s
  where
    go (Mu0 g) = g . joinPS0 . Mu0 $ g
    go (Cons0 x xs) = Cons0 x $ go xs
    go e = e

-- toListPS0 . unrollPS0 $ exPS0 == [0, 1, 2, 1, 2]

PHOAS免费

这让我想起了Edward Kmett在FPComplete上的一篇优秀文章：PHOAS For Free。这个想法是让AST成为一个profunctor，分离PHOAS变量的负和正出现。
函子的“具有位置顺序的不动点”用类似自由单子的AST（Fegaras and Sheard）表示：

data Rec p a b = Place b
               | Roll (p a (Rec p a b))

假设p是一个原函子（或者p a是一个函子），Rec p a是一个单子（也是一个函子！）。
流AST可以用非递归函子PSF编码：

data PSF x a b = MuF (a -> b)
               | ConsF x   b

-- Type and pattern synonyms:
type PS1 x = Rec (PSF x)
pattern Var1 x = Place x
pattern Mu1 h = Roll (MuF h)
pattern Cons1 x xs = Roll (ConsF x xs)

-- Closed terms:
newtype Stream1 x = Stream1 { runS1 :: forall b. PS1 x b b }

-- Example : [0, 1, 2, 1, 2, 1, 2, ...
exPS1 = Stream1 $ Cons1 0 (Mu1 $ \x -> Cons1 1 (Cons1 2 (Var1 x)))

问题

来自Rec monad示例的join与论文中的原始joinPS1不同！
joinPS0使用模式同义词的文学翻译是：

joinPS1 :: PS1 x (PS1 x b b) (PS1 x b b) -> PS1 x b b
joinPS1 (Var1 b) = b
joinPS1 (Mu1 h) = Mu1 $ joinPS1 . h . Var1 -- Var1 affects the negative occurrences
joinPS1 (Cons1 x xs) = Cons1 x $ joinPS1 xs

然而，在(>>= id)中内联(>>=)和fmap给予：

joinFreePSF :: PS1 x a (PS1 x a b) -> PS1 x a b
joinFreePSF (Var1 b) = b
joinFreePSF (Mu1 h) = Mu1 $ joinFreePSF . h -- No Var1 !
joinFreePSF (Cons1 x xs) = Cons1 x $ joinFreePSF xs

所以我的问题是，为什么会有这种差异？
问题是像unrollPS1这样的操作需要一个join来“粉碎”monad的正和负出现（就像joinPS1类型）。
我想这与绑定器的递归特性有关，我试图通过处理类型来重写unrollPS1，但我不确定是否能完全理解值级别上发生的事情。

备注

joinPS1的完全通用类型（由编译器推断）是

joinPS1 :: PS1 x (PS1 x' a a') (PS1 x a' b) -> PS1 x a' b

它可以专用于a' ~ a ~ b和x' ~ x。

PS：

我并不想达到什么具体的目标，这更多的是一种好奇心，就像试图把这些点联系起来。
所有示例的完整代码是available here (gist)。