Re: The dreaded monomorphism restriction

[haskell-request@cs.glasgow.ac.uk]

Date: 31 May 91 15:29
From: haskell-request@cs.glasgow.ac.uk
Sender: Mark.Jones@prg.oxford.ac.uk
To: haskell@cs.glasgow.ac.uk
Subject: Re: The dreaded monomorphism restriction

Original-Via: uk.ac.ox.prg; Fri, 31 May 91 15:16:09 BST


Simon's new proposal for the monomorphism restriction looks as if it will
solve the major problems of the current rule, whilst at the same time being
relatively easy to explain ... and implement.

However, I think we can simplify the proposal even further;  in particular,
I do not think it is necessary to distinguish between recursive and
non-recursive bindings.

To start with, take a look at Simon's statement of the current condition:

|"A variable bound by LET or WHERE is called "unrestricted" if and only if
|
|i) Its binding is non-recursive and
|  a) it is bound by a function binding, or
|  b) it is bound by a pattern binding,
|        and the pattern is a simple variable pattern
|        and the right hand side is a lambda abstraction
|
|                OR
|
|ii) its binding is recursive and all the variables in its mutually-recursive|        group have the property (a) or (b) above.

Note that, if a binding is non-recursive, then its `mutually-recursive'
group contains just a single binding.  And if that is an unrestricted
binding according to this definition then it must have the property (a)
or (b).  In other words, the definition above is equivalent to:

"A variable bound by LET or WHERE is called "unrestricted" if and only if
 each binding in its mutually-recursive group satisfies property (a) or (b)
 where (a) ...
       (b) ...
 ..."


Simon's new proposal is not quite so easy to simplify because it really
does distinguish between non-recursive and recursive bindings:

|"A variable bound by a LET or WHERE is called "unrestricted" if and only if:|
|i) Its binding is non-recursive and
|  a) it is bound by a function binding, or
|  b) it is bound by a pattern binding,
|        and the pattern is a simple variable pattern,
|        and a type signature is given
|
|OR
|
|ii) its binding is recursive and all the variables in its mutually-recursive|        group are bound by function bindings.
|
|The monomorphism restriction ... "
 
Which would allow:    succ :: Num a => a -> a
                      succ  = (+) 1
but not:              ones :: Num a => [a]
                      ones  = 1 : ones
Surely the second definition ought to be allowed, particularly after the
programmer has gone to the trouble of using an explicit type declaration?
 
Once we allow this, then the new proposal can be simplified to:
----------
"A variable bound by a LET or WHERE is called "unrestricted" if and only if:
 
For each binding in its mutually-recursive group is:
   either: a function binding
       or: a pattern binding,
           and the pattern is a simple variable pattern,
           and a type signature is given.
 
The monomorphism restriction ... [as in Simon's original proposal]"
----------
 
Any comments?
 
Mark