Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Carter Schonwald]

I mean for the fixed / new one I’m proposing :)

On Sun, May 20, 2018 at 8:21 PM Carter Schonwald 
wrote:

> No. I’m saying make same variables get the parent quantified, even if it’s
> implicit.
>
> Breaking changes are ok if they make things better.
>
> Measuring impact really comes down to making the patch and measuring. It
> will be an easy to fix breaking change and my experience has been that
> teams in an industrial context are a ok with none silent breaking changes.
> This would be very easy to catch :)
>
> On the pedagogy side it actually makes learning simpler afaict :)
>
> On Sun, May 20, 2018 at 8:03 PM Anthony Clayden <
> anthony_clay...@clear.net.nz> wrote:
>
>> On Mon, 21 May 2018 at 11:23 AM, Carter Schonwald <
>> redir...@vodafone.co.nz> wrote:
>>
>>> indeed .. and we can reasonably say "lets deal with the bandaid in one
>>> go by cleaning it up  in the next standard"
>>>
>>
>> Thanks Carter/Brandon, the reason for asking how we should go about the
>> discussion was exactly: where/how are we going to maximise the chance of
>> finding out what code is out there, and how disruptive any 'clean up' might
>> be?
>>
>> Ghc has occasionally made breaking releases (not saying that's what we
>> want to do), usually with some advance warning/deprecation period. And
>> generally the Haskell community has accommodated that with understanding of
>> the decision, to fix their code.
>>
>>
>>
>>> so what would the next gen look like?
>>>
>>> eg: fresh variables get the usual implicit forall at the front of the
>>> type, and everything else either needs an explicit quantifier OR it refers
>>> to the outer implicit quantified variable?
>>>
>>
>> I wanted to avoid discussing 'next gen' in possibly-obscure/write-only
>> mailing lists; and preferably get the discussion where posterity can see
>> the reasoning/examination of options.
>>
>> "fresh variables get the usual implicit forall" is what happens now.
>> (It's just that the User Guide explains it really badly -- I'm trying to
>> fix that separately https://ghc.haskell.org/trac/ghc/ticket/15146 .) If
>> the outer variable(s) are not explicitly forall-quantified, then even
>> same-named variables count as fresh. IOW merely putting a `forall` can
>> change the meaning of a program -- that's what causes the most confusion
>> (judging by SO).
>>
>> The exception is variables bound in a pattern signature for an
>> existentially-quantified data constructor: they *must* be fresh. This is
>> hard for a reader to follow because the pattern signature with data
>> constructor looks the same whether or not the constructor is
>> existentially-quantified. What's worse a constructor might have a mix of
>> existential and universal variables.
>>
>> AntC
>>
>>
>>> On Sat, May 19, 2018 at 2:56 PM, Brandon Allbery 
>>> wrote:
>>>
 On Sat, May 19, 2018 at 7:32 AM, Anthony Clayden <
 anthony_clay...@clear.net.nz> wrote:

> So the explanation I've seen for the current design is it was 
> deliberately idiosyncratic, to minimise any disruption to existing code. 
> Then I'm asking whether any of that code is still around? If not/if it's 
> been re-factored to use ScopedTypeVariables, then any tweak to the design 
> could have a freer hand.
>
>
 The reason there's no discussion about that is that nobody here has the
 ability to go hunt down every last piece of code in every public or private
 (think Standard Chartered, Facebook, etc.) code base and its current owner,
 and order them to "fix" it. You can't win that battle.

 --
 brandon s allbery kf8nh   sine nomine
 associates
 allber...@gmail.com
 ballb...@sinenomine.net
 unix, openafs, kerberos, infrastructure, xmonad
 http://sinenomine.net

>>>
 ___
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.org
 http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Carter Schonwald]

No. I’m saying make same variables get the parent quantified, even if it’s
implicit.

Breaking changes are ok if they make things better.

Measuring impact really comes down to making the patch and measuring. It
will be an easy to fix breaking change and my experience has been that
teams in an industrial context are a ok with none silent breaking changes.
This would be very easy to catch :)

On the pedagogy side it actually makes learning simpler afaict :)

On Sun, May 20, 2018 at 8:03 PM Anthony Clayden <
anthony_clay...@clear.net.nz> wrote:

> On Mon, 21 May 2018 at 11:23 AM, Carter Schonwald 
> wrote:
>
>> indeed .. and we can reasonably say "lets deal with the bandaid in one go
>> by cleaning it up  in the next standard"
>>
>
> Thanks Carter/Brandon, the reason for asking how we should go about the
> discussion was exactly: where/how are we going to maximise the chance of
> finding out what code is out there, and how disruptive any 'clean up' might
> be?
>
> Ghc has occasionally made breaking releases (not saying that's what we
> want to do), usually with some advance warning/deprecation period. And
> generally the Haskell community has accommodated that with understanding of
> the decision, to fix their code.
>
>
>
>> so what would the next gen look like?
>>
>> eg: fresh variables get the usual implicit forall at the front of the
>> type, and everything else either needs an explicit quantifier OR it refers
>> to the outer implicit quantified variable?
>>
>
> I wanted to avoid discussing 'next gen' in possibly-obscure/write-only
> mailing lists; and preferably get the discussion where posterity can see
> the reasoning/examination of options.
>
> "fresh variables get the usual implicit forall" is what happens now. (It's
> just that the User Guide explains it really badly -- I'm trying to fix that
> separately https://ghc.haskell.org/trac/ghc/ticket/15146 .) If the outer
> variable(s) are not explicitly forall-quantified, then even same-named
> variables count as fresh. IOW merely putting a `forall` can change the
> meaning of a program -- that's what causes the most confusion (judging by
> SO).
>
> The exception is variables bound in a pattern signature for an
> existentially-quantified data constructor: they *must* be fresh. This is
> hard for a reader to follow because the pattern signature with data
> constructor looks the same whether or not the constructor is
> existentially-quantified. What's worse a constructor might have a mix of
> existential and universal variables.
>
> AntC
>
>
>> On Sat, May 19, 2018 at 2:56 PM, Brandon Allbery 
>> wrote:
>>
>>> On Sat, May 19, 2018 at 7:32 AM, Anthony Clayden <
>>> anthony_clay...@clear.net.nz> wrote:
>>>
 So the explanation I've seen for the current design is it was deliberately 
 idiosyncratic, to minimise any disruption to existing code. Then I'm 
 asking whether any of that code is still around? If not/if it's been 
 re-factored to use ScopedTypeVariables, then any tweak to the design could 
 have a freer hand.


>>> The reason there's no discussion about that is that nobody here has the
>>> ability to go hunt down every last piece of code in every public or private
>>> (think Standard Chartered, Facebook, etc.) code base and its current owner,
>>> and order them to "fix" it. You can't win that battle.
>>>
>>> --
>>> brandon s allbery kf8nh   sine nomine
>>> associates
>>> allber...@gmail.com
>>> ballb...@sinenomine.net
>>> unix, openafs, kerberos, infrastructure, xmonad
>>> http://sinenomine.net
>>>
>>
>>> ___
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users@haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>>
>>>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Anthony Clayden]

On Mon, 21 May 2018 at 11:23 AM, Carter Schonwald 
wrote:

> indeed .. and we can reasonably say "lets deal with the bandaid in one go
> by cleaning it up  in the next standard"
>

Thanks Carter/Brandon, the reason for asking how we should go about the
discussion was exactly: where/how are we going to maximise the chance of
finding out what code is out there, and how disruptive any 'clean up' might
be?

Ghc has occasionally made breaking releases (not saying that's what we want
to do), usually with some advance warning/deprecation period. And generally
the Haskell community has accommodated that with understanding of the
decision, to fix their code.



> so what would the next gen look like?
>
> eg: fresh variables get the usual implicit forall at the front of the
> type, and everything else either needs an explicit quantifier OR it refers
> to the outer implicit quantified variable?
>

I wanted to avoid discussing 'next gen' in possibly-obscure/write-only
mailing lists; and preferably get the discussion where posterity can see
the reasoning/examination of options.

