Comments on current TypeHoles implementation

[Simon Marlow]

On 04/10/2012 10:40, Simon Peyton-Jones wrote:

> 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.

It's a great idea.  I suggest that we have a separate flag that controls 
whether an unbound variable results in a warning or an error, rather 
than piggybacking on -fdefer-type-errors.  Perhaps 
-fdefer-unbound-errors or something.

What I'm aiming at is that eventually we can have -fdefer-errors that 
expands to -fdefer-type-errors, -fdefer-unbound-errors, 
-fdefer-parse-errors, etc.

Cheers,
	Simon


> (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
>