Re: Monomorphism

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

Date: 29 May 91 22:55
From: haskell-request@cs.glasgow.ac.uk
Sender: Joe Fasel <jhf@c3serve.c3.lanl.gov>
To: haskell <haskell%cs.yale.edu@yalevm.ycc.yale.edu>
Cc: brian@c3serve.c3.lanl.gov
Subject: Re: Monomorphism

Original-Via: uk.ac.nsf; Wed, 29 May 91 22:38:13 BST
Original-Sender: jhf <jhf%gov.lanl.c3.c3serve%edu.yale.ycc.yalevm%edu.yale.cs@yale.edu>

| From: john peterson <peterson-john%CS.YALE.EDU@yalevm.ycc.yale.edu>
|
| This is a serious problem that really needs to be addressed in the
| type inference algorithm.  The only short term possibilities that seem
| practical are to either leave this alone or Joe's #2 approach: use
| type signatures as a syntactic marker to indicate non-monomorphic
| bindings.  His #1 proposal to drop monomorphism completely is not
| practical since it leads to unresolvable ambiguity problems.

I'm not aware of any overloading ambiguity that the monomorphism
restriction solves.  Could you please elaborate, John?

| I think Joe over-simplifies the issue by bringing up the re-evaluation
| aspect.  The real issue has to do with the semantics of the definition
| mechanism.

Well, as I understand it, re-evaluation was exactly the reason that
John Hughes proposed the monomorphism restriction.  It is to avoid an
apparent loss of full laziness.

| Consider the following:
|
| x = exp
| y = ... x ...
| z = ... x ...
|
| We would expect x to be bound to exactly the same value in both y and
| z; this is the heart of the monomorphism argument.  Without it, there
| is no way to be sure that the two references to x yield the same
| value.  This is what leads to ambiguity and loss of a fundamental
| abstraction property.

On the contrary, I would say that it is the monomorphism restriction
that interferes with the principle of abstraction.  Consider
the following

	y = sin (pi / 4) + 1
	z = 15 `div` 4 + 1

If x is bound nonmonomorphically, the following is equivalent:

	x = 1
	y = sin (pi / 4) + x
	z = 15 `div` 4 + x

but the type of x cannot be resolved if x must be bound monomorphically.

| To really debate this topic, we need to make this proposal more
| concrete.  Let me try to formalize Joe's proposal:
|
| A definition without a type signature is monomorphic (status quo).
| A variable with a type signature can be non-monomorphic if the
| signature attached allows.  The interpretation of non-monomorphic
| binding is the same as if the () hack had been used in the definition
| and all references.  Thus:
|
| indices :: (Ix a) => Array a b -> [a]
| indices = range . bounds
| y = indices x
|
| would be treated as
|
| indices = (range . bounds) ()
| y = (indices ()) x

I don't see how this is a useful formalization of our proposal.  (I thought
it was originally yours, by the way--apologies if I've misrepresented
your earlier suggestion.)  We are simply saying that the syntactic
indicator of a nonmonomorphic binding is a type binding with a context,
rather than a value binding that is evidently a function definition.
By no means would I want to say that this is the same as making everything
a function over the unit type and doing all those applications to (),
although the final result is the same.

| The effect of this on more complex pattern bindings is less clear.
| Consider the following:
|
| (f,g) = ((+),(*))
| f :: Num a => a -> a -> a
| g :: Num a => a -> a -> a
|
| So do we also want to deal with this case?  If so, how?


Yes, each of those type bindings would be needed to make the value
binding fully nonmonomorphic.  (What an awkward phrase! It's unfortunate
that "monomorphic" for us is not for us the opposite of "polymorphic".)
Such an example does serve to illustrate why I prefer just eliminating
the monomorphism restriction, though.

| Here's some objections:
| 1.  We're trying to use one notation for two different kinds of
| definition.  This `explicit signature' solution is not at all obvious
| and looks like a hack.

I'll accept that it's a hack.  So is the monomorphism restriction itself.
So, certainly is  cmPerInch () = 2.54 .  I do think our proposal is more
intuitively reasonable, however, in light of John Hughes's original
motivation for proposing the restriction:  to avoid the nasty surprise
that an innocent-looking definition is in fact overloaded, and thus
subject to re-evaluation, depending upon the context and the cleverness
of the compiler.  It is reasonable because the explicit type binding
says that the programmer knows about the overloading.

| 2.  The underlying problem is still there; the deeper issues have been
| ignored.

The deeper issues would seem to be about whether one wants overloading
or not and whether it is reasonable to regard this as an extension
of Hindley-Milner polymorphism.  We are pretty-much committed to this
at this stage.  In other words, an variable's being used at different
overloadings in different places is not very different from its being
used at different polymorphic instances.

| 3.  The eta conversion that this avoids is not that difficult or ugly.

I strongly disagree with this statement, for the reasons I have
previously given:  I want to encourage higher-order programming,
and discouraging eta-reduction is harmful to this cause.

--Joe (with Brian)