"fresh variables get the usual implicit forall" is what happens now. (It's
just that the User Guide explains it really badly -- I'm trying to fix that
separately https://ghc.haskell.org/trac/ghc/ticket/15146 .) If the outer
variable(s) are not explicitly forall-quantified, then even same-named
variables count as fresh. IOW merely putting a `forall` can change the
meaning of a program -- that's what causes the most confusion (judging by
SO).

The exception is variables bound in a pattern signature for an
existentially-quantified data constructor: they *must* be fresh. This is
hard for a reader to follow because the pattern signature with data
constructor looks the same whether or not the constructor is
existentially-quantified. What's worse a constructor might have a mix of
existential and universal variables.

AntC


> On Sat, May 19, 2018 at 2:56 PM, Brandon Allbery 
> wrote:
>
>> On Sat, May 19, 2018 at 7:32 AM, Anthony Clayden <
>> anthony_clay...@clear.net.nz> wrote:
>>
>>> So the explanation I've seen for the current design is it was deliberately 
>>> idiosyncratic, to minimise any disruption to existing code. Then I'm asking 
>>> whether any of that code is still around? If not/if it's been re-factored 
>>> to use ScopedTypeVariables, then any tweak to the design could have a freer 
>>> hand.
>>>
>>>
>> The reason there's no discussion about that is that nobody here has the
>> ability to go hunt down every last piece of code in every public or private
>> (think Standard Chartered, Facebook, etc.) code base and its current owner,
>> and order them to "fix" it. You can't win that battle.
>>
>> --
>> brandon s allbery kf8nh   sine nomine
>> associates
>> allber...@gmail.com
>> ballb...@sinenomine.net
>> unix, openafs, kerberos, infrastructure, xmonad
>> http://sinenomine.net
>>
>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Carter Schonwald]

indeed .. and we can reasonably say "lets deal with the bandaid in one go
by cleaning it up  in the next standard"

so what would the next gen look like?

eg: fresh variables get the usual implicit forall at the front of the type,
and everything else either needs an explicit quantifier OR it refers to the
outer implicit quantified variable?

On Sat, May 19, 2018 at 2:56 PM, Brandon Allbery 
wrote:

> On Sat, May 19, 2018 at 7:32 AM, Anthony Clayden <
> anthony_clay...@clear.net.nz> wrote:
>
>> So the explanation I've seen for the current design is it was deliberately 
>> idiosyncratic, to minimise any disruption to existing code. Then I'm asking 
>> whether any of that code is still around? If not/if it's been re-factored to 
>> use ScopedTypeVariables, then any tweak to the design could have a freer 
>> hand.
>>
>>
> The reason there's no discussion about that is that nobody here has the
> ability to go hunt down every last piece of code in every public or private
> (think Standard Chartered, Facebook, etc.) code base and its current owner,
> and order them to "fix" it. You can't win that battle.
>
> --
> brandon s allbery kf8nh   sine nomine
> associates
> allber...@gmail.com
> ballb...@sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad
> http://sinenomine.net
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Brandon Allbery]

On Sat, May 19, 2018 at 7:32 AM, Anthony Clayden <
anthony_clay...@clear.net.nz> wrote:

> So the explanation I've seen for the current design is it was deliberately 
> idiosyncratic, to minimise any disruption to existing code. Then I'm asking 
> whether any of that code is still around? If not/if it's been re-factored to 
> use ScopedTypeVariables, then any tweak to the design could have a freer hand.
>
>
The reason there's no discussion about that is that nobody here has the
ability to go hunt down every last piece of code in every public or private
(think Standard Chartered, Facebook, etc.) code base and its current owner,
and order them to "fix" it. You can't win that battle.

-- 
brandon s allbery kf8nh   sine nomine associates
allber...@gmail.com  ballb...@sinenomine.net
unix, openafs, kerberos, infrastructure, xmonadhttp://sinenomine.net
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Anthony Clayden]

On Wed, 9 May 2018 03:01 UTC, cheater00 wrote:

> I couldn't live without ScopedTypeVariables. For me it's an essential tool
when I want to figure out

Yes absolutely. To be clear: nobody's talking about removing it. The
question is, could we get the same functionality without being so
confusing and contrary to how Haskell usually works with type
variables? (I'm not saying yea or nay, I'm trying to invite
discussion.)

> ...

> Backwards compat: Isn't this what we have Haskell 98, Haskell 2010, etc?

The current design for ScopedTypeVariables potentially changes the
types for programs that are valid H98/H2010. (Or for programs that
were valid as at when ScopedTypeVariables was introduced ~10 years
ago, perhaps using ExplicitForAll.) Probably the effect would be that
they don't compile, but it might be more subtle.


So the explanation I've seen for the current design is it was
deliberately idiosyncratic, to minimise any disruption to existing
code. Then I'm asking whether any of that code is still around? If
not/if it's been re-factored to use ScopedTypeVariables, then any
tweak to the design could have a freer hand.


But seems there's no enthusiasm for such discussion, so I'm going to
let it die. I hear there might be moves afoot elsewhere ...


AntC
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[cheater00 cheater00]

I couldn't live without ScopedTypeVariables. For me it's an essential tool
when I want to figure out

1. if the type being inferred is the one I expect
2. what type a specific thing in code I am working with is

Also useful for adding that one bit the inferer is missing without
immediately modifying a complex type sig. I can do that later, but the
proof of concept should be quick and easy.

Backwards compat: Isn't this what we have Haskell 98, Haskell 2010, etc?

On Sat, 5 May 2018 04:35 Anthony Clayden, 
wrote:

> This thread is a discussion about discussions, not the discussion itself
> ;-)
>
> I'm cc'ing to the cafe; but I'd prefer replies to come to
> glasgow-haskell-users.
>
>
> >> I can volunteer to at least scrape together all the objections to
> ScopedTypeVariables as currently. It's not yet a proposal, so not on
> github. Start a wiki page? A cafe thread? (It'll get lost.) A ghc-users
> thread? (It'll get ignored.)
>
> > ... don’t care what forums or list or whatever. As long as it’s
> collated and such
> > It could even be on the prime issue tracker for prime proposals. Just
> that it’s written down :)
>
> Thanks Carter, but I understand Haskell Prime to be to assess
> mature/stable proposals (preferably already delivered as extensions). This
> discussion is at first going to be more exploratory:
> * likes and dislikes about ScopedTypeVariables as currently.
> * confusions experienced by users (especially newbies)
> -- although absolute newbies wouldn't be using it(?), so intermediates?
> * feedback from those teaching Haskell.
> * wild ideas for possible alternative designs.
> * possible improvements to the current design.
> * I think we're all agreed that ScopedTypeVariables should have been in
> Haskell from the beginning;
> but it wasn't, so now we have to worry about backwards compatibility for
> programs that worked around the omission.
> Or do we? What code would break? How much pain would that cause?
> * anything else?
>
> > We have lots of forums, but your point is that certain sorts of
> discussions never get going with the right audience – you especially point
> to “confused beginners”.
> > ... It’s quite a challenge because beginners tend not to be vocal, and
> yet they are a crucial set of Haskell users. Every Haskell user started as
> a beginner.
>
> On this particular topic, there's plenty of confused people asking
> questions on StackOverflow. (Heads up: they're especially asking why they
> need explicit `forall` whereas in reguar Haskell that 'intermediates' see,
> the forall is implicit.)
>
> Can other people point me to questions/likes/dislikes on other forums?
> Reddit for example.
>
> If you've read this far, you now understand what we're trying to cover.
> It's going to be random/varied thoughts at first, then perhaps coalescing
> to an approach or two. At that point a formal proposal on github proper;
> and the random stuff might be interesting background but will essentially
> get archived/thrown away.
>
> I do agree with David's suggestion that github Issue tracker looks like a
> suitable solution. We can write formatted code and text. We can add links
> and references. What do others think? Joachim has opened up Issues tracker,
> as a try-out. If using it doesn't work out, that's fine and in keeping with
> my "thrown away" above.
>
> Also where else should I post links to this message to 'advertise' the
> thread? I don't reddit much, so if that's suitable, please someone post
> there.
>
> Thank you
> AntC
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

[Anthony Clayden]

This thread is a discussion about discussions, not the discussion itself ;-)

