haskell - 有没有办法使用 Djinn 在 Emacs 中自动生成 Haskell 代码？

Question

标题几乎说明了一切。我正在寻找这样的东西：

f :: Int -> Bool -> Int
f = _body

Djinn 可以使用定理证明来通过证明该类型是有人居住的来为此类函数生成代码。

我想知道，是否有从 Emacs 中获取此功能的现有方法？所以不是在我的代码中编写 TemplateHaskell，我只是在我的代码上运行一个命令并插入生成的代码？

我已经安装了 ghc-mod，但我对它不是很熟悉。

Answer 1

引用 Serras emacs guide的相关部分：

这很好，但在某些情况下 ghc-mod 可以为您做更多的事情：它可以编写您的整个表达式！它通过利用 Djinn 的力量来做到这一点。例如，让我们回到拆分后的mayberMap的定义：

MaybeMap 什么都没有 f = _maybeMap_body

MaybeMap (Just x) f = _maybeMap_body

如果在每个孔中按 Cc Ca，将显示要编写的代码的几个选项，包括第一种情况下的 Nothing，以及第二种情况下的 Nothing 和 Just x。您只需要从列表中选择要包含的代码，它就会自动完成。请注意，当您需要使用涉及柯里化和元组的表达式时，此功能会变得非常方便，因为它会为您获取正确类型的表达式。

所以，是的，在某些情况下，你可以使用 Djinn 编写整个表达式。我没有亲自使用它们，但在 Emacs 中似乎是可能的。