# News aggregator

### On smart code-completion in Haskell, idris-mode style. (Advice needed)

**tl;dr** I'd like to hear your opinion about smart code completion in haskell, in the spirit of agda-mode or idris-mode, and propose two possible way to limit the information loss caused by having a weaker type-system.

I really like the completion mechanism for code in languages with full dependent types like Idris or Agda. I'd like similar (or better) code completion facilities for Haskell.

To see how this could be done, let's start with a idris example:

filter : (a -> Bool) -> List a -> List a filter f [] = [] filter f (x::xs) = ?whatNow, a type-correct (and minimal, in the sense of proof search) completion of ?what is xs, and is in fact the answer of idris-mode. This is of course not ok, so let's say you want a precise enough type to be able to generate the function automatically. You could encode additional invariants in your function, beginning with:

filter : {a : Type} -> {P : a -> Type} -> (decideP : (x : a) -> Dec (P x)) -> List a -> List (x : a ** P x)or the code in this paste. (thanks to ziman and {AS} for the conversation in #idris and the examples). At the end of the spectrum, you could encode all your invariants in the type.

On the flip side, I don't see a general, easy way to balance specification vs. code, and I fear the proliferation of many functions essesntially on the same object but with different specifications. **Moreover**, I'd like to take advantage of the rich ecosystem and the wonderful compiler we have in haskell.

So, how could we alleviate the loss of dependent types? The answer I'm thinking of is a mixture of heuristics and code generation via examples.

**Heuristics:** One could argue that in the second definition of filter, the answer

fails to recognise the role f and x could have in the equation. In a sense, this expression scores low on the heuristic "argument usage". Another heuristics may me the number of function applications in your code (lower is better), which could rule out the obvious pitfalls of a naive theorem prover (solutions like x : [], x : x : [], x : x : x : [] etc). One could also guide the program towards the intended implementation writing "hints", functions that we imagine would be used in the final implementation (heuristic: hint-usage).

Other heuristics could be found among the standard ones used in automated theorem proving. The point here is that it seems to me that there are sufficient good heuristics avaiable to guide the writing of our code.

**Code generation via examples:** The second point I'd like to make is related to interface: even using all heuristics we are able to come up with, the answer could still typecheck without being what we had in mind:

So here the program could take simple arguments (or even generate them via quickCheck), like odd :: Integral a => a -> Bool, and [1,2,3,4,5], and output various possible answers for filter odd [1,2,3,4,5], based on the different implementations it can come up with. Hopefully choosing the expected answer could guide the program towards a unique correct implementation.

On a final note, I have "tested" this approach with some (simple, but not too simple) programs (imagining the heuristics that would be used, and the examples that would guide the generation). The results seemed nice to me, and having those automated would be a great speedup for my coding.

So, I'd like to hear your thoughts here, expecially on:

What flaws/problems/shortcomings may this approach have, in your opinion? Please provide some example.

Could you name programs/tools that I should probably use in this project, and why?

Do you know some papers/theory I should definitely read to refine my approach?

If you're a person interested in giving occasional hints and guidance on the overall architecture, be sure to write it below.

Extra advices are always appreciated, even if they don't belong to previous categories.

[link] [9 comments]

### withFile variant which takes a ByteString?

### CFP: PRDC2014 Call for Fast Abstracts / Industry Track Papers / Posters

### HART 2014 - deadline extended

### Final Call for Papers: OCL 2014 Submissions Due in OneWeek

### Haskell Weekly News: Issue 298

### New gtk2hs 0.12.4 release

Thanks to John Lato and Duncan Coutts for the latest bugfix release! The latest packages should be buildable on GHC 7.6, and the cairo package should behave a bit nicer in ghci on Windows. Thanks to all!

~d