Dan, I believe there was some work on this functionality for GHC some time ago (agda-like goals for GHC, where ? in agda merely becomes 'undefined' in haskell.) See:
https://github.com/sebastiaanvisser/ghc-goals This work was done a few years ago during a hackathon (the 09 Utrecht hackathon.) There is a frontend-executable providing goal information, as well as a patch to GHC to support it. It was never integrated into GHC and was left dead in the water essentially (for exactly what reasons, I do not know.) I find myself using the 'undefined' trick somewhat often as well. I'm not very familiar with agda, but familiar enough to have seen goals before in the interactive emacs mode, and I think this would be a nice feature for people who find themselves doing similar things. On Thu, Apr 28, 2011 at 3:18 PM, Dan Doel <dan.d...@gmail.com> wrote: > (Sorry if you get this twice, Ertugrul; and if I reply to top. I'm > stuck with the gmail interface and I'm not used to it.) > > On Thu, Apr 28, 2011 at 11:27 AM, Ertugrul Soeylemez <e...@ertes.de> wrote: >> I don't see any problem with this. Although I usually have a bottom-up >> approach, so I don't do this too often, it doesn't hurt, when I have to. > > I do. It's low tech and inconvenient. > > Whenever I program in Haskell, I miss Agda's editing features, where I > can write: > > foo : Signature > foo x y z = ? > > Then compile the file. The ? stands in for a term of any type, and > becomes a 'hole' in my code. The editing environment will then tell me > what type of term I have to fill into the hole, and give me > information on what is available in the scope. Then I can write: > > foo x y z = { partialImpl ? ? } > > and execute another command. The compiler will make sure that > 'partialImpl ? ?' has the right type to fill in the hole (with ?s > again standing in for terms of arbitrary type). If the type checking > goes through, it expands into: > > foo x y z = partialImpl { } { } > > and the process repeats until my function is completely written. And > of course, let's not forget the command for automatically going from: > > foo x y z = { x } > > to > > foo Con1 y z = { } > foo Con2 y z = { } > foo Con3 y z = { } > ... > > I don't think there's anything particularly Agda-specific to the > above. In fact, the inference required should be easier with > Haskell/GHC. Features like this would be pretty killer to have for > Haskell development; then I wouldn't have to prototype in Agda. :) > > -- Dan > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Regards, Austin _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
