RE: TypeHoles behaviour

[Simon Peyton-Jones]

OK I've done this.  Patch will land shortly.

Thank you for a well-articulated message.

Simon

| -Original Message-
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Andres Löh
| Sent: 23 August 2013 21:02
| To: glasgow-haskell-users@haskell.org
| Subject: TypeHoles behaviour
| 
| Hi.
| 
| I've just started playing with TypeHoles. (I'm writing some Haskell
| course
| materials and would like to use them from the very beginning once they
| become
| available.)
| 
| However, I must say that I don't understand the current notion of
| relevance
| that seems to determine whether local bindings are included or not.
| 
| The current rule seems to be that bindings are included only if the
| intersection between the type variables their types involve and the type
| variables in the whole is non-empty. However, I think this is confusing.
| 
| Let's look at a number of examples:
| 
|  f1 :: Int - Int - Int
|  f1 x y = _
| 
| Found hole ‛_’ with type: Int
| In the expression: _
| In an equation for ‛f1’: f1 x y = _
| 
| No bindings are shown.
| 
|  f2 :: a - a - a
|  f2 x y = _
| 
| Found hole ‛_’ with type: a
| Where: ‛a’ is a rigid type variable bound by
|the type signature for f2 :: a - a - a at List.hs:6:7
| Relevant bindings include
|   f2 :: a - a - a (bound at List.hs:7:1)
|   x :: a (bound at List.hs:7:4)
|   y :: a (bound at List.hs:7:6)
| In the expression: _
| In an equation for ‛f2’: f2 x y = _
| 
| Both x and y (and f2) are shown. Why should this be treated differently
| from f1?
| 
|  f3 :: Int - (Int - a) - a
|  f3 x y = _
| 
| Found hole ‛_’ with type: a
| Where: ‛a’ is a rigid type variable bound by
|the type signature for f3 :: Int - (Int - a) - a at
| List.hs:9:7
| Relevant bindings include
|   f3 :: Int - (Int - a) - a (bound at List.hs:10:1)
|   y :: Int - a (bound at List.hs:10:6)
| In the expression: _
| In an equation for ‛f3’: f3 x y = _
| 
| Here, y is shown, but x isn't, even though y has to be applied to an Int
| in order to produce an a. Of course, it's possible to obtain an Int from
| elsewhere ...
| 
| f4 :: a - (a - b) - b
| f4 x y = _
| 
| Found hole ‛_’ with type: b
| Where: ‛b’ is a rigid type variable bound by
|the type signature for f4 :: a - (a - b) - b at
| List.hs:12:7
| Relevant bindings include
|   f4 :: a - (a - b) - b (bound at List.hs:13:1)
|   y :: a - b (bound at List.hs:13:6)
| In the expression: _
| In an equation for ‛f4’: f4 x y = _
| 
| Again, only y is shown, and x isn't. But here, the only sane way of
| filling
| the hole is by applying y to x. Why is one more relevant than the
| other?
| 
| f5 x y = _
| 
| Found hole ‛_’ with type: t2
| Where: ‛t2’ is a rigid type variable bound by
| the inferred type of f5 :: t - t1 - t2 at List.hs:15:1
| Relevant bindings include
|   f5 :: t - t1 - t2 (bound at List.hs:15:1)
| In the expression: _
| In an equation for ‛f5’: f5 x y = _
| 
| Neither x and y are included without a type signature. Even though all
| of
| the above types are admissible, which would convince GHC that one or
| even
| all may be relevant.
| 
| IMHO, this isn't worth it. It's a confusing rule. Just include all local
| bindings
| in the output, always. That's potentially verbose, but easy to
| understand. It's
| also potentially really helpful, because it trains beginning programmers
| to see
| what types local variables get, and it's a way to obtain complex types
| of locally
| bound variables for expert programmers. It's also much easier to
| explain. It
| should be easier to implement, too :)
| 
| Could we please change it?
| 
| Cheers,
|   Andres
| 
| --
| Andres Löh, Haskell Consultant
| Well-Typed LLP, http://www.well-typed.com
| 
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: TypeHoles behaviour

[Simon Peyton-Jones]

I'm sympathetic to Andres's point here. Easy to implement. Any objections?

Simon