I'm cc'ing to the cafe; but I'd prefer replies to come to
glasgow-haskell-users.


>> I can volunteer to at least scrape together all the objections to
ScopedTypeVariables as currently. It's not yet a proposal, so not on
github. Start a wiki page? A cafe thread? (It'll get lost.) A ghc-users
thread? (It'll get ignored.)

> ... don’t care what forums or list or whatever. As long as it’s collated
and such
> It could even be on the prime issue tracker for prime proposals. Just
that it’s written down :)

Thanks Carter, but I understand Haskell Prime to be to assess mature/stable
proposals (preferably already delivered as extensions). This discussion is
at first going to be more exploratory:
* likes and dislikes about ScopedTypeVariables as currently.
* confusions experienced by users (especially newbies)
-- although absolute newbies wouldn't be using it(?), so intermediates?
* feedback from those teaching Haskell.
* wild ideas for possible alternative designs.
* possible improvements to the current design.
* I think we're all agreed that ScopedTypeVariables should have been in
Haskell from the beginning;
but it wasn't, so now we have to worry about backwards compatibility for
programs that worked around the omission.
Or do we? What code would break? How much pain would that cause?
* anything else?

> We have lots of forums, but your point is that certain sorts of
discussions never get going with the right audience – you especially point
to “confused beginners”.
> ... It’s quite a challenge because beginners tend not to be vocal, and
yet they are a crucial set of Haskell users. Every Haskell user started as
a beginner.

On this particular topic, there's plenty of confused people asking
questions on StackOverflow. (Heads up: they're especially asking why they
need explicit `forall` whereas in reguar Haskell that 'intermediates' see,
the forall is implicit.)

Can other people point me to questions/likes/dislikes on other forums?
Reddit for example.

If you've read this far, you now understand what we're trying to cover.
It's going to be random/varied thoughts at first, then perhaps coalescing
to an approach or two. At that point a formal proposal on github proper;
and the random stuff might be interesting background but will essentially
get archived/thrown away.

I do agree with David's suggestion that github Issue tracker looks like a
suitable solution. We can write formatted code and text. We can add links
and references. What do others think? Joachim has opened up Issues tracker,
as a try-out. If using it doesn't work out, that's fine and in keeping with
my "thrown away" above.

Also where else should I post links to this message to 'advertise' the
thread? I don't reddit much, so if that's suitable, please someone post
there.

Thank you
AntC
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Scoped type variables Re: Open up the issues tracker on ghc-proposals

[Carter Schonwald]

Please do this!

I don’t care what forums or list or whatever. As long as it’s collated and
such

It could even be on the prime issue tracker for prime proposals.  Just that
it’s written down :)

On Wed, May 2, 2018 at 7:17 PM Anthony Clayden 
wrote:

