Comments on current TypeHoles implementation

[Edward Kmett]

I really like this proposal.

-Edward

On Thu, Oct 4, 2012 at 5: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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121004/5ebdd43f/attachment.htm>