Holes in GHC
wren ng thornton
wren at freegeek.org
Fri Jan 27 04:18:44 CET 2012
On 1/26/12 1:30 PM, Dan Doel wrote:
> On Thu, Jan 26, 2012 at 12:45 PM, Thijs Alkemade
> <thijsalkemade at gmail.com> wrote:
>> Let me try to describe the goal better. The intended users are people
>> new to Haskell or people working with existing code they are not
>> familiar with.
>
> Also me. I want this feature. It pretty much single handedly makes
> prototyping things in Agda and then porting them to Haskell a better
> experience than writing them straight in Haskell to begin with. I can
> partially implement functions and get feedback on what I need to
> provide and what is available, add candidate terms, have them type
> checked and filled in if they work. Etc.
>
> It's significantly better than any Haskell editor I'm aware of, and
> adding undefined or ?foo and poking at things in ghci isn't
> comparable.
Ditto. I've long wished for holes and sheds in Haskell. I do a lot of my
programming in an interactive bric-a-brac manner. And ever since I've
started hacking with Coq and Agda ---even more than the dependent
types--- this sort of interactivity has become a must-have feature.
Just think about how having a REPL makes life so much nicer than going
through the build cycle every time you change something. Having holes
and sheds is like making the same leap in utility and productivity,
except that we're making the leap from where REPLs leave off.
--
Live well,
~wren
More information about the Glasgow-haskell-users
mailing list