RE: The monomorphism restriction and monomorphic pattern bindings
| Ok. So I counter-propose that we deal with pattern bindings like this:
|
|The static semantics of a pattern binding are given by the following
|translation. A binding 'p = e' has the same meaning as the set of
|bindings
|
| z = e
| x1 = case z of { p - x1 }
| ...
| xn = case z of { p - xn }
|
|where z is fresh, and x1..xn are the variables of the pattern p.
|
| For bang patterns, I think it suffices to say that a bang at the top
| level of p is carried to the binding for z, and then separately define
| what banged variable bindings mean (i.e. add appropriate seqs).
Fair enough. Although there will still be quite a bit of System F plumbing
generated, I do agree that answers my questions about the static semantics of
pattern bindings (*provided* we lift the MR). And I agree that it gives a
simple, consistent, and explicable story to the programmer.
The result may or may not do what you want though:
(f, g) = ( (+), (+) )
will generate
f :: (Num a, Num b) = a - a - a
which is ambiguous. In general, pattern bindings for overloaded things are
probably useless. Perhaps worth pointing this out in the report.
Let's also make sure that the spec explicitly includes type signatures. That
is, the above transformation is carried out, and then the individual bindings
for the xi are compared with their individual type signatures.
Simon
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
On Wed, Apr 30, 2008 at 12:18:47PM +0100, Ross Paterson wrote: On Wed, Apr 23, 2008 at 10:32:24AM -0700, Simon Marlow wrote: The current proposal on the table for what to do about the monomorphism restriction (henceforth MR) is * remove the MR entirely Just to be clear, are we talking only about Rule 1 of the MR? Rule 2 seems unavoidable, but it should probably say entire group of mutually recursive modules rather than entire module. Rule 2 Any monomorphic type variables that remain when type inference for an entire module is complete, are considered ambiguous, and are resolved to particular types using the defaulting rules. Sounds right to me. Although personally I think defaulting should be removed from the language (but left in the interactive environments), but that's another debate! Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
Hi,
On Mon, Apr 28, 2008 at 9:42 AM, Simon Marlow [EMAIL PROTECTED] wrote:
Ok. So I counter-propose that we deal with pattern bindings like this:
The static semantics of a pattern binding are given by the following
translation. A binding 'p = e' has the same meaning as the set of
bindings
z = e
x1 = case z of { p - x1 }
...
xn = case z of { p - xn }
where z is fresh, and x1..xn are the variables of the pattern p.
For bang patterns, I think it suffices to say that a bang at the top level
of p is carried to the binding for z, and then separately define what banged
variable bindings mean (i.e. add appropriate seqs).
Does anyone see any problems with this?
Seems good to me.
Oh, and I also propose to use the terminology variable binding instead of
simple pattern binding, which is currently used inconsistently in the
report (see section 4.4.3.2).
This also makes sense. Perhaps, we should use strict variable
binding instead of banged variable binding as well?
-Iavor
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
On Mon, Apr 28, 2008 at 09:42:10AM -0700, Simon Marlow wrote:
Ok. So I counter-propose that we deal with pattern bindings like this:
The static semantics of a pattern binding are given by the following
translation. A binding 'p = e' has the same meaning as the set of
bindings
z = e
x1 = case z of { p - x1 }
...
xn = case z of { p - xn }
where z is fresh, and x1..xn are the variables of the pattern p.
Just to check, this is saying no change relative to Haskell 98
(although perhaps specifying it less ambiguously), right?
Oh, and I also propose to use the terminology variable binding instead
of simple pattern binding,
Good idea.
Thanks
Ian
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
RE: The monomorphism restriction and monomorphic pattern bindings
| The report doesn't actually mention this translation although it is | widely used to implement pattern bindings, and in some compilers (not | GHC) the translation is done before type checking. | | What's interesting to me is that perhaps this gives us a way to | understand what the static semantics of pattern bindings should be, | absent MPB. e.g. Yes, that's a fine point. If this became the formal definition of the *static* semantics of pattern bindings, that would be a significant improvement, because it'd give us a precise way to answer the various questions I asked. (We might or might not like the answers, but at least we could answer them.) Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
Hi Simon, Those additional reasons given are much more compelling, and should definately go on the wiki. I think the essential point is that it makes reasoning about the code simpler - regardless of the effect on implementation. My main remaining reservation is that: (x) /= x [EMAIL PROTECTED] /= x It really worries me that (caf) = foo Can be in an entirely different complexity class from caf = foo. It seems like the kind of refactoring that beginners will be immediately drawn to, and even experienced programmers will get tripped up on. Anyone doing (caf) is virtually going to be required to add a comment just above stating that the brackets are essential. Does it still work if you relax the definitions so that [EMAIL PROTECTED] is a pattern binding only if y is a pattern binding, and (x) is a pattern binding only if x is a pattern binding? Thanks Neil On 4/25/08, Simon Peyton-Jones [EMAIL PROTECTED] wrote: | The report doesn't actually mention this translation although it is | widely used to implement pattern bindings, and in some compilers (not | GHC) the translation is done before type checking. | | What's interesting to me is that perhaps this gives us a way to | understand what the static semantics of pattern bindings should be, | absent MPB. e.g. Yes, that's a fine point. If this became the formal definition of the *static* semantics of pattern bindings, that would be a significant improvement, because it'd give us a precise way to answer the various questions I asked. (We might or might not like the answers, but at least we could answer them.) Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: The monomorphism restriction and monomorphic pattern bindings
| Iavor: | the change is valid. I do believe that you can probably work around | the problem in many situations but the question in my mind is why | should we have to work around stuff when we have a system that already | works? In other words, what problem do MBPs solve? ... | Neil: | Haskell has always had the attitude of doing what suits users, and | making implementations work hard to handle the language features. In | addition, this is a breaking change. I have not made my case well! 1. [Minor point] In general I agree with what Iavor and Neil say above, but it should not be an Iron Law. If a small and easily-describable restriction in programming yields a significant simplification in implementation, that's a benefit that may be worth having. 2. More importantly, I am using System F *not* because it tells us about GHC's implementation, but because I have found that it's an excellent litmus test that tells when something smelly is going on. The fact that one has to go through contortions to translate pattern bindings is a Bad Sign, I believe. 3. I'm more concerned about the programmer than the implementation. Consider (f,g) = (negate, show) What type do you expect 'f' to have? A straightforward answer might be f :: (Num a, Show b) = a - a If you don't want that, you need to explain a more complicated typing rule for pattern bindings.I'll ask the same about (f,g) = (reverse, length) A simple and consistent story is that all the pattern bound variables are generalised over all the class constraints and all the type variables of the RHS. But I bet that is not what you want. 4. Would it make a difference if you gave a type signature for f? Can f,g have different sets of class constraints? (H98 says 'no' for class constraints, but 'yes' for type variables, which is an obvious wart). 5. I'm also concerned about the interaction with strictness. let (f,g) = e in f (...f...g...) Here 'f' is clearly used strictly, so the pair will certainly be evaluated. Does this mean the same? case e of (f,g) - f (...f..g...) 6. If we allow bang patterns, what does !(f,g) = e actually mean? The implementation is not the driving force. It's just the way I know that something is afoot. What is the problem MPB tries to solve? The problem of specifying the type system for pattern bindings. Try writing down the full typing rules for pattern bindings, including type signatures! Higher-rank types too. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
Iavor Diatchki wrote: I should also point out that if we were to adopt the MBP rule, we would have to adjust the definition of what pattern bindings mean. For example, I think that this is how things are desugared at the moment: (x,y) = e becomes new_var = e x = case new_var of (v,_) - v y = case new_var of (_,v) - v The report doesn't actually mention this translation although it is widely used to implement pattern bindings, and in some compilers (not GHC) the translation is done before type checking. What's interesting to me is that perhaps this gives us a way to understand what the static semantics of pattern bindings should be, absent MPB. e.g. (x,y) = (negate,show) (Simon's example) translates to z = (negate,show) x = fst z y = snd z and we can see why both x and y end up generalised over both constraints, because z :: (Num a, Show b) = (a - a, b - String) and this also explains why the pattern-bound variables don't have to be generalised over all the type variables. e.g. in z = (id,id) x = fst z y = snd z we'd get z :: forall a b . (a-a, b-b) x :: forall a . a - a not x :: forall a b . a - a because the generalisation step for x only generalises over the type variables in the type arising from its right-hand side. Cheers, Simon It seems that under MBP the second program is not equivalent to the first because it is more polymorphic. -Iavor On Wed, Apr 23, 2008 at 10:32 AM, Simon Marlow [EMAIL PROTECTED] wrote: Folks, The current proposal on the table for what to do about the monomorphism restriction (henceforth MR) is * remove the MR entirely * adopt Monomorphic Pattern Bindings (MPB) Right now, the committee is almost uniformly in favour of dropping the MR, and most of us are coming round to the idea of MPB. Since this area has historically been difficult to achieve a concensus on, I'm excited that we appear to be close to making a decision, and a good one at that! The arguments for removing the MR are pretty well summarised on the wiki: http://hackage.haskell.org/trac/haskell-prime/wiki/MonomorphismRestriction You can read about MPB here: http://hackage.haskell.org/trac/haskell-prime/wiki/MonomorphicPatternBindings GHC has implemented MPB by default (i.e. we deviate slightly from Haskell 98) since 6.8.1. The nice thing about the combination of removing MR and adopting MPB is that we retain a way to explicitly declare monomorphic bindings. These are monomorphic bindings: ~x = e [EMAIL PROTECTED] = e or if you don't mind a strict binding: !x = e. The wiki points out that (x) = e would also be monomorphic, but arguably this is in poor taste since we expect (x) to mean the same as x everywhere. Cheers, Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
Hello, Removing the MR seems reasonable. I am a little less certain about the MPB rule though. I suspect that, as the wiki page points out, many uses of pattern bindings are monomorphic but still, there seem to be a number of examples on the wiki where people have run into this problem. So I am not sure that the conclusion that nobody has noticed the change is valid. I do believe that you can probably work around the problem in many situations but the question in my mind is why should we have to work around stuff when we have a system that already works? In other words, what problem do MBPs solve? I should also point out that if we were to adopt the MBP rule, we would have to adjust the definition of what pattern bindings mean. For example, I think that this is how things are desugared at the moment: (x,y) = e becomes new_var = e x = case new_var of (v,_) - v y = case new_var of (_,v) - v It seems that under MBP the second program is not equivalent to the first because it is more polymorphic. -Iavor On Wed, Apr 23, 2008 at 10:32 AM, Simon Marlow [EMAIL PROTECTED] wrote: Folks, The current proposal on the table for what to do about the monomorphism restriction (henceforth MR) is * remove the MR entirely * adopt Monomorphic Pattern Bindings (MPB) Right now, the committee is almost uniformly in favour of dropping the MR, and most of us are coming round to the idea of MPB. Since this area has historically been difficult to achieve a concensus on, I'm excited that we appear to be close to making a decision, and a good one at that! The arguments for removing the MR are pretty well summarised on the wiki: http://hackage.haskell.org/trac/haskell-prime/wiki/MonomorphismRestriction You can read about MPB here: http://hackage.haskell.org/trac/haskell-prime/wiki/MonomorphicPatternBindings GHC has implemented MPB by default (i.e. we deviate slightly from Haskell 98) since 6.8.1. The nice thing about the combination of removing MR and adopting MPB is that we retain a way to explicitly declare monomorphic bindings. These are monomorphic bindings: ~x = e [EMAIL PROTECTED] = e or if you don't mind a strict binding: !x = e. The wiki points out that (x) = e would also be monomorphic, but arguably this is in poor taste since we expect (x) to mean the same as x everywhere. Cheers, Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: The monomorphism restriction and monomorphic pattern bindings
Hi * remove the MR entirely Finally! * adopt Monomorphic Pattern Bindings (MPB) There are 6 reasons on that page why we shouldn't adopt MPB - of those number 5 I think is particularly compelling. There seems to be 1 main reason to remove it, which is that it has a complex translation to System F. That doesn't seem to be a particularly good reason at all! I'm guessing someone has written the translation so now applying consistently isn't that hard? Having x /= (x) is rather disturbing. Haskell has always had the attitude of doing what suits users, and making implementations work hard to handle the language features. In addition, this is a breaking change. The nice thing about the combination of removing MR and adopting MPB is that we retain a way to explicitly declare monomorphic bindings. These are monomorphic bindings: ~x = e [EMAIL PROTECTED] = e If you really care, add a type signature. Given the tendancy for Hackage packages to have -Wall turned on and all warnings removed in patches (I'm sure half the people on Hackage have had a patch doing that from Gwern) I don't see a top-level type signature as being particularly problematic. In addition, both of those forms are non-obvious ways to declaring something monomorphic, and could easily be cleaned up by someone not appreciating the subtleties of sharing. Thanks Neil ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
