4

Title pretty much says it all. I'm looking for something like this:

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

Djinn can use theorem proving to generate code for such a function by proving that the type is inhabited.

I'm wondering, is there an existing way to get this functionality from within Emacs? So instead of writing TemplateHaskell in my code, I just run a command on my code and it inserts the generated code?

I have ghc-mod installed, but I'm not very familiar with it.

jmite
  • 8,171
  • 6
  • 40
  • 81
  • I'm not sure what the answer is, but I feel like that would have pretty limited utility. In fact, the code you gave is a good example of where Djinn would likely not be very useful (there's a *huge* number of inhabitants of that type. For a 64-bit `Int` size, I believe it would have `((2^64)^2)^(2^64)` inhabitants if I did my math right). It would mostly be useful for polymorphic types but it doesn't support type classes and I don't think it's been updated in a while. – David Young Feb 07 '15 at 20:11
  • Yeah, the example I gave wasn't meant to be practical, more just a syntactic example. – jmite Feb 07 '15 at 20:16

1 Answers1

2

Quoting the relevant part of 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.

So, yes using Djinn you can write whole expressions in some cases. I haven't personally used them but it seems to be possible in Emacs.

Sibi
  • 47,472
  • 16
  • 95
  • 163