参数化高阶抽象语法(PHOAS)结构图编码
我正在看报纸结构化图的函数式编程奥利维拉和库克(幻灯片,草稿纸上。)在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))
折叠(to list)
AST可以折叠成list而不考虑循环:
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 For Free
这让我想起了Edward Kmett在FPComplete上的一篇精彩文章:免费拍照。这个想法是使AST成为一个profunctor,分离PHOAS变量的负和正出现。
带place-order"的函子用类似于自由单子的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
。(如joinPS1
类型)
我认为这与粘合剂的递归特性有关。我试图通过使用类型来重写unrollPS1
,但我不确定是否对值级别上发生的事情有充分的理解。
一个完全通用的joinPS1
类型(由编译器推断)是
joinPS1 :: PS1 x (PS1 x' a a') (PS1 x a' b) -> PS1 x a' b
可以专门化a' ~ a ~ b
和x' ~ x
。
我并没有试图取得什么具体的成就,这更多的是好奇心的问题,就像试图把这些点联系起来。
所有实例的完整代码是
实际上您可以轻松地从我的"profunctor HOAS"自由单子连接中重建Olivera和Cook的join
:
joinPS1 = join . lmap Var
他们的版本做了在他们的类型中唯一能做的事情。
他们必须保留a = b
,所以它通过引入Var
来实现。我们可以单独穿上。它不是单子所必需的,也不应该在所有情况下都这样做。
需要来保持a
和b
同步,这就是为什么它们只能是一个"伪单子",为什么profunctor HOAS让你实际上有一个真正的单子。