Comments on current TypeHoles implementation

[Nicolas Frisby]

tl;wr Variables and holes should have disparate syntax, so that code
is easy to locally parse.

Simon, your proposal is very crisp from the GHC implementor's
perspective, but I think it might be harmful from the user's
perspective.

My premise is that free variables — which are normally fatal — should
never be conflated with anything else, regardless of the
circumstances. Similarly, I'd like holes to remain a unique notion; I
don't want (as a GHC user) to think of them as a special case of
anything else.

Also, the scoping of variables versus holes — lexical versus global,
if I understand correctly — seem disparate enough to me that reusing
the complicated one for the simpler one seems dangerously clever.

For example, assuming that -XTypeHoles is on, "_foo" in one context is
a hole and "_foo" in another context isn't, depending on what's in
scope (eg the _foo record selector).

If variables and holes do end up conflated in this way, then my above
observations boil down to this: we should provide messages that make
it very difficult for the accidental creation of a hole to go
unnoticed.

Is the principal motivation for the reuse of the variable machinery in
the implementation of holes to avoid a separate syntactic form for
named holes?

Thanks for working on this exciting feature!

On Thu, Oct 4, 2012 at 4:40 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> There is also the small matter, in this example, of distinguishing which `_'
> is which. The description works, but you have to think about it. I don't
> have an immediate and simple solution to this. Perhaps the addition of
> unique labels (e.g. _$1 _$2). But this is not a major problem. It can even
> wait until some future development/expansion on TypeHoles.
>
>
>
> I have a proposal.  Someone has already suggested on
> hackage.haskell.org/trac/ghc/ticket/5910 that an un-bound variable behaves
> like a hole.  Thus, if you say
>
>
>
>           f x = y
>
> GHC says “Error: y is not in scope”.  But (idea) with -XTypeHoles
>
>
>
> f x = y
>
> might generate
>
> 1.   (renamer) Warning: y is not in scope
>
> 2.   (type) Error: Hole “y” has type....
>
> So that’s like a named hole, in effect.
>
>
>
> If you say
>
>    f x = 4
>
> GHC warns about the unused binding for x.  But if you say
>
>    f _x = 4
>
> the unused-binding warning is suppressed.  So (idea) if you say
>
>           f x = _y
>
> maybe we can suppress warning (1).  And, voila, named holes.
>
>
>
> Moreover if you add –fdefer-type-errors you can keep going and run the
> program.
>
>
>
> Any comments?  This is pretty easy to do.
>
>
>
> (I’m unhappy that –XTypeHoles is a language pragma while –fdefer-type-errors
> is a compiler flag.  Maybe we should have –XDeferTypeErrors?)
>
>
>
> Simon
>
>
>
>
>
>
>
> From: sean.leather at gmail.com [mailto:sean.leather at gmail.com] On Behalf Of
> Sean Leather
> Sent: 03 October 2012 16:45
> To: Simon Peyton-Jones
> Cc: GHC Users List; Thijs Alkemade
> Subject: Comments on current TypeHoles implementation
>
>
>
> Hi Simon,
>
>
>
> Thanks for all your work in getting TypeHoles into HEAD. We really
> appreciate it.
>
>
>
> I was playing around with HEAD today and wanted to share a few observations.
>
>
>
> (1) One of the ideas we had was that a hole `_' would be like `undefined'
> but with information about the type and bindings. But in the current
> version, there doesn't appear to be that connection. This mainly applies to
> ambiguous type variables.
>
>
>
> Consider:
>
>> f = show _
>
> The hole has type a0.
>
>
>
> But with
>
>> f = show undefined
>
> there is a type error because a0 is ambiguous.
>
>
>
> We were thinking that it would be better to report the ambiguous type
> variable first, rather than the hole. In that case, tou can use
> -fdefer-type-errors to defer the error. Currently, you don't have that
> option. I can see the argument either way, however, and I'm not sure which
> is better.
>
>
>
> (2) There is a strange case where an error is not reported for a missing
> type class instance, even though there is no (apparent) relation between the
> missing instance and the hole. (This also relates to the connection to
> `undefined', but less directly.)
>
>
>
> We have the following declaration:
>
>> data T = T Int {- no Show instance -}
>
>
>
> With a hole in the field
>
>> g = show (T _)
>
> we get a message that the hole has type Int.
>
>
>
> With
>
>> g = show (T undefined)
>
> we get an error for the missing instance of `Show T'.
>
>
>
> (3) In GHCi, I see that the type of the hole now defaults. This is not
> necessarily bad, though it's maybe not as useful as it could be.
>
>
>
> ghci> :t show _
>
> reports that the hole has type ().
>
>
>
> (4) In GHCi, sometimes a hole throws an exception, and sometimes it does
> not.
>
>
>
> ghci> show _
>
> throws an exception with the hole warning message
>
>
>
> ghci> show (T _)
>
> and
>
> ghci> _ + 42
>
> cause GHCi to panic.
>
>
>
> (5) There are some places where unnecessary parentheses are used when
> pretty-printing the code:
>
>
>
> ghci> :t _ _
>
>
>
> <interactive>:1:1: Warning:
>
>     Found hole `_' with type t0 -> t
>
>     Where: `t0' is a free type variable
>
>            `t' is a rigid type variable bound by
>
>                the inferred type of it :: t at Top level
>
>     In the expression: _
>
>     In the expression: _ (_)
>
>
>
> <interactive>:1:3: Warning:
>
>     Found hole `_' with type t0
>
>     Where: `t0' is a free type variable
>
>     In the first argument of `_', namely `_'
>
>     In the expression: _ (_)
>
> _ _ :: t
>
>
>
> The argument `_' does not need to be printed as `(_)'.
>
>
>
> There is also the small matter, in this example, of distinguishing which `_'
> is which. The description works, but you have to think about it. I don't
> have an immediate and simple solution to this. Perhaps the addition of
> unique labels (e.g. _$1 _$2). But this is not a major problem. It can even
> wait until some future development/expansion on TypeHoles.
>
>
>
> Regards,
>
> Sean
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>