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

Question

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

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

Djinn 可以使用定理证明，通过证明该类型存在来生成此类函数的代码。

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

我安装了 ghc-mod，但我不太熟悉它。

Answer 1

引用Serras的相关部分emacs guide :

This is nice, but in some cases ghc-mod can do even more for you: it can write your whole expression! It does so by leveraging the power of Djinn. For example, let's go back to the definition of maybeMap after splitting:

maybeMap Nothing f = _maybeMap_body

maybeMap (Just x) f = _maybeMap_body

If you press C-c C-a in each of the holes, several options for the code to be written there will be shown, including Nothing in the first case, and Nothing and Just x in the second case. You just need to select the code you want to include from a list, and it will be automatically completed. Note that this functionality becomes very handy when you need to work with expressions involving currying and tupling, because it takes care of obtaining a correctly-typed expression for you.

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