> On Th, 3 May 2018 at 13:53 UTC, Joachim Breitner wrote:
> > I am worried about the signal-to-noise ratio for those poor committee
> members ...
>
> Thanks Joachim, Yes that's exactly the worry. So please tell the rest of
> us how to best use your collective time.
>
> First help yourselves/get your own shit together:
> there's now a long discussion on the committee mailing list about the
> specifics of #99. There are good questions, good answers, good ideas. None
> of the rest of use can contribute to that. The committee list is supposed
> to be low volume/decision making only. WTF?
>
> (That seems to be triggered by one particular committee member who
> seldom/never looks at github, and prefers email discussion. Yous others
> could perhaps coach him?)
>
> > hmm, some of that sounds like it would be better suited for haskell-cafe,
> StackOverflow, ...
>
> My point about "sometimes it's more of a niggle" was aimed at exactly your
> (Joachim's) series of proposals 'Resurrect Pattern Signatures'. The
> motivation is it helps "confused beginners". But those beginners won't be
> providing feedback on github. Instead you've got feedback from experienced
> users who've all said they see no point in the proposal. So the discussion
> has gone round and round and spun off other proposals. That whole series of
> discussions would be better happening somewhere else: where?
>
> David's quite correct
> >> Haskell-cafe might work, but it's a bit tricky to pull up all the
> language extension ideas discussed there.
>
> My impression is not many people who could help refine a pre-proposal ever
> take part in the cafe.
>
> Stackoverflow likewise. (I did raise a 'how do I do this?' type question
> there. It was David who responded, thank you. But I ended up answering it
> myself; and it turned out there was already a proposal on the slate.)
>
> >> My limited experience with glasgow-haskell-users is that it's where
> threads go to die.
>
> (I did try to continue one of David's threads there a few months ago.) But
> yes, my experience too. And that's sad because it's a wasted resource. I'm
> grateful to Simon for noticing this thread; but most topics I've raised on
> ghc-users have gone nowhere. So then I've tried pursuing them by poaching
> on Trac or github -- which is an abuse, I know.
>
> > Most vague ideas get better when the proposer is nudged to sit down and 
> > write
> it up properly! (And some get dropped in the process, which is also good
> :-)).
>
> Yes exactly what I'm trying to get to happen. How/where?
>
> Here's a specific example: there's talk of baking ScopedTypeVariables into
> the H2020 standard. There's also people unhappy with ScopedTypeVariables as
> currently (I'm one, but I don't know if my reservations are the same as
> others'). If we don't have an alternative proposal (and preferably an
> experimental extension) by 2020, the committee can only go with the as
> currently fait accompli or continue the H2010 status quo.
>
> I can volunteer to at least scrape together all the objections to
> ScopedTypeVariables as currently. It's not yet a proposal, so not on
> github. Start a wiki page? A cafe thread? (It'll get lost.) A ghc-users
> thread? (It'll get ignored.)
>
>
> AntC
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

RE: confusing GADT/scoped type variables behaviour

[Simon Peyton-Jones]

Ganesh

Sorry to be slow on this.  Thanks for the bug report.

| Now 6.6 is happy. But 6.8 doesn't believe they are the same, and rejects
| it. I finally got it to work with both by removing the forall in the
| So, is there a good explanation of the errors from 6.8? Is 6.8 behaving
| as expected?

This is a definite bug in 6.8, in the interaction of GADTs and scoped type 
variables.  I know exactly why it happens, but probably won't fix it because 
it'll fall out naturally of the work we (mainly Manuel) are doing to fully 
implement type equalities.

I've added http://hackage.haskell.org/trac/ghc/ticket/1823, which gives an even 
smaller test case.

| Finally, ideally I'd like not to have any type signatures in the body of f
| - is this feasible with 6.8 like it was with 6.6?

I'm quite surprised 6.6 works:

| f :: forall x y . D x y - ()
| f (D (C p))
|   | P q - (\p@(P a) - p) p
|= case q of

The fact that q has a rigid type is quite complicated to figure out.  Did you 
really need that lambda?

Meanwhile Ian asks:

| Although this program is the one that finally worked in both 6.6 and
| 6.8, I don't understand why it worked in either: y is not an
| existentially quantified variable, so shouldn't be allowed to be
| introduced by a type signature there based on my reading of the user
| guide.

The user guide is at fault.  You can bind a type variable with a pattern type 
signature if type of the pattern is rigid.  (With GADTs the idea of 
existential becomes fuzzier.)  So this defn is a bit more generous than 
before.  I've updated the manual.   See the GADT wobbly-type paper for a 
description of rigidity.

Simon

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

confusing GADT/scoped type variables behaviour

[Ganesh Sittampalam]

Hi,

I'm having some trouble writing code that uses GADTs. I finally got 
something that is portable between GHC 6.6 and 6.8, but I don't really 
understand what's going on, and I'm a bit unhappy with the number of type 
signatures required.


I'll explain them with a series of cut-down examples below, so please 
forgive the gratuitous beta-redexes.


My testing has been with GHC 6.6 and 6.8.0.20070921, but I believe from 
more limited testing that 6.6.1 behaves the same as 6.6.


My first program works fine with both GHC 6.6 and 6.8:

{-# OPTIONS_GHC -fglasgow-exts #-}
module GADT where

data C x y where
C :: P x y - C x x

data P x y where
P :: Q x y - P x y

data Q x y where
Q :: Q x y

data D x y where
D :: C y z - D x z

f :: forall x y . D x y - ()
f (D (C p))
 | P q - (\p - p) p
  = case q of
   Q - ()

{- end of program -}

However, when I change it slightly to make the lambda expression inspect 
the structure of p:


{-# OPTIONS_GHC -fglasgow-exts #-}
module GADT where

data C x y where
C :: P x y - C x x

data P x y where
P :: Q x y - P x y

data Q x y where
Q :: Q x y

data D x y where
D :: C y z - D x z

f :: forall x y . D x y - ()
f (D (C p))
 | P q - (\p@(P a) - p) p
  = case q of
   Q - ()

{- end of program -}

it continues to work with 6.6, but 6.8 complains that q has a wobbly type 
and I should add a type annotation.


So, I do so, also adding one to the original pattern for p otherwise my 
type variables aren't in scope:


{-# OPTIONS_GHC -fglasgow-exts #-}
module GADT where

data C x y where
C :: P x y - C x x

data P x y where
P :: Q x y - P x y

data Q x y where
Q :: Q x y

data D x y where
D :: C y z - D x z

f :: forall x y . D x y - ()
f (D (C (p :: P w z)))
 | P q :: P w z - (\p@(P a) - p) p
  = case q of
   Q - ()

{- end of program -}

Fine with 6.8, but now 6.6 is unhappy. The type variable 'w' is actually 
the same as 'y', and 6.6 seems to have noticed this fact and says I should 
have given them the same name.


So, I do so:

{-# OPTIONS_GHC -fglasgow-exts #-}
module GADT where

data C x y where
C :: P x y - C x x

data P x y where
P :: Q x y - P x y

data Q x y where
Q :: Q x y

data D x y where
D :: C y z - D x z

f :: forall x y . D x y - ()
f (D (C (p :: P y z)))
 | P q :: P y z - (\p@(P a) - p) p
  = case q of
   Q - ()

{- end of program -}

Now 6.6 is happy. But 6.8 doesn't believe they are the same, and rejects 
it. I finally got it to work with both by removing the forall in the 
signature of f:


{-# OPTIONS_GHC -fglasgow-exts #-}
module GADT where

data C x y where
C :: P x y - C x x

data P x y where
P :: Q x y - P x y

data Q x y where
Q :: Q x y

data D x y where
D :: C y z - D x z

f :: D x y - ()
f (D (C (p :: P y z)))
 | P q :: P y z - (\p@(P a) - p) p
  = case q of
   Q - ()

{- end of program -}

But, I don't really understand why this is so. I guess the 'y' in the 
outer signature is no longer a scoped type variable, so 6.6 doesn't 
complain, and is no longer the same as the inner 'y', so 6.8 doesn't 
complain, but it all feels a bit unsatisfactory.


So, is there a good explanation of the errors from 6.8? Is 6.8 behaving 
as expected?


Finally, ideally I'd like not to have any type signatures in the body of f 
- is this feasible with 6.8 like it was with 6.6?


Cheers,

Ganesh
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: confusing GADT/scoped type variables behaviour

[Ian Lynagh]

On Mon, Oct 22, 2007 at 09:46:39PM +0100, Ganesh Sittampalam wrote:
 
 {-# OPTIONS_GHC -fglasgow-exts #-}
 module GADT where
 
 data C x y where
 C :: P x y - C x x
 
 data P x y where
 P :: Q x y - P x y
 
 data Q x y where
 Q :: Q x y
 
 data D x y where
 D :: C y z - D x z
 
 f :: D x y - ()
 f (D (C (p :: P y z)))
  | P q :: P y z - (\p@(P a) - p) p
   = case q of
Q - ()

Although this program is the one that finally worked in both 6.6 and
6.8, I don't understand why it worked in either: y is not an
existentially quantified variable, so shouldn't be allowed to be
introduced by a type signature there based on my reading of the user
guide.

Here's a simpler example:

f :: a - a
f (x :: b) = x

and here's the bit of the user guide that's confusing me (in all of the
6.6.1 release, 6.8 and HEAD branches):


http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#pattern-type-sigs

There is only one situation in which you can write a pattern type
signature that mentions a type variable that is not already in scope,
namely in pattern match of an existential data constructor.

In the simpler program above 'b' is not in scope, so I would expect the
program to be rejected, but ghc-6.6.1 -fglasgow-exts and
ghc-6.8 -XPatternSignatures -XScopedTypeVariables both accept the
program.

ghc-6.8 -XPatternSignatures rejects it with

z.hs:3:8: Not in scope: type variable `b'

which also doesn't really make sense to me.

I'm not sure if this is a bug in the compiler, or if I'm just reading
the docs wrong?


Thanks
Ian

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Problem with lexically scoped type variables.

[Simon Peyton-Jones]

Aha.  That's a bug.  The forall'd type variables of an expression type
signature should scope over the expression.

Thank you -- I'll fix it, though I don't know if it'll get into 6.6 now.

Simon

| -Original Message-
| From: Mirko Rahn [mailto:[EMAIL PROTECTED]
| Sent: 02 October 2006 16:05
| To: Simon Peyton-Jones
| Cc: glasgow-haskell-users@haskell.org
| Subject: Re: Problem with lexically scoped type variables.
| 
| 
|  Oh I see. Well, you'd need to put the type annotation for s back in:
| 
|  t1 = runST ( (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) -
seen
|  s)
|  :: forall s. ST s [Int] )
| 
| ...and reach the starting point again. This version gives the same
error
| message as the original one.
| 
| But what works is to give some more detailed hints to the type system:
| 
| t1S = trav f [1..10] (1,52) :: ST s (STRef s (Set Int))
| t2S = trav f [1..10] (1,52) :: ST s (STUArray s Int Bool)
| 
| t1 = runST ( t1S = seen )
| t2 = runST ( t2S = seen )
| 
| This compiles (and works).
| 
| Thank's for advice, MR
| 
| --
| -- Mirko Rahn -- Tel +49-721 608 7504 --
| --- http://liinwww.ira.uka.de/~rahn/ ---
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Problem with lexically scoped type variables.

[Mirko Rahn]

Dear all, in

http://www.haskell.org/pipermail/glasgow-haskell-users/2006-January/009565.html

Simon Peyton-Jones asks for programs that are broken by the proposed 
change. Here is a nearly real world one:


{-# OPTIONS_GHC -fglasgow-exts #-}

import Control.Monad
import Control.Monad.ST
import Data.Array.MArray
import Data.Array.ST
import Data.STRef
import Data.Set hiding (map,filter)

-- a store that allows to mark keys
class Mark m store key | store - key m where
new   :: (key,key) - m store
mark  :: store - key - m ()
markQ :: store - key - m Bool
seen  :: store - m [ key ]

-- implementation 1
instance Ord key = Mark (ST s) (STRef s (Set key)) key where
new   _   = newSTRef empty
mark  s k = modifySTRef s (insert k)
markQ s k = liftM (member k) (readSTRef s)
seen  s   = liftM elems (readSTRef s)

-- implementation 2
instance Ix key = Mark (ST s) (STUArray s key Bool) key where
new   bnd = newArray bnd False
mark  s k = writeArray s k True
markQ = readArray
seen  s   = liftM (map fst . filter snd) (getAssocs s)

-- traversing the hull suc^*(start) with loop detection
trav suc start i = new i = \ c - mapM_ (compo c) start  return c
where compo c x = markQ c x = flip unless (visit c x)
  visit c x = mark c x  mapM_ (compo c) (suc x)

-- sample graph
f 1 = 1 : []
f n = n : f (if even n then div n 2 else 3*n+1)

t1 = runST (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) - seen s)
t2 = runST (trav f [1..10] (1,52) = \ (s::STUArray s Int Bool) - seen s)

In ghc-6.4.2 this works as expected, but ghc-6.5.20061001 says

B.hs:40:44:
A pattern type signature cannot bind scoped type variables `s'
  unless the pattern has a rigid type context
In the pattern: s :: STRef s (Set Int)
In a lambda abstraction: \ (s :: STRef s (Set Int)) - seen s
In the second argument of `(=)', namely
`\ (s :: STRef s (Set Int)) - seen s'

Unfortunately I cannot find an easy workaround but use similiar patterns 
somewhere deeply nested in my programs...


Is there a simple workaround? Could we relax the rules for lexically 
scoped type variables a bit?


Regards, Mirko Rahn

--
-- Mirko Rahn -- Tel +49-721 608 7504 --
--- http://liinwww.ira.uka.de/~rahn/ ---
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Problem with lexically scoped type variables.

[Brian Hulley]

Mirko Rahn wrote:

In ghc-6.4.2 this works as expected, but ghc-6.5.20061001 says

B.hs:40:44:
A pattern type signature cannot bind scoped type variables `s'
  unless the pattern has a rigid type context


Why are the rules for lexically scoped type variables so complicated?
Could we not just have a very simple rule like the following:

   1) Any type variable not explicitly introduced by a forall is implicitly 
scoped over the entire top level decl that contains the expression/pattern 
that contains the type variable


By entire top level decl I mean the highest level decl that makes sense 
eg:


   foo :: MonadIO m = a - m a
   foo x = let
   bar :: forall b. b - m b-- 'm' bound by foo's 
sig

   bar y = return y
   in
   bar x

   zap :: a - Int
   zap _ = let
   yup = sizeOf (undefined :: a)
   in
   yup

Regards, Brian.
--
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.

http://www.metamilk.com 


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Problem with lexically scoped type variables.

[Simon Peyton-Jones]

| Simon Peyton-Jones asks for programs that are broken by the proposed
| change. Here is a nearly real world one:

You may not like this but this should work:

Instead of

| t1 = runST (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) - seen
s)

try

t1 = runST ( (trav f [1..10] (1,52) = \ s - seen s)
:: forall s. ST s [Int] )

or, equivalently

t1 = runST run_it
  where
run_it :: forall s. ST s Int
run_it = trav f [1..10] (1,52) = \s - seen s


What's interesting about this example is that you aren't trying to bind
the type variable 's'.  You'd be quite happy to write
\ (s :: STRef _ (Set Int)) - seen s

Note the wildcard _.  Arguably, one could loosen the rules in this
case.  This is an avenue that I have seen suggested before, but which I
have, for one, not yet explored.   Maybe others have better ideas.

Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Problem with lexically scoped type variables.

[Mirko Rahn]

Simon Peyton-Jones wrote:


| t1 = runST (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) - seen
s)

try

t1 = runST ( (trav f [1..10] (1,52) = \ s - seen s)
:: forall s. ST s [Int] )


No, the problem is that t1 should use another implementation than t2. 
This version cannot discriminate between different implementations 
anymore. (And logically it did not compile.)


In 6.4.2 I can choose the implementation just by type annotation but 
that's now impossible...



What's interesting about this example is that you aren't trying to bind
the type variable 's'.  You'd be quite happy to write
\ (s :: STRef _ (Set Int)) - seen s



Note the wildcard _.  Arguably, one could loosen the rules in this
case.  This is an avenue that I have seen suggested before, but which I
have, for one, not yet explored.   Maybe others have better ideas.


For me it would exactly solve the problem. So maybe one could 'quick 
hack' it into ghc!?


Regards, MR

--
-- Mirko Rahn -- Tel +49-721 608 7504 --
--- http://liinwww.ira.uka.de/~rahn/ ---
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Problem with lexically scoped type variables.

[Simon Peyton-Jones]

|  | t1 = runST (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) -
seen
|  s)
| 
|  try
| 
|  t1 = runST ( (trav f [1..10] (1,52) = \ s - seen s)
|  :: forall s. ST s [Int] )
| 
| No, the problem is that t1 should use another implementation than t2.
| This version cannot discriminate between different implementations
| anymore. (And logically it did not compile.)

Oh I see. Well, you'd need to put the type annotation for s back in:

t1 = runST ( (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) - seen
s)
:: forall s. ST s [Int] )

Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Problem with lexically scoped type variables.

[Mirko Rahn]

Oh I see. Well, you'd need to put the type annotation for s back in:

t1 = runST ( (trav f [1..10] (1,52) = \ (s::STRef s (Set Int)) - seen
s)
:: forall s. ST s [Int] )


...and reach the starting point again. This version gives the same error 
message as the original one.


But what works is to give some more detailed hints to the type system:

t1S = trav f [1..10] (1,52) :: ST s (STRef s (Set Int))
t2S = trav f [1..10] (1,52) :: ST s (STUArray s Int Bool)

t1 = runST ( t1S = seen )
t2 = runST ( t2S = seen )

This compiles (and works).

Thank's for advice, MR

--
-- Mirko Rahn -- Tel +49-721 608 7504 --
--- http://liinwww.ira.uka.de/~rahn/ ---
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: lexically-scoped type variables in GHC 6.6

[Simon Peyton-Jones]

| With reference to the documentation [about lexically scoped type
variables] that just appeared in darcs:

For the benefit of others, the draft 6.6 documentation is here

http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions
.html#scoped-type-variables

| Result type signatures are now equivalent to attaching the signature
| to the rhs, i.e. redundant.

Yes, that's true.  I don't think I had fully absorbed that.  They didn't
*use* to be redundant, because they used to bind type variables, but now
that they don't they are entirely redundant.  It is perhaps sometimes a
bit more convenient to write the (small) type before the (big)
expression, but that's true of type signatures in general.  If we cared
about that we should provide a prefix form of expression type signature

I think I will therefore remove them from the documentation, and (in due
course) from the code.  

| How about finishing the decoupling of type variable binding from
pattern
| type signatures by introducing an (optional) pattern form
| 
|   forall v1 ... vk. C p1 ... pn
| 
| mimicking the datatype declaration for an existential (with vi scoping
| over pj, guards, where decls and the rhs), so the example would become
| 
|   data T = forall a. MkT [a]
| 
|   k :: T - T
|   k (forall a. MkT [t]) = MkT t3
|   where
|   t3::[a] = [t,t,t]

Stepanie and I have discussed this idea -- but in a different syntax.
We were thinking of writing a pattern like

k (MkT {a} [t]) = ...

where the {a} binds the polymorphic parameters.  But that's new syntax
and I quite like your idea of re-using forall.

The other awkward question is: when there are several existential type
variables, which order do they come in?  You may say the foralls in the
data type decl must match the foralls in the pattern.  Thus
data T = forall a b. MkT ...
k (forall a b. MkT ...) = ...
But with GADTs, you don't necessarily write a forall.  Suppose T was
declared thus:
data T where
  MkT :: b - a - T
Now, which order should the foralls in the pattern come in?

Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: lexically-scoped type variables in GHC 6.6

[Brian Hulley]

Ross Paterson wrote:

data T = forall a. MkT [a]

k :: T - T
k (forall a. MkT [t]) = MkT t3
where
t3::[a] = [t,t,t]


What was wrong with the example in the documentation?

 k :: T - T
 k (MkT [t::a]) = MkT t3
where
  t3::[a] = [t,t,t]

The type of (t) is (a) - what could possibly be simpler?

No doubt I'm missing something because the docs then go on to say If this 
seems a little odd... - but it doesn't. It makes perfect sense. Why 
shouldn't a pattern type signature introduce a scoped type variable? It also 
has the advantage that you can see what the type variable is supposed to 
represent without having to track down the original data declaration.


Regards, Brian.
--
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.

http://www.metamilk.com 


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: lexically-scoped type variables in GHC 6.6

[Brian Hulley]

Brian Hulley wrote:

Ross Paterson wrote:

data T = forall a. MkT [a]

k :: T - T
k (forall a. MkT [t]) = MkT t3
where
t3::[a] = [t,t,t]


What was wrong with the example in the documentation?

 k :: T - T
 k (MkT [t::a]) = MkT t3
where
  t3::[a] = [t,t,t]

The type of (t) is (a) - what could possibly be simpler?

No doubt I'm missing something because the docs then go on to say If
this seems a little odd... - but it doesn't. It makes perfect sense.
Why shouldn't a pattern type signature introduce a scoped type
variable? It also has the advantage that you can see what the type
variable is supposed to represent without having to track down the
original data declaration.


If the problem is that pattern type signatures normally have an implicit 
forall (which stops them introducing lexically scoped type variables), 
perhaps the implicit forall could be discarded so that any type variables in 
a pattern signature not in the scope of an *explicit* forall would be 
lexically scoped over the whole of an equation (or the guarded part if they 
occur first in the guard) eg:


   foo (f :: a - b) (x:: a) = ((f x) :: b)

meaning:

   forall a b. (foo (f :: a - b) (x :: a) = ((f x) :: b))

and

   foo (f :: forall a. a- b) x = ((f x) :: b)

meaning:

   forall b. (foo (f :: forall a. a- b) x = ((f x) :: b))

Apologies if I'm still missing what the real problem is,
Brian. 


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

lexically-scoped type variables in GHC 6.6

[Ross Paterson]

With reference to the documentation that just appeared in darcs:

Result type signatures are now equivalent to attaching the signature
to the rhs, i.e. redundant.

How about finishing the decoupling of type variable binding from pattern
type signatures by introducing an (optional) pattern form

forall v1 ... vk. C p1 ... pn

mimicking the datatype declaration for an existential (with vi scoping
over pj, guards, where decls and the rhs), so the example would become

data T = forall a. MkT [a]

k :: T - T
k (forall a. MkT [t]) = MkT t3
where
t3::[a] = [t,t,t]

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Lexically scoped type variables

[Simon Peyton-Jones]

I took a look.  Here's a typical example:

newVariableListFromSet :: Ord a = VariableSetSource a - VariableList a
newVariableListFromSet (variableSetSource :: VariableSetSource a) =
   let
  attachListOp parallelX (listDrawer :: ListDrawer a pos) =
 do
(posRegistry :: Registry a pos) - newRegistry

groupingCount - newIORef 0

let
   updateFn :: VariableSetUpdate a - IO ()
   updateFn (AddElement a) = 
  do
 addElement a

...

To fix this you'd need to

a) Add a 'forall a.' to the sig for newVariableListFromSet.  That brings
'a' into scope in the defn of the function.  (Arguably, the *implicit*
foralls should be in scope too; I'd be interested in what you think.)

b) Add a type signature for attachListOp, beginning with forall pos.



The main thing we're creeping towards is making it clear where scoped
type variables are quantified.  For example, is attachListOp polymorphic
in 'pos'?  We are thinking about allowing you to bind the polymorphic
type variables of a function in patterns *on the left* of the '='.  That
would make you happy, I think.

Simon

| -Original Message-
| From: Christian Maeder [mailto:[EMAIL PROTECTED]
| Sent: 02 February 2006 17:19
| To: Simon Peyton-Jones; GHC Users Mailing List
| Subject: Re: Lexically scoped type variables
| 
|  | Simon Peyton-Jones wrote:
|  |  I'm very interested to know whether you like it or hate it.
|  |  In the latter case, I'd also like to know whether you also
|  |  have programs that will be broken by the change.
|  |
|  | I don't use GADTs yet and I assume this change will not
(seriously)
|  | break our code, but let me/us know which compiler we should use
for
|  testing.
| 
| I've installed now ghc-6.5.20060201 and I get quite a few errors of
the
| form:
| 
|  A pattern type signature cannot bind scoped type variables `s'
|unless the pattern has a rigid type context
| 
| (and these are not always easy to fix in unknown non-haskell98 code by
| adding a forall and/or omitting the pattern type signatures)
| 
| Christian
| 
| You may try to translate the attached sources by:
| 
|ghc --make -cpp -fallow-undecidable-instances -fglasgow-exts
| VariableList.hs
| 
| (and tell me how I should fix this)
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Lexically scoped type variables

[Christian Maeder]

Simon Peyton-Jones wrote:

I took a look.  Here's a typical example:

newVariableListFromSet :: Ord a = VariableSetSource a - VariableList a
newVariableListFromSet (variableSetSource :: VariableSetSource a) =
   let
  attachListOp parallelX (listDrawer :: ListDrawer a pos) =
 do
(posRegistry :: Registry a pos) - newRegistry

[..]


To fix this you'd need to



b) Add a type signature for attachListOp, beginning with forall pos.


That was exactly my problem. How should I find out the type of 
attachListOp (I have not written this bit of code)? Could I somehow ask 
ghci-6.4.1 to do it for me?


Thanks for looking into it, Christian
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Lexically scoped type variables

[Simon Peyton-Jones]

| That was exactly my problem. How should I find out the type of
| attachListOp (I have not written this bit of code)? Could I somehow
ask
| ghci-6.4.1 to do it for me?

(Unsatisfactory but would work) You could compile with -ddump-ds and
look at the output.

Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Lexically scoped type variables

[Christian Maeder]

Simon Peyton-Jones wrote:

(Unsatisfactory but would work) You could compile with -ddump-ds and
look at the output.


Yes, I did work (for VariableList.hs)

attachListOp :: forall pos . ParallelExec - ListDrawer a pos
  - IO (IO ())

Thanks, Christian

(I need to get a new ghc-6.5 without the overlapping-instances bug for 
further tests)

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Lexically scoped type variables

[Christian Maeder]

Simon Peyton-Jones wrote:

I'm very interested to know whether you like it or hate it.
In the latter case, I'd also like to know whether you also 
have programs that will be broken by the change.


I don't use GADTs yet and I assume this change will not (seriously) 
break our code, but let me/us know which compiler we should use for testing.


Cheers Christian
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Lexically scoped type variables

[Simon Peyton-Jones]

Dear GHC users

As part of a revision of GHC to make type inference for GADTs simpler
and more uniform, I propose to change the way in which lexically-
scoped type variables work in GHC.  (Indeed, I have done so, and will
commit it shortly.)  This message explains the new system, highlighting
the differences.

I'm very interested to know whether you like it or hate it.
In the latter case, I'd also like to know whether you also 
have programs that will be broken by the change.

Simon

Scoped type variables in GHC

January 2006

0) Terminology.
   
   A *pattern binding* is of the form
pat = rhs

   A *function binding* is of the form
f pat1 .. patn = rhs

   A binding of the formm
var = rhs
   is treated as a (degenerate) *function binding*.


   A *declaration type signature* is a separate type signature for a
   let-bound or where-bound variable:
f :: Int - Int

   A *pattern type signature* is a signature in a pattern: 
\(x::a) - x
f (x::a) = x

   A *result type signature* is a signature on the result of a
   function definition:
f :: forall a. [a] - a
head (x:xs) :: a = x

   The form
x :: a = rhs
   is treated as a (degnerate) function binding with a result
   type signature, not as a pattern binding.

1) The main invariants:

 A) A lexically-scoped type variable always names a rigid
type variable (not a wobbly one, and not a non-type-variable 
type).  THIS IS A CHANGE.  Previously, a scoped type variable
named an arbitrary *type*.

 B) A type signature always describes a rigid type (since
its free (scoped) type variables name rigid type variables).
This is also a change, a consequence of (A).

 C) Distinct lexically-scoped type variables name distinct
rigid type variables.  This choice is open; 

  This means that you cannot say
\(x:: [a]) - expr
  (where 'a' is not yet in scope) to enforce that x is a list without 
  saying anything about 'a'.  (Well, not unless the type of this lambda
  is known from the outside.)

1a) Possible extension.  We might consider allowing
\(x :: [ _ ]) - expr
where _ is a wild card, to mean x has type list of something,
without
naming the something.

  
2) Scoping

2(a) If a declaration type signature has an explicit forall, those type
   variables are brought into scope in the right hand side of the 
   corresponding binding (plus, for function bindings, the patterns on
   the LHS).  
f :: forall a. a - [a]
f (x::a) = [x :: a, x]
   Both occurences of 'a' in the second line are bound by 
   the 'forall a' in the first line

   A declaration type signature *without* an explicit top-level forall
   is implicitly quantified over all the type variables that are
   mentioned in the type but not already in scope.  GHC's current
   rule is that this implicit quantification does *not* bring into scope
   any new scoped type variables.
f :: a - a
f x = ...('a' is not in scope here)...
   This gives compatibility with Haskell 98

2(b) A pattern type signature implicitly brings into scope any type
   variables mentioned in the type that are not already into scope.
   These are called *pattern-bound type variables*.
g :: a - a - [a]
g (x::a) (y::a) = [y :: a, x]
   The pattern type signature (x::a) brings 'a' into scope.
   The 'a' in the pattern (y::a) is bound, as is the occurrence on 
   the RHS.  

   A pattern type siganture is the only way you can bring existentials 
   into scope.
data T where
  MkT :: forall a. a - (a-Int) - T

f x = case x of
MkT (x::a) f - f (x::a)

2a) QUESTION
class C a where
  op :: forall b. b-a-a

instance C (T p q) where
  op = rhs
Clearly p,q are in scope in rhs, but is 'b'?  Not at the moment.
Nor can you add a type signature for op in the instance decl.
You'd have to say this:
instance C (T p q) where
  op = let op' :: forall b. ...
   op' = rhs
   in op'

3) A pattern-bound type variable is allowed only if the pattern's
   expected type is rigid.  Otherwise we don't know exactly *which*
   skolem the scoped type variable should be bound to, and that means
   we can't do GADT refinement.  This is invariant (A), and it is a
