Comments on current TypeHoles implementation

[Roman Cheplyaka]

Sounds cool. I would also expect that if you have several occurences of
the same unbound identifier, then it gets a unified type.

I guess this is something you can get currently by creating a top-level
declaration

  foo = _

and then using foo in several places.

* Simon Peyton-Jones <simonpj at microsoft.com> [2012-10-04 09:40:02+0000]
> 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