Type checking of partial programs

[Jean-Philippe Bernardy]

2008/3/20 ac <quuxman at gmail.com>:
> Is anybody interested in working on this? This is a project I've been
> interested in for some time, but recognize I probably need some guidance
> before I go off and start hacking on it. As dcoutts pointed out on
> #haskell-soc, this may be of particular interest to people working on yi and
> HaRe. Other interesting and related projects include parsing partial
> programs to insert "placeholders" in appropriate places. An example of a
> partial program could be:
>
> foo :: [Foo] -> <placeholder 1>
> foo xs = map <placeholder 2> xs
>
> What are the possible type signatures for placeholder 1 and the possible
> expressions for placeholder 2?
>

(I'm maintainer of Yi)

It turns out that <placeholder 2> already exists, an is called undefined :)
It would be nice if GHC API could provide (maybe it does already) a
way to retrieve the type of an expression "after unification". That
would more or less solve this case.

When it comes to <placeholder 1>, I guess one could use the same approach.
You would then get the kind of the type.

Finding possible expressions is a much harder problem, but in the case
of haskell types
that might be more or less manageable.

If you implement the above in GHC API, they would be usable in Yi indeed.
At the moment we only have a beginning of integration with GHC API,
but is quite rudimentary. If you (or somebody) wishes to work on that
kind of a project I'll be ready to mentor it. I don't think I'm comfortable
enough with GHC to mentor your particular idea though.

I should also mention that a good example of what this could
look like is Agda2 (and its siblings) ; where the "placeholder" is
fundamental to interactive proof/program construction.

Cheers,
JP.