change
   from the current situation.

f (x::a) = x-- NO

g1 :: b - b
g1 (x::b) = x   -- YES, because the pattern type is rigid

g2 :: b - b
g2 (x::c) = x   -- YES, same reason

h :: forall b. b - b
h (x::b) = x-- YES, but the inner b is bound

k :: forall b. b - b
k (x::c) = x-- NO, it can't be both b and c

3a) You *can* give a different name to the same type variable in
different
disjoint scopes, just as you can (if you want) give diferent names
to 
the same value

Re: Lexically scoped type variables

[Johannes Waldmann]

On the syntax of type signatures: I'd like to be able to write e. g.

do
x :: Int - randomRIO ( 0, 10 )
print x

Currently I have to put ( x :: Int ) in parentheses. Is this necessary?
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
 http://www.imn.htwk-leipzig.de/~waldmann/ ---

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Henrik Nilsson]

Hi all,
Olaf Chitil wrote:
 Hence I support Jon in that ghc should only allow those type variables
 a wider scope that have been explicitly declared with the non-Haskell
 98 keyword forall.
I'm inclined to support Jon and Olaf here.
I'm pretty sure there's lot of code out there that use -fglasgow-exts
for all sorts of reasons totally unrelated to scoped type variables.
Moreover, I suspect that type signatures for local definitions are quite
common too. I, at least, use them a fair bit. So, unless it is 100%
clear that the proposed additional way of introducing scoped type
variables really is the way to go, I would say go for the version
that breaks the fewest programs.
If nothing else, if it does turn out to really be the right way, it
would seem fairly easy to later generalize the rule, by not requiring
an explicit forall (and thus recovering the property that the current
type signature syntax is just a syntactic shorthand) than go the other
way.
Personally, I always get a bit worried when there is too much magic
going on, e.g. when the meaning of syntactic constructs are stretched
in various ways in attempts to do the right thing tacitly. I believe
it usually better, in the long run at least, to state intentions more
explicitly. E.g., in this case, maybe it isn't such a bad idea after
all to differentiate syntactically between binding occurrences and
referring  occurrences of scoped type variables?
Thus, also from this perspective it would seem that requiring an
explicit forall for introducing scoped type variables would be the
better option as it could be argued that intentions are stated a bit
more explicitly that way, although maybe not in as explicitly as
could be desired.
It is, however, unfortunate that a signature without outer foralls
no longer would be just a syntactic shorthand for signatures with the
foralls mentioned explicitly.
Best regards,
/Henrik
--
Henrik Nilsson
School of Computer Science and Information Technology
The University of Nottingham
[EMAIL PROTECTED]
This message has been scanned but we cannot guarantee that it and any
attachments are free from viruses or other damaging content: you are
advised to perform your own checks.  Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Scoped type variables

