Sean Leather | 3 Oct 17:44 2012
Picon

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
Edward Kmett | 3 Oct 19:06 2012
Picon

Re: Comments on current TypeHoles implementation


On Wed, Oct 3, 2012 at 11:44 AM, Sean Leather <leather <at> cs.uu.nl> wrote:
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.
 
At least in the first case I would actually prefer it not to complain about the ambiguity. The point of putting the hole in is to figure out the type that something going into that location should have and what information I have available to use to plug that hole. 

An 'undefined' _is_ ambiguous, but _ is a placeholder for code that presumably will be valid when it gets expanded.

If I have to put a type annotation on it to avoid the compiler dumping out with an error about an ambiguous hole that would seem to me at least to largely defeat the very utility of holes. I would further suspect there are places where you'll be putting holes that have higher rank  types, and where undefined might complain.

I largely agree with but don't really have a deep opinion on the other issues you raised, though.

-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 4 Oct 11:33 2012
Picon

RE: Comments on current TypeHoles implementation

Thanks for all your work in getting TypeHoles into HEAD. We really appreciate it.

 

Great – maybe you can develop it further.

 

 

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

 

Yes; GHC classifies type errors into two groups:

·         insoluble (eg Int~Bool) are definitely wrong

·         unsolved (eg Eq a) might be ok if (say) the context changed

If there are any insolubles (anywhere), error messages about unsolved constraints are suppressed.  This is usually good; it focuses your attention on definite errors first.  Let’s call the suppressed errors “suppressed erorrs”.

 

Now, holes are classified as “insoluble” at the moment, and that’s why all other unsolved errors are suppressed.

 

 

At the moment, if you way –XTypeHoles you get only a warning even though it’s really an error.  Moreover it’s weird that the warning suppresses other error messages.

 

So I propose to change it so that –XTypeHoles gives an error message (for holes); and you can use –fdefer-type-errors to defer it.

 

In doing this I also realised that with –fdefer-type-errors you only get warnings for the things that would previously have been errors; you don’t get warnings for “supressed errors”.  And that’s arguably bad, since you don’t know about all the errors you are deferring to runtime.  So I’ve changed it so that with –fdefer-type-errors you get *all* errors as warnings (no supression).

 

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

 

You get this, which seems reasonable, no?  (I’ve changed the wording slightly.)

 

Foo.hs:5:12:

    Found hole `_' with type a0

    Where: `a0' is an ambiguous type variable

    In the first argument of `show', namely `_'

    In the expression: show _

    In an equation for `f': f x = show _

 

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

 

Yes... if there are insolubles around then doing defaulting isn’t going to help, and might confuse matters.  I’ll change that.

 

(5) There are some places where unnecessary parentheses are used when pretty-printing the code:

 

That’s easily fixed thanks.

 

I’ll think about GHCi separately.

 

Simon

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 4 Oct 11:40 2012
Picon

RE: Comments on current TypeHoles implementation

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
Roman Cheplyaka | 4 Oct 23:33 2012

Re: Comments on current TypeHoles implementation

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
Thijs Alkemade | 5 Oct 00:13 2012
Picon

Re: Comments on current TypeHoles implementation

On 4 okt. 2012, at 23:33, Roman Cheplyaka <roma <at> ro-che.info> wrote:

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

We have actually tried to do it this way for a pretty long time. But it's not as 
easy as it sounds. We were hoping to make all holes inside one module 
to be shared and get a unified type, but that turned out to not fit with our 
implementation of holes. Holes are treated as constraints, which apply to 
the type of one function, there's no such thing as a constraint for a whole 
module.

You can also not treat the holes as "fake" top level declarations:

> I guess this is something you can get currently by creating a top-level
> declaration
> 
>  foo = _
> 
> and then using foo in several places.

This example will just result in one hole with type "t". The call locations for 
`foo' have no influence on its type.

If we'd want holes to just be shared within one function, then that is pretty 
easy to do right now. We could turn the definition of a hole in HsExpr into 
`HsHole (Maybe RdrName)' (or whatever String-like type is most 
appropriate), in the renamer, change rnExpr for HsVars to return a hole 
when it can't find it, storing the original name. Then ensure holes with the 
same name interact properly (in canHole), and update the way they are 
printed.

Best regards,
Thijs
Simon Peyton-Jones | 5 Oct 09:14 2012
Picon

RE: Comments on current TypeHoles implementation

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

I thought about this, but I think not. Consider

f x1 = _y
g x2 = _y

Do you want _y and _y to be unified, so that f and g are no longer polymorphic?  I think not.  Any more than the "_"
holes we have now are unified.

| I guess this is something you can get currently by creating a top-level
| declaration
|   foo = _
| and then using foo in several places.

Yes. Or even _foo = _!

Simon
Roman Cheplyaka | 5 Oct 09:22 2012

Re: Comments on current TypeHoles implementation

* Simon Peyton-Jones <simonpj <at> microsoft.com> [2012-10-05 07:14:36+0000]
> | Sounds cool. I would also expect that if you have several occurences of
> | the same unbound identifier, then it gets a unified type.
> 
> I thought about this, but I think not. Consider
> 
> f x1 = _y
> g x2 = _y
> 
> Do you want _y and _y to be unified, so that f and g are no longer polymorphic?  I think not.  Any more than the "_"
holes we have now are unified.

Do you mean polymorphism in their argument? Why would it go away?

I would expect the functions to get types `a -> c` and `b -> c`
respectively, and `c` to be reported as the type of the hole.

Roman
Roman Cheplyaka | 5 Oct 09:24 2012

Re: Comments on current TypeHoles implementation

* Roman Cheplyaka <roma <at> ro-che.info> [2012-10-05 10:22:23+0300]
> * Simon Peyton-Jones <simonpj <at> microsoft.com> [2012-10-05 07:14:36+0000]
> > | Sounds cool. I would also expect that if you have several occurences of
> > | the same unbound identifier, then it gets a unified type.
> > 
> > I thought about this, but I think not. Consider
> > 
> > f x1 = _y
> > g x2 = _y
> > 
> > Do you want _y and _y to be unified, so that f and g are no longer polymorphic?  I think not.  Any more than the
"_" holes we have now are unified.
> 
> Do you mean polymorphism in their argument? Why would it go away?
> 
> I would expect the functions to get types `a -> c` and `b -> c`
> respectively, and `c` to be reported as the type of the hole.

Ah, I see. Since `c` is universally quantified, it means different
things for f and g. Good point.

Roman
Edward Kmett | 4 Oct 16:03 2012
Picon

Re: Comments on current TypeHoles implementation

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


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Nicolas Frisby | 4 Oct 19:09 2012
Picon

Re: Comments on current TypeHoles implementation

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
>
Roman Cheplyaka | 4 Oct 23:28 2012

Re: Comments on current TypeHoles implementation

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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Nicolas Frisby | 5 Oct 00:17 2012
Picon

Re: Comments on current TypeHoles implementation

On Thu, Oct 4, 2012 at 4:28 PM, Roman Cheplyaka <roma <at> ro-che.info> wrote:
> 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
>

That's a good point.

Upon reflection, my concerns are motivated by how I expect I'll be
using holes. I anticipate that will be for dealing with complex code,
and that's when I really don't want any other surprises.
Simon Marlow | 5 Oct 15:57 2012
Picon

Re: Comments on current TypeHoles implementation


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
>

Gmane