TypeHoles behaviour
Nicolas Frisby
nicolas.frisby at gmail.com
Tue Aug 27 18:29:19 CEST 2013
I also say +1, but I am concerned about always showing all the bindings.
In my experiences over the years, the times when holes seem they would have
been most helpful is when the bindings were numerous and had large and
complicated types. Dumping all of the bindings in that sort of scenario
would generate a lot of output to sift through.
(Admittedly, I was doing my best Oleg impersonation at the time -- ie
complicated type-level programming -- so this is probably relatively
uncommon.)
I think I nice solution would be a line or two at the top of the message
indicating "which of the following bindings are most likely relevant"? I
don't know how intended the current behavior was, but perhaps it could be
distilled into a heuristic to guess those relevant bindings.
On Tue, Aug 27, 2013 at 10:24 AM, Krzysztof Gogolewski <
krz.gogolewski at gmail.com> wrote:
> 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
>>
>
>
> _______________________________________________
> 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/84f95d03/attachment.htm>
More information about the Glasgow-haskell-users
mailing list