[Simon Peyton-Jones]

| Would it help to stick the quantifier at the beginning of
| the type declaration?
| 
|  forall a b . g :: Foo a b = [a] - [a]
|  g = ...

Since GHC already allows explicit quantifiers, I had indeed wondered
about saying that a type sig only brings type variables into scope if it
has an explicit quantifier.  Thus

g :: forall a b. Foo a b = [a] - [a]
g = ...
would bring a  b into scope in the ..., but
g :: Foo a b = [a] - [a]
g = ...
would not.  I guess that has the merit that adding the feature would
break fewer programs.

I'm not keen on putting the foralls before the function name.

Simon

___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Olaf Chitil]

I'm not sure I understand the objection raised by Jon; the 'implicit
declaration' of type variables in type signatures has never bothered
me, and in fact seems quite similar to how names for values don't have
to be declared beforehand but are brought into scope by the binding
(which I also have no problem with).
 

The binding of a variable is the declaration of the variable. In 
contrast, type variables are never declared in Haskell 98, they are only 
used. In my opinion this lack of an explicit type variable quantifier is 
just acceptable, because all type variables are universally quantified 
and their scope is just the type in which they appear. The very moment 
you allow for wider scopes of type variables the disadvantage of the 
lacking type variable quantifier becomes appearant:

