TypeHoles behaviour

[Simon Peyton-Jones]

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 at haskell.org] On Behalf Of Andres Löh
| Sent: 23 August 2013 21:02
| To: glasgow-haskell-users 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 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users