TypeHoles behaviour

[Krzysztof Gogolewski]

I have also seen this behaviour and support the change.
-KG

2013/8/27 Austin Seipp <aseipp at pobox.com>

> 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
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130827/1458a6cf/attachment.htm>