When you see
   f :: a - a
somewhere within an inner where clause you do not know at all if this 
means
   f :: forall a. a - a
or the a is actually quantified somewhere outside and hence f has a 
far more restricted type (because Haskell does not even require you to 
write a type signature next to its variable binding, you have to search 
the *whole* module to find out).

So scoped type variables do not fit Haskell well anyway, but I think 
when added they should at least be an upward compatible extension; any 
Haskell 98 program should still be correct. Hence I support Jon in that 
ghc should only allow those type variables a wider scope that have been 
explicitly declared with the non-Haskell 98 keyword forall.

Olaf
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Atze Dijkstra]

At 17:51 + 17/12/2004, Simon Peyton-Jones wrote:
OK, OK, I yield!
This message is about lexically scoped type variables.  I've gradually
become convinced that if you write
f :: [a] - [a]
f x = body
then the type variable 'a' should be in scope in body.   At present in
GHC you have to write
f (x :: [a]) = body
to bring 'a' into scope.
I've fought against this because it seems funny for a 'forall' in a type
signature to bring a type variable into scope in perhaps-distant
function body, but it's just so convenient and natural.  Furthermore,
as Martin Sulzmann points out, you might have type variables that are
mentioned only in the context of the type:
g :: Foo a b = [a] - [a]
g = ...
GHC provides no way to bring 'b' into scope at the moment, and that
seems bad design.
Some design choices are unclear, at least to me. First, the 
separation of body and signature. I am used to locally introduced 
identifiers being visible locally too (i.e. requiring minimal 
scrolling through a file). This would break, meaning that I have to 
know which identifier was used in the signature. Related to this, how 
does this work out for signatures of class members and their 
instances, often separated over different files? A change in a type 
variable in a signature in a class inside a library might then break 
my instance of that class. Or is this mechanism only meant for let 
bound values? If not, and if taken to the other extreme, a type 
variable identifier may well become part of the type itself and its 
'meaning'. That is, given a type signature and a value definition 
complying with the signature always has the type variables available. 
The following then also might be admitted:

f :: (forall a . a - a) - ...
v = f (\x - x::a)
Second, for a duplicate introduction of 'a' in:
f :: [a] - [a]
f (x::a) = body
Is the 'a' introduced in 'f (x::a)' shadowing the 'a' introduced in 
'f :: [a] - [a]'? If so, the separation of body and signature is 
slightly less of a problem because the 'a' introduced in the pattern 
will not create a 'duplicate identifier introduction' error message 
or a type mismatch (here between [a] and a).

From a purist point of view I prefer to avoid spreading local 
information globally because we humans can cater with large programs 
only because we keep things local. From a pragmatic point of view as 
a Haskell user the feature seems to be a convenient one indeed. From 
a pragmatic point of view as a Haskell implementor I obviously still 
have questions.

cheers,
--
- Atze -
Atze Dijkstra, Institute of Information  Computing Sciences,/|\
Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands  / | \
Tel.: +31-30-2534093/1454 | WWW  : http://www.cs.uu.nl/~atze   /--|  \
Fax : +31-30-2513971  | Email: [EMAIL PROTECTED]  /   |___\
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Andre Pang]