| -Original Message-
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Andres Löh
| Sent: 23 August 2013 21:02
| To: glasgow-haskell-users@haskell.org
| Subject: TypeHoles behaviour
| 
| Hi.
| 
| I've just started playing with TypeHoles. (I'm writing some Haskell
| course
| materials and would like to use them from the very beginning once they
| become
| available.)
| 
| However, I must say that I don't understand the current notion of
| relevance
| that seems to determine whether local bindings are included or not.
| 
| The current rule seems to be that bindings are included only if the
| intersection between the type variables their types involve and the type
| variables in the whole is non-empty. However, I think this is confusing.
| 
| Let's look at a number of examples:
| 
|  f1 :: Int - Int - Int
|  f1 x y = _
| 
| Found hole ‛_’ with type: Int
| In the expression: _
| In an equation for ‛f1’: f1 x y = _
| 
| No bindings are shown.
| 
|  f2 :: a - a - a
|  f2 x y = _
| 
| Found hole ‛_’ with type: a
| Where: ‛a’ is a rigid type variable bound by
|the type signature for f2 :: a - a - a at List.hs:6:7
| Relevant bindings include
|   f2 :: a - a - a (bound at List.hs:7:1)
|   x :: a (bound at List.hs:7:4)
|   y :: a (bound at List.hs:7:6)
| In the expression: _
| In an equation for ‛f2’: f2 x y = _
| 
| Both x and y (and f2) are shown. Why should this be treated differently
| from f1?
| 
|  f3 :: Int - (Int - a) - a
|  f3 x y = _
| 
| Found hole ‛_’ with type: a
| Where: ‛a’ is a rigid type variable bound by
|the type signature for f3 :: Int - (Int - a) - a at
| List.hs:9:7
| Relevant bindings include
|   f3 :: Int - (Int - a) - a (bound at List.hs:10:1)
|   y :: Int - a (bound at List.hs:10:6)
| In the expression: _
| In an equation for ‛f3’: f3 x y = _
| 
| Here, y is shown, but x isn't, even though y has to be applied to an Int
| in order to produce an a. Of course, it's possible to obtain an Int from
| elsewhere ...
| 
| f4 :: a - (a - b) - b
| f4 x y = _
| 
| Found hole ‛_’ with type: b
| Where: ‛b’ is a rigid type variable bound by
|the type signature for f4 :: a - (a - b) - b at
| List.hs:12:7
| Relevant bindings include
|   f4 :: a - (a - b) - b (bound at List.hs:13:1)
|   y :: a - b (bound at List.hs:13:6)
| In the expression: _
| In an equation for ‛f4’: f4 x y = _
| 
| Again, only y is shown, and x isn't. But here, the only sane way of
| filling
| the hole is by applying y to x. Why is one more relevant than the
| other?
| 
| f5 x y = _
| 
| Found hole ‛_’ with type: t2
| Where: ‛t2’ is a rigid type variable bound by
| the inferred type of f5 :: t - t1 - t2 at List.hs:15:1
| Relevant bindings include
|   f5 :: t - t1 - t2 (bound at List.hs:15:1)
| In the expression: _
| In an equation for ‛f5’: f5 x y = _
| 
| Neither x and y are included without a type signature. Even though all
| of
| the above types are admissible, which would convince GHC that one or
| even
| all may be relevant.
| 
| IMHO, this isn't worth it. It's a confusing rule. Just include all local
| bindings
| in the output, always. That's potentially verbose, but easy to
| understand. It's
| also potentially really helpful, because it trains beginning programmers
| to see
| what types local variables get, and it's a way to obtain complex types
| of locally
| bound variables for expert programmers. It's also much easier to
| explain. It
| should be easier to implement, too :)
| 
| Could we please change it?
| 
| Cheers,
|   Andres
| 
| --
| Andres Löh, Haskell Consultant
| Well-Typed LLP, http://www.well-typed.com
| 
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: TypeHoles behaviour

[Austin Seipp]

I'm +1 on changing the behavior. I find it probably the most confusing
aspect of using TypeHoles, which is otherwise great.

