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://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