monomorphic pattern binding

[john peterson <peterson-john@cs.yale.edu>]

Original-Via: uk.ac.nsf; Thu, 6 Sep 90 20:30:44 BST
Date: Thu, 6 Sep 90 15:10:05 EDT
From: john peterson <peterson-john@cs.yale.edu>
To: Haskell@cs.yale.edu
Subject: monomorphic pattern binding
Sender: haskell-request@cs.glasgow.ac.uk

Amir Kishon & I are trying to start a crusade against the `pattern
binding law'.  Our general feeling is that this law is a severe
impediment to using Haskell which has very limited benefits.
Amir is on vacation so I have edited the following, which is mostly Amir's.

Page 34 of the Haskell Report:

  "Variables not bound directly to a lambda abstraction may be
  polymorphic and overloaded, but must also obey the rule: variables not
  bound directly to lambda abstractions must not be used at more than
  one distinct overloading."

Unfortunately, this law introduces some unanticipated problems.  The
following note considers some of these problems, and discusses some
alternate avenues for solutions.  The intent is to stir up a
discussion on the merits/inadequacy of this law.

Here is a check list of some of the problems which we have perceived.
We would like to thank Kevin Hammond who provided us with his own
insights about the problem. Some of the following points are based on
his note "Monomorphic Pattern Bindings in Haskell".


Monomorphic pattern binding makes functions second class objects
----------------------------------------------------------------

With the introduction of this law, one can not package functions in 
data structures without possibly rendering them monomorphic. We
consider this as a major flaw since we believe that the use of
functions as any other value should be encouraged rather than
discouraged.

Implementing Haskell dictionaries (used in the class system), we need
to create constant tuples of functions.  If this is done at the source
level, a definition of the sort "dict = (f1,f2,f3 ...)" is created.
Unfortunately, this law will render the f's monomorphic.  As
implementors, we can make this a special case in type inference to
avoid this problem, but we feel this a symptom of a more serious
problem.  In fact, even some very simple idioms will not work as
expected.  A simple definition like

op = (+)

will fail due to this law.  While "op x y = x + y" will work (since the
top lambda is present), this is not as simple or clear.


Source to source transformations again suffers a blow
-----------------------------------------------------
Consider:

(f,g) = (\x. x + x, \y. y - y)
 
According to this law f and g are monomorphic. A valid
transformation, like:

f = \ x -> x + x
g = \ y -> y - y

would render these functions polymorphic. This means that some 
source to source transformation are now invalid.

Another example pointed out by Kevin:

f = fromInteger 1 :: Num a => a
f = t :: Num a => a where t = fromInteger 1

In Kevin's words, "The transformation introduces an error. Since t has
type (Num a) => a, rather than "forall a . Num a => a", the type
signature "forall a. Num a => a" is too general. The type of
fromInteger 1 is "forall a . Num a => a", so this would have checked
correctly."

One may also claim that Hindley-Milner type system prohibits some
source to source transformation, namely, the translation of a let
clause to a lambda expression. We argue that in any case such limitations 
are undesirable.  Furthermore this rule adds to the previous
limitations.  Finally, it seems like the consequences to source
transformations of this law are not yet fully understood.

Soundness and Completeness?
---------------------------

Recall that the correctness and completeness proof for Haskell system
is based on the assumption that any Haskell program w/ classes can be
translated to an equivalent class'less program typeable by
Hindley-Milner W algorithm.  We are not so sure that the introduction
of monomorphism to Hindley Milner type system is sound or complete in
respect to HM soundness and completeness. This deserves a proof.

Conceptual burden on the programmer
-----------------------------------

It is clear that the Haskell type system is much more complex than
previous type systems (LML, Miranda etc.).  To this end this type
system has not been tested in "real" use.  That is why we believe that
optimization issues should be deferred until we can fully understand
classes.



For the rest of this note we discuss how we can achieve almost the
same optimizations without this law.  Note that we do not claim that
these solutions are the best solutions they just provide a different 
direction.

Alternate solutions
-------------------

Top level monomorphism is clearly unnecessary since a type signature
can solve the problem. This does not harm the generality of the
current solution because type signatures can be parameterized with
type synonyms.  If efficiency is felt to be a serious problem, the
compiler could (optimally) issue warnings about top level objects.
For top level constants, it is not clear that efficiency is much of a
consideration anyway since these can easily be directly integrated.
Also, if the user explicitly provides a type signature for a variable,
such as

x :: (Num a) => a -> a -> a
x = (+)

what is the advantage of making this illegal?  The point of this law
should be to avoid unintended inefficiency, not to limit the
expressive power of the langiage.


As for local monomorphism, a typical example is:

f x = (y,y) where y = factorial 1000

Two possible solutions are based on unifying both types either
by a type signature or by a "unifying function" and then use 
common sub-expression elimination to optimize.

1. One can unify both types using a "unifying" function:

u :: (a,a) -> (a,a)
u (x,y) = (x,y)

Thus:

f x = u(y,y) where y = factorial 1000

2. Another possibility is to relax the constraint on type signatures
which says:

   "it is illegal to give a type signature for a variable bound in an
   outer scope"

and then supply the type signature to the code, as we done with top
level monomorphism:

f x = (y,y)::(a,a) where y = factorial 1000

[I don't believe this is currently illegal -- John]

Finally, common subexpression elimination (w/ partial evaluation) in
both cases should eventually change the translated code to something
similar to the optimization implicated by the pattern binding law.
Furthermore, this solution is more general since it does not prevent
the programmer from deciding that he wishes both elements to be of
different types.

Again, this solutions are not meant to replace the above rule; the
intention is to point to some other possible avenues for a solution.



As a final note, we believe that the efficiency we gain by the pattern
binding typing law is far less substantial than the eventual
complications to Haskell.  As we understand, this law came up mainly
to solve efficiency problems.  If this is the case, it might be better
to experiment "off-line" with such rules and compare their
effectiveness to other automatic compile-time optimization techniques
rather then putting it "on-line" in the standard.

Any comments would be greatly appreciated,

-amir and John