4

我正在尝试使用数据类型点菜的方法来定义一个免费的 monad 用于模板目的。我写了一些组合器，但我被卡住了。我的程序不断分歧，我不明白为什么。

考虑：

math :: Math :<: f => MathExpr a -> Free f ()
blank :: f :<: (Textual :+: Math) => Free f () -> Free (Blank k f) ()
equals :: Free (Math :+: (Blank L Math)) ()
       -> Free (Math :+: (Blank R Math)) ()
       -> Free Equation ()

组合（空白。数学）具有以下类型：

blank . math :: ( f :<: (Textual :+: Math)
                , Math :<: f
                ) => MathExpr a -> Free (Blank k f) ()

请注意，f 必须同时小于 Textual 和 Math 的连接，并且大于 Math。所以 f 的唯一可能性是数学。（我意识到如果没有我的更多工作，编译器无法推断出这一点，如果有的话）

当我尝试评估时会出现问题：

test :: Free Equation ()
test = (hoistFree (inj :: Blank 'L Math a -> (Math :+: Blank 'L Math) a)
     . blank
     . (math :: MathExpr x -> Free Math ())
     $ "hi"
     )
     `equals` (math $ "world")

这显然是循环的，将我的 CPU 固定在 100%。计算将其结果打印为：

Free (Equation (Free (DirectSum {unDirectSum = Right

此时该值被截断并且 GHCi 退出。因此，它显然可以确定 equals 的第一个参数位于直接和的后半部分，但它似乎无法计算空白。

我所有的功能都是完整的，我在这里看不到底部，但我从来都不擅长定点组合器。有任何想法吗？

编辑：带有免费 monad 的模块现在位于： http ://lpaste.net/93471 模块 Data.Domain 位于：http ://lpaste.net/93472

4

1 回答 1

1

（我没有足够的代表发表评论，所以我正在做这个蹩脚的答案......）

您 lpastes 中的代码（几乎）适用于 GHC 7.6.3 和 free-3.4.2

为了进行类型检查，我确实必须更改一些东西，但它们非常简单。

  • 将 (MathExpr a) 替换为文本。

  • 添加 -XKindSignatures 和 -XOverloadedStrings。

  • 对（显示空白）派生使用独立派生。

    派生实例 (Show (g (Free g ())), Show f) => Show (Blank kgf)

我只能想象那些影响终止的最后一个。

在这些更改之后，我在 ghci 中看到了这一点：

*> test
Free (Equation (Free (DirectSum {unDirectSum = Right (Blank (Free (Math "hi" (Pure ()))) (Pure ()))})) (Free (DirectSum {unDirectSum = Left (Math "hello" (Pure ()))})) (Pure ()))

那么，也许您正在使用 GHC 和免费的过时/错误组合？HTH。

于 2013-09-27T20:41:38.560 回答