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

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

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

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

我安装了ghc-mod,但我对它不是很熟悉.

最佳答案 引用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中使用.