On Tue, Aug 27, 2013 at 3:17 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
 I'm sympathetic to Andres's point here. Easy to implement. Any objections?

 Simon

 | -Original Message-
 | From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
 | boun...@haskell.org] On Behalf Of Andres Löh
 | Sent: 23 August 2013 21:02
 | To: glasgow-haskell-users@haskell.org
 | Subject: TypeHoles behaviour
 |
 | Hi.
 |
 | I've just started playing with TypeHoles. (I'm writing some Haskell
 | course
 | materials and would like to use them from the very beginning once they
 | become
 | available.)
 |
 | However, I must say that I don't understand the current notion of
 | relevance
 | that seems to determine whether local bindings are included or not.
 |
 | The current rule seems to be that bindings are included only if the
 | intersection between the type variables their types involve and the type
 | variables in the whole is non-empty. However, I think this is confusing.
 |
 | Let's look at a number of examples:
 |
 |  f1 :: Int - Int - Int
 |  f1 x y = _
 |
 | Found hole ‛_’ with type: Int
 | In the expression: _
 | In an equation for ‛f1’: f1 x y = _
 |
 | No bindings are shown.
 |
 |  f2 :: a - a - a
 |  f2 x y = _
 |
 | Found hole ‛_’ with type: a
 | Where: ‛a’ is a rigid type variable bound by
 |the type signature for f2 :: a - a - a at List.hs:6:7
 | Relevant bindings include
 |   f2 :: a - a - a (bound at List.hs:7:1)
 |   x :: a (bound at List.hs:7:4)
 |   y :: a (bound at List.hs:7:6)
 | In the expression: _
 | In an equation for ‛f2’: f2 x y = _
 |
 | Both x and y (and f2) are shown. Why should this be treated differently
 | from f1?
 |
 |  f3 :: Int - (Int - a) - a
 |  f3 x y = _
 |
 | Found hole ‛_’ with type: a
 | Where: ‛a’ is a rigid type variable bound by
 |the type signature for f3 :: Int - (Int - a) - a at
 | List.hs:9:7
 | Relevant bindings include
 |   f3 :: Int - (Int - a) - a (bound at List.hs:10:1)
 |   y :: Int - a (bound at List.hs:10:6)
 | In the expression: _
 | In an equation for ‛f3’: f3 x y = _
 |
 | Here, y is shown, but x isn't, even though y has to be applied to an Int
 | in order to produce an a. Of course, it's possible to obtain an Int from
 | elsewhere ...
 |
 | f4 :: a - (a - b) - b
 | f4 x y = _
 |
 | Found hole ‛_’ with type: b
 | Where: ‛b’ is a rigid type variable bound by
 |the type signature for f4 :: a - (a - b) - b at
 | List.hs:12:7
 | Relevant bindings include
 |   f4 :: a - (a - b) - b (bound at List.hs:13:1)
 |   y :: a - b (bound at List.hs:13:6)
 | In the expression: _
 | In an equation for ‛f4’: f4 x y = _
 |
 | Again, only y is shown, and x isn't. But here, the only sane way of
 | filling
 | the hole is by applying y to x. Why is one more relevant than the
 | other?
 |
 | f5 x y = _
 |
 | Found hole ‛_’ with type: t2
 | Where: ‛t2’ is a rigid type variable bound by
 | the inferred type of f5 :: t - t1 - t2 at List.hs:15:1
 | Relevant bindings include
 |   f5 :: t - t1 - t2 (bound at List.hs:15:1)
 | In the expression: _
 | In an equation for ‛f5’: f5 x y = _
 |
 | Neither x and y are included without a type signature. Even though all
 | of
 | the above types are admissible, which would convince GHC that one or
 | even
 | all may be relevant.
 |
 | IMHO, this isn't worth it. It's a confusing rule. Just include all local
 | bindings
 | in the output, always. That's potentially verbose, but easy to
 | understand. It's
 | also potentially really helpful, because it trains beginning programmers
 | to see
 | what types local variables get, and it's a way to obtain complex types
 | of locally
 | bound variables for expert programmers. It's also much easier to
 | explain. It
 | should be easier to implement, too :)
 |
 | Could we please change it?
 |
 | Cheers,
 |   Andres
 |
 | --
 | Andres Löh, Haskell Consultant
 | Well-Typed LLP, http://www.well-typed.com
 |
 | ___
 | Glasgow-haskell-users mailing list
 | Glasgow-haskell-users@haskell.org
 | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
 ___
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.org
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



-- 
Regards,
Austin - PGP: 4096R/0x91384671

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: TypeHoles behaviour

[Krzysztof Gogolewski]

I have also seen this behaviour and support the change.
-KG

