Holes in GHC

[Thijs Alkemade]

On Thu, Jan 26, 2012 at 5:10 PM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
>
> ...
>
> To me it looks like you get exactly the info that (I think) you want, and moreover you can do that without changing the type inference engine at all.
>
> Simon


On Thu, Jan 26, 2012 at 5:26 PM, Twan van Laarhoven <twanvl at gmail.com> wrote:
>
>
> You can do something similar right now with implicit parameters:
>
>   ...
>
> Twan
>
>

Thanks for your feedback.

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. When starting with Haskell, at least in my experience,
it happens lot that you have an idea about what you need to write, but
there are some parts in the expression you're working on you don't
know yet. For example, you might have a function you want to call, but
some arguments you don't know yet how to supply. You can put
`undefined` in those places, and after that it compiles (and maybe if
you're lucky it will even run), but that will not help to figure out
what the correct thing to put there is.

This is where you would want to use a hole. Just like undefined, it
has type `a`, so it can be used anywhere (and when compiling, we
intend to turn it into an exception too), but the difference with
undefined is that after the typechecking has succeeded, you get a list
of your holes, with the type that was inferred for them, as a sort of
todo-list.

So there are certainly ways to figure out this information right now,
but the goal is to use it as feedback to the user when writing code.
Yes, it's possible to translate the expression by changing holes into
arguments of a function, but that might be problematic when that
expression is part of a module, as to properly typecheck that
expression the whole module needs to be typechecked. I have not used
them myself, but I think people learning Haskell will easily end up
shooting themselves in the foot with implicit parameters.

A more general, but different, way to achieve this goal we are
considering is: being able to use the typechecker to get more than
just the final type of an expression, but also the types of certain
subexpressions. Imagine being able to annotate an expression (for
example, with certain brackets), to say "typecheck everything, and
after that, also show me the type of this part".


As an update to my problem with Any *: I think I've found the cause.
The holes were inferred independently, not all of them at once (they
are now all passed as name_taus to simplifyInfer), and this was
happening after zonkTopDecls was already done, so all unbound type
variables had already been zapped to Any * (as that uses
emptyZonkEnv).

Regards,
Thijs Alkemade