Re: TypeHoles behaviour

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.gogolewski@gmail.com> wrote:

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

2013/8/27 Austin Seipp

...

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

...

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

Simon

| -----Original Message----- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | bounces@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

On Tue, Aug 27, 2013 at 3:17 AM, Simon Peyton-Jones wrote: 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

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