TypeHoles behaviour
Simon PeytonJones
simonpj at microsoft.com
Tue Aug 27 10:17:37 CEST 2013
I'm sympathetic to Andres's point here. Easy to implement. Any objections?
Simon
 Original Message
 From: Glasgowhaskellusers [mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of Andres Löh
 Sent: 23 August 2013 21:02
 To: glasgowhaskellusers at 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 nonempty. 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
 WellTyped LLP, http://www.welltyped.com

 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list