Comments on current TypeHoles implementation

[Roman Cheplyaka]

I don't see why it is an issue. You should never encounter holes in the
released code. The only source of holes should be stuff that you just
wrote. With this proposal not only you get an error for the unbound
variable (as you'd get before), but GHC even tells you the type of a
thing that you should plug there!

Roman

* Nicolas Frisby <nicolas.frisby at gmail.com> [2012-10-04 12:09:24-0500]
> 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
> >
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users