Holes in GHC

[Dan Doel]

On Thu, Jan 26, 2012 at 2:36 PM, Simon Peyton-Jones
<simonpj at microsoft.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.
>
> My question remains: what is the feature?   Agda has a sophisticated IDE; is that a key part of "the feature".  I expect so.

The Agda piece of the feature is support for keeping a type checker
running continuously, which has the ability to type check expressions
with holes, like:

    foo { }0 bar baz { }1

and can be queried for the type of expression that must be put into
the holes to make them type check, a list of all the variables in
scope at each hole together with their types, and the ability to type
check expressions against the necessary type for each hole without
rechecking the entire file (at least in the Agda case, checking the
part can be much faster than checking the whole; perhaps it'd matter
less in GHC). It probably must also be possible to tell the system
you're filling in a hole, because that might refine the type of the
other holes.

The rest is an emacs mode that interacts with the running type checker
appropriately.

Another view might be that the holes allow you to capture and interact
with contexts in the middle of type checking. A hole captures the
continuation, and then proceeds as if successful for any type, but the
continuation may be queried for the above information. Then you can
call the continuation to fill in the holes (possibly with expressions
having their own holes). But I'm not going to suggest that's a
feasible way to implement it.

The support of the compiler is necessary before you can build any
editor making use of it, though.