Re: [Haskell] MR details (was: Implicit type of numeric constants)

On 23/09/2006, at 4:33 AM, Christian Sievers wrote:
Hello,
I don't take my advice to go to haskell-cafe :-)
I will take your advice :)
The discussion continued outside the mailing list, and now I have two questions myself:
1. Why do the rules of the monomorphism restriction explicitly mention *simple* pattern bindings? Where is the difference, especially as there is a translation to simple pattern bindings? Why should
p | "a"=="b" = 2 | otherwise = 3
be treated different than
p = if "a"=="b" then 2 else 3
They are the same (both are simple pattern bindings). The report says in section 4.4.3.2 that the first can be translated into the second. A simple pattern binding is one where the lhs is a variable only. If a pattern binding is not simple, it must have a data constructor on the lhs, therefore it cannot be overloaded. So the (dreaded) MR only applies to simple pattern bindings. Cheers, Bernie.

On 9/23/06, Bernie Pope
If a pattern binding is not simple, it must have a data constructor on the lhs, therefore it cannot be overloaded. So the (dreaded) MR only applies to simple pattern bindings.
I thought it was simple pattern bindings that could be *exempted* from the MR by supplying an explicit type signature, while non-simple pattern bindings are always subject to it. Mike

On 24/09/2006, at 1:46 AM, Michael Shulman wrote:
On 9/23/06, Bernie Pope
wrote: If a pattern binding is not simple, it must have a data constructor on the lhs, therefore it cannot be overloaded. So the (dreaded) MR only applies to simple pattern bindings.
I thought it was simple pattern bindings that could be *exempted* from the MR by supplying an explicit type signature, while non-simple pattern bindings are always subject to it.
Actually, I realised after I posted my message that what I wrote was dubious. I'm sorry about that, please ignore it. This section from the Report seems to clear things up: In "Motivation", section 4.5.5: "Rule 1 prevents ambiguity. For example, consider the declaration group [(n,s)] = reads t Recall that reads is a standard function whose type is given by the signature reads :: (Read a) => String -> [(a,String)] Without Rule 1, n would be assigned the type forall a. Read a =>a and s the type forall a. Read a =>String. The latter is an invalid type, because it is inherently ambiguous. It is not possible to determine at what overloading to use s, nor can this be solved by adding a type signature for s. Hence, when non-simple pattern bindings are used (Section 4.4.3.2), the types inferred are always monomorphic in their constrained type variables, irrespective of whether a type signature is provided. In this case, both n and s are monomorphic in a." Sorry for the confusion, Bernie.

Bernie Pope answered:
1. Why do the rules of the monomorphism restriction explicitly mention *simple* pattern bindings? Where is the difference, especially as there is a translation to simple pattern bindings? Why should
p | "a"=="b" = 2 | otherwise = 3
be treated different than
p = if "a"=="b" then 2 else 3
They are the same (both are simple pattern bindings). The report says in section 4.4.3.2 that the first can be translated into the second.
Indeed, I meant to allude to this translation.
A simple pattern binding is one where the lhs is a variable only.
That's consistent with the second reason for rule one of the MR. However, the mentioned section 4.4.3.2 defines it differently: A simple pattern binding has form p = e. And if there is any doubt about what p stands for, it goes on: The pattern p ... Contrasting to that: The general form of a pattern binding is p match, where a match is the same structure as for function bindings above; in other words, a pattern binding is: p | g1 = e1 | g2 = e2 ... | gm = em where { decls } So according to this definition, a pattern binding is simple iff there are no guards (unless they are in the expression). Also the translation to a "simple pattern binding" only gets rid of guards. So there seems to be an error in the report, which can be fixed by either redefining "simple pattern binding", or using a differnet description in the MR. Bye Christian Sievers

On 26/09/2006, at 12:19 AM, Christian Sievers wrote:
Bernie Pope answered:
1. Why do the rules of the monomorphism restriction explicitly mention *simple* pattern bindings? Where is the difference, especially as there is a translation to simple pattern bindings? Why should
p | "a"=="b" = 2 | otherwise = 3
be treated different than
p = if "a"=="b" then 2 else 3
They are the same (both are simple pattern bindings). The report says in section 4.4.3.2 that the first can be translated into the second.
Indeed, I meant to allude to this translation.
A simple pattern binding is one where the lhs is a variable only.
That's consistent with the second reason for rule one of the MR.
However, the mentioned section 4.4.3.2 defines it differently:
A simple pattern binding has form p = e.
And if there is any doubt about what p stands for, it goes on:
The pattern p ...
Contrasting to that:
The general form of a pattern binding is p match, where a match is the same structure as for function bindings above; in other words, a pattern binding is:
p | g1 = e1 | g2 = e2 ... | gm = em where { decls }
So according to this definition, a pattern binding is simple iff there are no guards (unless they are in the expression). Also the translation to a "simple pattern binding" only gets rid of guards.
So there seems to be an error in the report, which can be fixed by either redefining "simple pattern binding", or using a differnet description in the MR.
Aha, Christian I see what you mean. It seems I did not read section 4.4.3.2 carefully. In fact I think I was interpreting that section in light of the MR. So I am now as puzzled as you are. Anyway, thanks for persisting on this point. Cheers, Bernie.

My understanding of the MR is heavily influenced by the work I did on Hatchet, which is based directly on Mark Jones' paper (and code) "Typing Haskell in Haskell". I thought I would go back to that paper and see how he defines "simple" pattern bindings and the MR. I now quote directly from the relevent sections of the paper: He represents function bindings with the Alt type, which is defined on page 9:
"The representation of function bindings in following sections uses alternatives, represented by values of type Alt :
type Alt = ([Pat], Expr)
An Alt specifies the left and right hand sides of a function definition."
On page 12 he defines what simple means with repsect to the Alt type and the MR:
"A single implicitly typed binding is described by a pair con- taining the name of the variable and a list of alternatives:
type Impl = (Id , [Alt])
The monomorphism restriction is invoked when one or more of the entries in a list of implicitly typed bindings is simple, meaning that it has an alternative with no left-hand side patterns.
restricted :: [Impl] -> Bool retricted bs = any simple bs where simple (i, alts) = any (null . fst) alts "
Curiously, his Alt type does not offer any way to represent pattern bindings where the lhs is a non-variable pattern. But he addresses this point later on page 13:
"In addition to the function bindings that we have seen al- ready, Haskell allows variables to be defined using pattern bindings of the form pat = expr . We do not need to deal di- rectly with such bindings because they are easily translated into the simpler framework used in this paper. For example, a binding: (x,y) = expr can be rewritten as: nv = expr x = fst nv y = snd nv where nv is a new variable. The precise definition of the monomorphism restriction in Haskell makes specific refer- ence to pattern bindings, treating any binding group that includes one as restricted. So, at first glance, it may seem that the definition of restricted binding groups in this pa- per is not quite accurate. However, if we use translations as suggested here, then it turns out to be equivalent: even if the programmer supplies explicit type signatures for x and y in the original program, the translation will still contain an implicitly typed binding for the new variable nv."
It is not obvious that this is consistent with the Report; I'll have to think about it more. Cheers, Bernie.
participants (3)
-
Bernie Pope
-
Christian Sievers
-
Michael Shulman