在存在递归绑定器的情况下,单独出现PHOAS变量的正面和负面事件

Question

参数高阶抽象语法(PHOAS)中的结构化图形编码

我在读纸通过奥利韦拉和Cook"与结构化图形函数式编程"(幻灯片, 纸草案.)提出一种优雅的解决方案来编码在使用递归绑定在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

作者指出,编码是一个准monad,有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成为一个分析者,分离出PHOAS变量的负面和正面出现.

仿函数的"具有位置顺序的固定点"用类似于自由monad的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可以使用非递归仿函数进行编码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)))

问题

在join从Rec单子实例比原来不同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"粉碎"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:

我不会尝试实现任何特定的东西,更多的是好奇心,比如尝试连接点.

这里提供了包含所有实例的完整代码 (要点).

Answer 1

join实际上，您可以从我的“profunctor HOAS”免费 monad join轻松重建 Olivera 和 Cook ：

joinPS1 = join . lmap Var

他们的版本做了他们类型中唯一能做的事情。

他们必须保留a = b，因此它通过引入Var. 这里我们可以单独放置。它不是 monad 所必需的，也不应该在所有情况下都这样做。

保持同步的需要是为什么它们只能是一个“伪单子”，也是为什么 profunctor HOAS 让你实际上拥有一个真正的单子。ab