2013/8/27 Austin Seipp ase...@pobox.com

 I'm +1 on changing the behavior. I find it probably the most confusing
 aspect of using TypeHoles, which is otherwise great.

 On Tue, Aug 27, 2013 at 3:17 AM, Simon Peyton-Jones
 simo...@microsoft.com wrote:
  I'm sympathetic to Andres's point here. Easy to implement. Any
 objections?
 
  Simon
 
  | -Original Message-
  | From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
  | boun...@haskell.org] On Behalf Of Andres Löh
  | Sent: 23 August 2013 21:02
  | To: glasgow-haskell-users@haskell.org
  | Subject: TypeHoles behaviour
  |
  | Hi.
  |
  | I've just started playing with TypeHoles. (I'm writing some Haskell
  | course
  | materials and would like to use them from the very beginning once they
  | become
  | available.)
  |
  | However, I must say that I don't understand the current notion of
  | relevance
  | that seems to determine whether local bindings are included or not.
  |
  | The current rule seems to be that bindings are included only if the
  | intersection between the type variables their types involve and the
 type
  | variables in the whole is non-empty. However, I think this is
 confusing.
  |
  | Let's look at a number of examples:
  |
  |  f1 :: Int - Int - Int
  |  f1 x y = _
  |
  | Found hole '_' with type: Int
  | In the expression: _
  | In an equation for 'f1': f1 x y = _
  |
  | No bindings are shown.
  |
  |  f2 :: a - a - a
  |  f2 x y = _
  |
  | Found hole '_' with type: a
  | Where: 'a' is a rigid type variable bound by
  |the type signature for f2 :: a - a - a at List.hs:6:7
  | Relevant bindings include
  |   f2 :: a - a - a (bound at List.hs:7:1)
  |   x :: a (bound at List.hs:7:4)
  |   y :: a (bound at List.hs:7:6)
  | In the expression: _
  | In an equation for 'f2': f2 x y = _
  |
  | Both x and y (and f2) are shown. Why should this be treated differently
  | from f1?
  |
  |  f3 :: Int - (Int - a) - a
  |  f3 x y = _
  |
  | Found hole '_' with type: a
  | Where: 'a' is a rigid type variable bound by
  |the type signature for f3 :: Int - (Int - a) - a at
  | List.hs:9:7
  | Relevant bindings include
  |   f3 :: Int - (Int - a) - a (bound at List.hs:10:1)
  |   y :: Int - a (bound at List.hs:10:6)
  | In the expression: _
  | In an equation for 'f3': f3 x y = _
  |
  | Here, y is shown, but x isn't, even though y has to be applied to an
 Int
  | in order to produce an a. Of course, it's possible to obtain an Int
 from
  | elsewhere ...
  |
  | f4 :: a - (a - b) - b
  | f4 x y = _
  |
  | Found hole '_' with type: b
  | Where: 'b' is a rigid type variable bound by
  |the type signature for f4 :: a - (a - b) - b at
  | List.hs:12:7
  | Relevant bindings include
  |   f4 :: a - (a - b) - b (bound at List.hs:13:1)
  |   y :: a - b (bound at List.hs:13:6)
  | In the expression: _
  | In an equation for 'f4': f4 x y = _
  |
  | Again, only y is shown, and x isn't. But here, the only sane way of
  | filling
  | the hole is by applying y to x. Why is one more relevant than the
  | other?
  |
  | f5 x y = _
  |
  | Found hole '_' with type: t2
  | Where: 't2' is a rigid type variable bound by
  | the inferred type of f5 :: t - t1 - t2 at
 List.hs:15:1
  | Relevant bindings include
  |   f5 :: t - t1 - t2 (bound at List.hs:15:1)
  | In the expression: _
  | In an equation for 'f5': f5 x y = _
  |
  | Neither x and y are included without a type signature. Even though all
  | of
  | the above types are admissible, which would convince GHC that one or
  | even
  | all may be relevant.
  |
  | IMHO, this isn't worth it. It's a confusing rule. Just include all
 local
  | bindings
  | in the output, always. That's potentially verbose, but easy to
  | understand. It's
  | also potentially really helpful, because it trains beginning
 programmers
  | to see
  | what types local variables get, and it's a way to obtain complex types
  | of locally
  | bound variables for expert programmers. It's also much easier to
  | explain. It
  | should be easier to implement, too :)
  |
  | Could we please change it?
  |
  | Cheers,
  |   Andres
  |
  | --
  | Andres Löh, Haskell Consultant
  | Well-Typed LLP, http://www.well-typed.com
  |
  | ___
  | Glasgow-haskell-users mailing list
  | Glasgow-haskell-users@haskell.org
  | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
  ___
  Glasgow-haskell-users mailing list
  Glasgow-haskell-users@haskell.org
  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



 --
 Regards,
 Austin - PGP: 4096R/0x91384671

 ___
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.org
 http

Re: TypeHoles behaviour

[Nicolas Frisby]

I also say +1, but I am concerned about always showing all the bindings.

In my experiences over the years, the times when holes seem they would have
been most helpful is when the bindings were numerous and had large and
complicated types. Dumping all of the bindings in that sort of scenario
would generate a lot of output to sift through.

(Admittedly, I was doing my best Oleg impersonation at the time -- ie
complicated type-level programming -- so this is probably relatively
uncommon.)

