Parametric Higher Order Abstract Syntax（PHOAS）中的结构化图编码
我正在阅读Olivera和Cook的论文“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。 这个想法是将AST变成profunctor，分离PHOAS变量的负面和正面出现。
一个函数子的“带有位置顺序的不动点”可以用类似自由单子的AST来表示 (Fegaras 和 Sheard)：
data Rec p a b = Place b
| Roll (p a (Rec p a b))
假设p是一个 profunctor（或 p a 是一个functor），则 Rec p a 是一个monad（和一个 functor！）。
流AST可以使用非递归的functor PSF 进行编码：
<code>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)))
</code>
问题
Rec单子实例中的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
然而，将 (>>=) 和 fmap 内联到 (>>= id) 中会给我们带来：
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 来“粉碎”单子的正负出现（就像在 joinPS1 类型中一样）。
我认为这与绑定器的递归性质有关。我尝试通过处理类型来重写 unrollPS1，但我不确定自己是否完全理解了值级别上正在发生的事情。
备注
编译器推断出的 joinPS1 的完全通用类型为
joinPS1 :: PS1 x (PS1 x' a a') (PS1 x a' b) -> PS1 x a' b
它可以通过 a' ~ a ~ b 和 x' ~ x 进行专门化。
附言：
我并不试图实现任何特定的目标，更多的是出于好奇心，就像尝试连接各个点一样。
所有实例的完整代码在 这里（gist） 可用。