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