| 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

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 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/MonomorphicPatternBinding...

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 x@_ = 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

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 x@x /= 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 x@y 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 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

Hi, On Mon, Apr 28, 2008 at 9:42 AM, 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.

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

Ian Lynagh wrote:

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?

Right. In the absence of the MR, we need a way to say precisely what polymorphic overloaded pattern bindings mean, and the translation does just that. Cheers, Simon

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