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
