News aggregator

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

Haskell on Reddit - Sat, 07/05/2014 - 6:43pm

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) = ?what

Now, 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

filter f (x::xs) = xs

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:

if f x then xs else x : xs if f x then xs else [x]

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.

submitted by meditans
[link] [9 comments]
Categories: Incoming News

withFile variant which takes a ByteString?

haskell-cafe - Sat, 07/05/2014 - 4:52pm
Hi all, Is there a variant of withFile which takes a ByteString? (I'm aware that I could use the lower-level System.Posix FD-based functions, but if someone already has a package out there, I'd rather not.) Regards,
Categories: Offsite Discussion

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

General haskell list - Sat, 07/05/2014 - 2:44am
PRDC2014 Call for Fast Abstracts / Industry Track Papers / Posters Singapore Nov.18-21,2014 http://prdc.dependability.org/PRDC2014/index.html --------------------------------- Call for Fast Abstracts http://prdc.dependability.org/PRDC2014/cffa.html --------------------------------- Fast Abstracts at PRDC are short oral presentations, either on new ideas or work in progress, or opinion pieces that can address any issue relevant to dependable systems and networks. Because they are brief and have a later deadline, Fast Abstracts enable their authors to: .Summarise work that is not yet complete .Put forward novel or challenging ideas .State positions on controversial issues .Suggest new approaches to the solution of open problems Thus, they provide an excellent opportunity to introduce new work, or present radical opinions, and receive early feedback from the community. Contributions are particularly solicited from industrial practitioners and academics that may not have been able to prepare full papers du
Categories: Incoming News

HART 2014 - deadline extended

General haskell list - Fri, 07/04/2014 - 3:11pm
We extended the deadline until 12th July. ========================================= CALL FOR PAPERS Second Workshop on Haskell And Rewriting Techniques (HART 2014) http://www.program-transformation.org/HART14/ To be held on September 5, co-located with ICFP 2014, the Haskell Symposium, etc., in Gothenburg. Haskell is an advanced purely-functional programming language. Pure functional programming is programming with equations, often defined by pattern-matching. Rewriting is the science of replacing equals by equals and thus a very powerful method for dealing with equations, often constructor-based. There are strong connections between Haskell (or generally, pure functional) programming and rewriting. The purpose of the HART workshop is to foster those connections. In addition to an invited talk by Oleg Kiselyov, we plan a half day of discussions, in an informal setting, on how Haskell (and related languages) and rewriting techniques and theories can cross-fert
Categories: Incoming News

Final Call for Papers: OCL 2014 Submissions Due in OneWeek

General haskell list - Thu, 07/03/2014 - 4:15pm
(Apologies for duplicates) CALL FOR PAPERS 14th International Workshop on OCL and Textual Modeling Applications and Case Studies (OCL 2014) Co-located with ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014) September 28-30 (tbc), 2014, VALENCIA, SPAIN http://www.software.imdea.org/OCL2014/ Modeling started out with UML and its precursors as a graphical notation. Such visual representations enable direct intuitive capturing of reality, but some of their features are difficult to formalize and lack the level of precision required to create complete and unambiguous specifications. Limitations of the graphical notations encouraged the development of text-based modeling languages that either integrate with or replace graphical notations for modeling. Typical examples of such languages are OCL, textual MOF, Epsilon, and Alloy. Textual modeling languages have thei
Categories: Incoming News

Haskell Weekly News: Issue 298

General haskell list - Thu, 07/03/2014 - 6:59am
Welcome to issue 298 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers from June 15 to 28, 2014 Quotes of the Week * Kinnison * imagines a radio station playing only things like 'Life tru a Lens', stuff by 'Dire States' or 'Monadonna' Top Reddit Stories * Today I published an introductory book on Haskell Data Analysis Domain: haskelldata.com, Score: 99, Comments: 26 Original: [1] http://goo.gl/R2kRFu On Reddit: [2] http://goo.gl/Ka0oP5 * Backpack: An ML-like module system for Haskell Domain: plv.mpi-sws.org, Score: 76, Comments: 44 Original: [3] http://goo.gl/7Zkxbg On Reddit: [4] http://goo.gl/78H37f * Cgrep, a context-aware grep for source code. Domain: awgn.github.io, Score: 67, Comments: 13 Original: [5] http://goo.gl/q1VdEA On Reddit: [6] http://goo.gl/2NNTrO * Teenage Haskell Domain: twdkz.wordpress.com, Score: 63, Comments: 7 Original: [7] http://goo.gl/c
Categories: Incoming News

New gtk2hs 0.12.4 release

gtk2hs - Wed, 11/21/2012 - 12:56pm

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

Categories: Incoming News