TypeHoles behaviour

[Austin Seipp]

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
<simonpj at 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-
> | 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
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



-- 
Regards,
Austin - PGP: 4096R/0x91384671