Haskell-prime Digest, Vol 1, Issue 4

[John Hughes]

Ross Paterson wrote:

> I suggest = for bind-by-name, and
> := for bind-by-need. 
> ...
  


You're proposing that the =/:= distinction both decides whether
constrained type variables are monomorphic and whether the binding
should be implemented using sharing.  If it only did the former (and the
expectation was that all pattern bindings with unconstrained types used
sharing), then existing legal programs would still be legal, and the
examples that currently trip over the MR would be legal but inefficient.
(Also, what does the shared/unshared distinction mean for functions?)

  

Not just constrained type variables. All type variables. Because changes 
in the program
elsewhere can easily change the status of a type variable from 
unconstrained to constrained,
thus triggering monomorphism unexpectedly--that was the point of my 
comment about
introducing an equality test in a function called from the definition. 
Changing the status
of a type variable should not change the way it is treated by any 
replacement for the M-R.

I don't quite follow what you're suggesting above. The main point of a 
=/:= distinction is
to distinguish between sharing and non-sharing, isn't it? And sharing 
means you have to
be monomorphic, at least for constrained type variables, and (by the 
argument above)
thus for unconstrained ones too. How can sharing/unsharing and 
monomorphic/overloaded
be separated?

I'd really like to avoid ANOTHER rule that "guesses" what method to use, 
based on the
form of the definition (your reference to pattern bindings above). That 
leads to surprises
for the programmer, at least the less-than-expert one, when a definition 
is replaced by
something that LOOKS equivalent, but type-checking or sharing suddenly 
behaves
differently. Much preferable is a simple and obvious rule: = means 
unshared and
polymorphic, := means shared and monomorphic.

Shared/unshared doesn't matter for function definitions, but 
monomorphic/polymorphic
can still be important. There is an interaction with implicit parameters 
here--which I
suppose might make it into Haskell'. A := definition says: resolve all 
overloading here.
Thus, if there is an implicit parameter in the RHS of such a definition, 
then it refers
to the instance of that parameter in scope at the point of definition. 
With a = definition,
it refers to the instance in scope at the point of use. This is an 
important distinction
whether you're defining a function or anything else. This is discussed 
in my paper
on Global Variables in Haskell, which suggested using implicit 
parameters to refer
to global variables, rather than an unsafe unsafePerformIO applied to a 
newIORef.

What if one has mutually recursive bindings, some using = and some := ?
Does monomorphism kick in if some of the variables in a binding group
use :=, or would we just require that all bindings in the same group
use the same binder?  (At first I couldn't see why one would ever use :=
with function bindings, but perhaps that's the reason.)

  

I don't think there's really a problem in allowing a mixture of = and := 
in the same
mutually recursive group, even if it could be quite confusing to do so! 
= just means
that type variables and dictionaries should be abstracted, and that the 
binding
should be by-name... let's assume that we're translating to System F, 
and we always
insert at least a \()-> on such bindings in the translation. := means, 
on the other hand,
that type variables and dictionaries are not abstracted, and so must be 
inherited from
an enclosing scope. So in a group of the form

    f = ...g...
    g := ...f...

then any type variables in the definition of g must refer to the 
enclosing scope, which
means that they cannot be generalised in the definition of f either 
(since they are
"free in the context"). But if there are type variables in the 
definition of f which do
NOT occur in the type of g, then they can be generalised as usual. 
Meanwhile f can
be bound by name, and g by need--there's no difficulty with that. This 
would be an
odd thing to do, but I think it makes perfect sense. (I wonder what 
happens today,
if you write mutually recursive definitions where the M-R applies to 
some, but
not others?)

Of course, polymorphic recursion would REQUIRE an = binding, but that 
shouldn't
surprise anybody.

John