[Haskell-cafe] Python is lazier than Haskell

[austin seipp]

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.doel at 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 <es at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Regards,
Austin