I think I nice solution would be a line or two at the top of the message
indicating which of the following bindings are most likely relevant? I
don't know how intended the current behavior was, but perhaps it could be
distilled into a heuristic to guess those relevant bindings.


On Tue, Aug 27, 2013 at 10:24 AM, Krzysztof Gogolewski 
krz.gogolew...@gmail.com wrote:

 I have also seen this behaviour and support the change.
 -KG

 2013/8/27 Austin Seipp ase...@pobox.com

 I'm +1 on changing the behavior. I find it probably the most confusing
 aspect of using TypeHoles, which is otherwise great.

 On Tue, Aug 27, 2013 at 3:17 AM, Simon Peyton-Jones
 simo...@microsoft.com wrote:
  I'm sympathetic to Andres's point here. Easy to implement. Any
 objections?
 
  Simon
 
  | -Original Message-
  | From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
  | boun...@haskell.org] On Behalf Of Andres Löh
  | Sent: 23 August 2013 21:02
  | To: glasgow-haskell-users@haskell.org
  | Subject: TypeHoles behaviour
  |
  | Hi.
  |
  | I've just started playing with TypeHoles. (I'm writing some Haskell
  | course
  | materials and would like to use them from the very beginning once they
  | become
  | available.)
  |
  | However, I must say that I don't understand the current notion of
  | relevance
  | that seems to determine whether local bindings are included or not.
  |
  | The current rule seems to be that bindings are included only if the
  | intersection between the type variables their types involve and the
 type
  | variables in the whole is non-empty. However, I think this is
 confusing.
  |
  | Let's look at a number of examples:
  |
  |  f1 :: Int - Int - Int
  |  f1 x y = _
  |
  | Found hole '_' with type: Int
  | In the expression: _
  | In an equation for 'f1': f1 x y = _
  |
  | No bindings are shown.
  |
  |  f2 :: a - a - a
  |  f2 x y = _
  |
  | Found hole '_' with type: a
  | Where: 'a' is a rigid type variable bound by
  |the type signature for f2 :: a - a - a at List.hs:6:7
  | Relevant bindings include
  |   f2 :: a - a - a (bound at List.hs:7:1)
  |   x :: a (bound at List.hs:7:4)
  |   y :: a (bound at List.hs:7:6)
  | In the expression: _
  | In an equation for 'f2': f2 x y = _
  |
  | Both x and y (and f2) are shown. Why should this be treated
 differently
  | from f1?
  |
  |  f3 :: Int - (Int - a) - a
  |  f3 x y = _
  |
  | Found hole '_' with type: a
  | Where: 'a' is a rigid type variable bound by
  |the type signature for f3 :: Int - (Int - a) - a at
  | List.hs:9:7
  | Relevant bindings include
  |   f3 :: Int - (Int - a) - a (bound at List.hs:10:1)
  |   y :: Int - a (bound at List.hs:10:6)
  | In the expression: _
  | In an equation for 'f3': f3 x y = _
  |
  | Here, y is shown, but x isn't, even though y has to be applied to an
 Int
  | in order to produce an a. Of course, it's possible to obtain an Int
 from
  | elsewhere ...
  |
  | f4 :: a - (a - b) - b
  | f4 x y = _
  |
  | Found hole '_' with type: b
  | Where: 'b' is a rigid type variable bound by
  |the type signature for f4 :: a - (a - b) - b at
  | List.hs:12:7
  | Relevant bindings include
  |   f4 :: a - (a - b) - b (bound at List.hs:13:1)
  |   y :: a - b (bound at List.hs:13:6)
  | In the expression: _
  | In an equation for 'f4': f4 x y = _
  |
  | Again, only y is shown, and x isn't. But here, the only sane way of
  | filling
  | the hole is by applying y to x. Why is one more relevant than the
  | other?
  |
  | f5 x y = _
  |
  | Found hole '_' with type: t2
  | Where: 't2' is a rigid type variable bound by
  | the inferred type of f5 :: t - t1 - t2 at
 List.hs:15:1
  | Relevant bindings include
  |   f5 :: t - t1 - t2 (bound at List.hs:15:1)
  | In the expression: _
  | In an equation for 'f5': f5 x y = _
  |
  | Neither x and y are included without a type signature. Even though all
  | of
  | the above types are admissible, which would convince GHC that one or
  | even
  | all may be relevant.
  |
  | IMHO, this isn't worth it. It's a confusing rule. Just include all
 local
  | bindings
  | in the output, always. That's potentially verbose, but easy to
  | understand. It's
  | also potentially really helpful, because it trains beginning
 programmers
  | to see
  | what types local variables get, and it's a way to obtain complex types