On 18/12/2004, at 4:51 AM, Simon Peyton-Jones wrote:
This message is about lexically scoped type variables.  I've gradually
become convinced that if you write
f :: [a] - [a]
f x = body
then the type variable 'a' should be in scope in body.
I don't have a particularly strong opinion about this, but I've always 
thought that your suggestion is the way it should have been done.  I 
actually find it confusing when someone re-declares the type 
variables in the function body; e.g. in your example of ...

f :: [a] - [a]
f x = my_id x
   where
   my_id :: a - a
   my_id y = y
I would be very much inclined to use a type signature of my_id :: b - 
b, which makes it 100% obvious that it's using a fresh type variable.  
Considering that normal variables are lexically scoped, it seems 
intuitive to me that type variables should also be lexically scoped.

--
% Andre Pang : trust.in.love.to.save
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Scoped type variables

[Simon Peyton-Jones]

OK, OK, I yield!

This message is about lexically scoped type variables.  I've gradually
become convinced that if you write

f :: [a] - [a]
f x = body

then the type variable 'a' should be in scope in body.   At present in
GHC you have to write
f (x :: [a]) = body
to bring 'a' into scope. 

I've fought against this because it seems funny for a 'forall' in a type
signature to bring a type variable into scope in perhaps-distant
function body, but it's just so convenient and natural.  Furthermore,
as Martin Sulzmann points out, you might have type variables that are
mentioned only in the context of the type:
g :: Foo a b = [a] - [a]
g = ...
GHC provides no way to bring 'b' into scope at the moment, and that
seems bad design.


If I do this, which I'm inclined to, it could break some programs,
because (with -fglasgow-exts) all type signatures will bring scoped type
variables into scope in their function body.  Here's an example that
will break

f :: [a] - [a]
f x = my_id x
   where
   my_id :: a - a
   my_id y = y

The type signature for my_id will become monomorphic, since 'a' is now
in scope, so the application (my_id x) will fail saying
can't unify 'a' with '[a]'.  
In some ways that makes sense.  If you used 'b' instead in the defn of
my_id, it'd be fine, because my_id would get the type (forall b. b-b).
Fixing such breakages is easy.


So there it is.   Any one have strong opinions?  (This is in addition to
the existing mechanism for bringing scoped type variables into scope via
pattern type signatures, of course.)

Simon
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Jon Fairbairn]

On 2004-12-17 at 17:51GMT Simon Peyton-Jones wrote:
 This message is about lexically scoped type variables.

I've been trying to work out what I think about this since
you sent out the first message in this thread. I'm not sure
that I've come to a useful conclusion, so I'll summarise my
thoughts and see if that makes anything pop out of someone
else's head.

First, I've never liked the fact that type variables in
signatures aren't declared anywhere -- this was part of the
motivation that drove me to use a non-Hindley-Milner type
system in Ponder. There, you could put a quantifier on an
expression, so instead of 

   f :: [a] - [a]
   f x = body

you could write (mangled to make it look more like Haskell)
stuff like f = forall a.\(x::[a]) - body::[a] and the
scope of a was completely clear.

Of course, this doesn't work with the way variables are
declared in Haskell.

Would it help to stick the quantifier at the beginning of
the type declaration?

   forall a b . g :: Foo a b = [a] - [a]
   g = ...

That reads OK, and one can imagine that whenever you see a
g = ...  bit, you implicitly get the type variables that
come at the front of the type declaration in scope as well.

Doing this would mean that you keep the old behaviour for
cases where there is no quantifier at the beginning of the
type declaration, so things wouldn't break.

 So there it is.  Any one have strong opinions?  (This is
 in addition to the existing mechanism for bringing scoped
 type variables into scope via pattern type signatures, of
 course.)

If I have a strong opinion about anything it's that the only
thing that should bring type variables into scope is a(n
implied) quantifier. Free variables are nasty. I don't hold
out much hope of convincing anyone of this last, though.


  Jón

-- 
Jón Fairbairn [EMAIL PROTECTED]


___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Keean Schupke]

what about having -fno-lexically-scoped-types for old code?
   Keean.
Simon Peyton-Jones wrote:
OK, OK, I yield!
This message is about lexically scoped type variables.  I've gradually
become convinced that if you write
f :: [a] - [a]
f x = body
then the type variable 'a' should be in scope in body.   At present in
GHC you have to write
	f (x :: [a]) = body
to bring 'a' into scope. 

I've fought against this because it seems funny for a 'forall' in a type
signature to bring a type variable into scope in perhaps-distant
function body, but it's just so convenient and natural.  Furthermore,
as Martin Sulzmann points out, you might have type variables that are
mentioned only in the context of the type:
g :: Foo a b = [a] - [a]
g = ...
GHC provides no way to bring 'b' into scope at the moment, and that
seems bad design.
If I do this, which I'm inclined to, it could break some programs,
because (with -fglasgow-exts) all type signatures will bring scoped type
variables into scope in their function body.  Here's an example that
will break
f :: [a] - [a]
f x = my_id x
   where
   my_id :: a - a
   my_id y = y
The type signature for my_id will become monomorphic, since 'a' is now
in scope, so the application (my_id x) will fail saying
	can't unify 'a' with '[a]'.  
In some ways that makes sense.  If you used 'b' instead in the defn of
my_id, it'd be fine, because my_id would get the type (forall b. b-b).
Fixing such breakages is easy.

So there it is.   Any one have strong opinions?  (This is in addition to
the existing mechanism for bringing scoped type variables into scope via
pattern type signatures, of course.)
Simon
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
 

___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Scoped type variables

[Abraham Egnor]

Please!  I've lost count of the number of times when I've written code as

f :: a - b
f (x :: a) = ...

wishing that I didn't have to locally bind the 'a'.

I'm not sure I understand the objection raised by Jon; the 'implicit
declaration' of type variables in type signatures has never bothered
me, and in fact seems quite similar to how names for values don't have
to be declared beforehand but are brought into scope by the binding
(which I also have no problem with).

Abe

On Fri, 17 Dec 2004 19:37:00 +, Keean Schupke
[EMAIL PROTECTED] wrote:
 what about having -fno-lexically-scoped-types for old code?
 
 Keean.
 
 Simon Peyton-Jones wrote:
 
 OK, OK, I yield!
 
 This message is about lexically scoped type variables.  I've gradually
 become convinced that if you write
 
f :: [a] - [a]
f x = body
 
 then the type variable 'a' should be in scope in body.   At present in
 GHC you have to write
f (x :: [a]) = body
 to bring 'a' into scope.
 
 I've fought against this because it seems funny for a 'forall' in a type
 signature to bring a type variable into scope in perhaps-distant
 function body, but it's just so convenient and natural.  Furthermore,
 as Martin Sulzmann points out, you might have type variables that are
 mentioned only in the context of the type:
g :: Foo a b = [a] - [a]
g = ...
 GHC provides no way to bring 'b' into scope at the moment, and that
 seems bad design.
 
 
 If I do this, which I'm inclined to, it could break some programs,
 because (with -fglasgow-exts) all type signatures will bring scoped type
 variables into scope in their function body.  Here's an example that
 will break
 
f :: [a] - [a]
f x = my_id x
   where
   my_id :: a - a
   my_id y = y
 
 The type signature for my_id will become monomorphic, since 'a' is now
 in scope, so the application (my_id x) will fail saying
can't unify 'a' with '[a]'.
 In some ways that makes sense.  If you used 'b' instead in the defn of
 my_id, it'd be fine, because my_id would get the type (forall b. b-b).
 Fixing such breakages is easy.
 
 
 So there it is.   Any one have strong opinions?  (This is in addition to
 the existing mechanism for bringing scoped type variables into scope via
 pattern type signatures, of course.)
 
 Simon
 ___
 Glasgow-haskell-users mailing list
 [EMAIL PROTECTED]
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
 
 
 
 ___
 Glasgow-haskell-users mailing list
 [EMAIL PROTECTED]
 http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users