On Thu, Jan 26, 2012 at 2:36 PM, Simon Peyton-Jones
| > 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.