ANN: exference: a different djinn
Hello folks, Exference[1] is a Haskell tool for generating expressions from a type, e.g. Input: (Show b) => (a -> b) -> [a] -> [String] Output: \ b -> fmap (\ g -> show (b g)) In contrast to Djinn, the well known tool with the same general purpose, Exference supports a larger subset of the haskell type system - most prominently type classes. (Djinn's environment many contain type classes, but using them in queries will not really work.) This comes at a cost, however: Exference makes no promise regarding termination. Where Djinn tells you "there are no solutions", Exference will keep trying, sometimes aborting a non-ending search with "i could not find any solutions". See [2] for a report about the implementation, capabilities and limitations. [1] https://github.com/lspitzner/exference [2] https://github.com/lspitzner/exference/raw/master/exference.pdf Lennart
Could this somehow be used with the GHC API, so that it could be embedded as autocomplete in an interpreter / code editor? I am imagining using this with GHC 7.10 Type Holes in IHaskell. To autocomplete, you'd insert a hole ("_"), GHC would be able to tell you the type of the hole, you'd be able to pass it to exference, and then your autocomplete suggestions would be full expressions. Does this sound plausible? Sounds like a very cool tool! Andrew On Sun, Apr 26, 2015 at 9:08 AM, lennart spitzner < lsp@informatik.uni-kiel.de> wrote:
Hello folks,
Exference[1] is a Haskell tool for generating expressions from a type, e.g.
Input: (Show b) => (a -> b) -> [a] -> [String]
Output: \ b -> fmap (\ g -> show (b g))
In contrast to Djinn, the well known tool with the same general purpose, Exference supports a larger subset of the haskell type system - most prominently type classes. (Djinn's environment many contain type classes, but using them in queries will not really work.) This comes at a cost, however: Exference makes no promise regarding termination. Where Djinn tells you "there are no solutions", Exference will keep trying, sometimes aborting a non-ending search with "i could not find any solutions".
See [2] for a report about the implementation, capabilities and limitations.
[1] https://github.com/lspitzner/exference [2] https://github.com/lspitzner/exference/raw/master/exference.pdf
Lennart _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
On 26/04/15 19:38, Andrew Gibiansky wrote:
Could this somehow be used with the GHC API, so that it could be embedded as autocomplete in an interpreter / code editor?
I am imagining using this with GHC 7.10 Type Holes in IHaskell. To autocomplete, you'd insert a hole ("_"), GHC would be able to tell you the type of the hole, you'd be able to pass it to exference, and then your autocomplete suggestions would be full expressions. Does this sound plausible?
This certainly counts as a long-term goal for Exference. As it stands, there are two issues: a) ideally, Exference would take into account all locally defined (or even all visible) functions. This is problematic, as one generally has to be careful adding too many / the wrong functions to the environment because it can blow up the search space. There might be some heuristics to determine what can safely be added; alternatively the user could selectively add functions. b) performance in general is not as good as i would like, both memory and run-time. (to give you an idea: running my test-cases needs something in the range of 3GB memory, the default even is at -M4G.) There certainly is room for optimizations; also i have not really tested what types of queries can be solved when you give tight limits to memory/run-time. Lennart
a) ideally, Exference would take into account all locally defined (or even all visible) functions. This is problematic, as one generally has to be careful adding too many / the wrong functions to the environment because it can blow up the search space. There might be some heuristics to determine what can safely be added; alternatively the user could selectively add functions.
Is this a major problem? As far as I can tell Agda's automated proof search does not take into account any globally defined functions or constants and yet is still (moderately) useful. Have you seen the recent announcement of Mote, a Vim plugin trying to replicate something akin to Agda-mode for Haskell? https://github.com/imeckler/mote It seems that marrying these two projects, extending Mote with a search facility based on exference, would be a good idea?
On 27/04/15 11:23, Dominic Mulligan wrote:
Is this a major problem? As far as I can tell Agda's automated proof search does not take into account any globally defined functions or constants and yet is still (moderately) useful.
No, i just have high expectations :) Even with just the current functionality, if there is a typed hole in an expression like `f = _ x y` if the user knows that the implementation will involve some specific global function bar, she could write `f = _ bar x y`.
Have you seen the recent announcement of Mote, a Vim plugin trying to replicate something akin to Agda-mode for Haskell? It seems that marrying these two projects, extending Mote with a search facility based on exference, would be a good idea?
In a way it even inspired me to (finally) make the announcement. I have not, but will try to find time to play with Mote in the next days.
participants (3)
-
Andrew Gibiansky -
Dominic Mulligan -
lennart spitzner