wiki:MonomorphicPatternBindings

Version 10 (modified by simonpj@…, 7 years ago) (diff)

--

Make pattern bindings monomorphic

The Proposal

I propose that we make all pattern bindings completely monomorphic (regardless of type signatures). As a result, the expression

  let (p,q) = (\x -> x, True) in (p True, p 'c')

would fail to typecheck, because it requires p to be polymorphic. The program would be rejected even if p had a type signature:

  let { p :: a -> a
      ; (p,q) = (\x -> x, True) 
  } in (p True, p 'c')

We need to be precise about what a "pattern binding" is. Definition: a pattern binding has the form pat=rhs, where pat is not simply a variable. Examples:

  (x,y) = e    -- Pattern binding
  [x]   = e    -- Pattern binding
  (x)   = e    -- Pattern binding
  x@y   = e    -- Pattern binding
  ~x    = e    -- Pattern binding

  x     = e    -- NOT a pattern binding

This rule is simple and easy to remember.

Notice that enclosing the variable in parens, thus (x)=e, makes it a pattern binding, and therfore forces it to be monomorphic. So this is a way to get the monomorphic form of binding that John Hughes has, at times, argued for.

Another way to say it is this: only function bindings are generalised, where a function binding has the form

f p1 ... pn = e

where n>=0. The n=0 case is a bare variable.

Discussion

At the moment you can say

	let (f,g) = e in ...

and get *polymorphic* values f,g. This causes a good deal of trouble in the implementation (think of what the System F translation looks like), and it's an odd thing to do. Why odd? Well here it's fine:

	data T = C (forall a. a->a)
	h x = let C f = e in ...

Constructor C has a polymorphic argument, so we can match e against (C f) and get a polymorphic function. But in the first example, (,) only takes monomorphic arguments, so we have to generalise after selection. To put it another way, even if the "..." is definitely strict in f, we cannot transform to

	case e of (f,g) -> ...

So this proposal makes the bang-pattern proposal easier to describe http://hackage.haskell.org/trac/haskell-prime/ticket/76

Experiment

In July I changed GHC (the HEAD) to make pattern bindings monomorphic by default. (A binding of a simple variable is not considered to be a pattern binding.) The flag -fno-mono-pat-binds restores the standard behaviour. I deliberately made the new behaviour the default so that I'd hear of any breakage.

The interesting observation is this: all of the libraries compile without a tremor, and I have received only two messages remarking on the new behaviour.

First message

Ross Paterson sent me this code

import Control.Monad.ST

newtype ListMap m a b = ListMap ([a] -> m [b])

runMap :: (forall s. ListMap (ST s) a b) -> [a] -> [b]
runMap lf as = runST (f as)
	  where ListMap f = lf

This no longer works because f isn't polymorphic, and runST needs it to be. It's easily fixed:

runMap lf as = runST (f as)
	  where f = case lf of { ListMap f -> f }

Comment: A polymorphic pattern binding isn't required in the above example, but the original code seems more elegant. Why not make monomorphism the default and permit polymorphism only when there is an explicit type signature on the binding?

Second message

Tristan Allwood (tora at doc.ic.ac.uk) said this. I was recently bitten by the fact pattern bindings are monomorphic; admitadly I'm writing code to learn about theoretical typing issues and nothing mainstream/production; but (as I hope my ghci session should illustrate) the cause of the problem is difficult to isolate if you're not aware of the property (which I wasn't until Igloo on #haskell pointed me this way);

  Prelude> :m +Data.Maybe

  Prelude Data.Maybe> let f = (fromJust (Just id)) in (f 3, f False)
  (3,False)

  Prelude Data.Maybe> let (Just f) = (Just id) in (f 3, f False)

  <interactive>:1:31:
      No instance for (Num Bool)
        arising from the literal `3' at <interactive>:1:31
      Possible fix: add an instance declaration for (Num Bool)
      In the first argument of `f', namely `3'
      In the expression: f 3
      In the expression: let (Just f) = (Just id) in (f 3, f False)

Ok, fine: except the reported type signatures are the same vis:

  Prelude Data.Maybe> :t let f = (fromJust (Just id)) in f
  let f = (fromJust (Just id)) in f :: forall a. a -> a

  Prelude Data.Maybe> :t let (Just f) = (Just id) in f
  let (Just f) = (Just id) in f :: forall a. a -> a

And just to cap it off, adding a layer of indirection...

  Prelude Data.Maybe> let q = ( let (Just f) = (Just id) in f ) in (q 3, q False)
  (3,False)

Simon's comment: yes, I guess this is a bit confusing. But the same will happen in H98 if the type of f was overloaded. And the example seems quite contrived.

Third report

Koen found this: http://hackage.haskell.org/trac/ghc/ticket/1369

Fourth report

Ron de Bruijn (rmbruijn@…) reported:

  [set_left_child_leaf, set_right_child_leaf] = map set_gen_child_leaf [l, r]

Here "l" and "r" are functions that get the left and right child of a tree and set_gen_child is a function generalized over the type of child being selected.

The above doesn't work on GHC 6.6.1. I get

    Cannot match a monotype with `forall s
                                         a
                                         (chain :: * -> * -> *)
                                         (m :: * -> *).
                                  STRef s (Node s a chain) -> m ()'

The only other sane way to get this working is to unroll the map by hand.

Fifth report

Matthew Naylor (mfn@…) writes: SparseCheck uses polymorhpic pattern bindings. For example, a SparseCheck datatype for lists is written as

  (nil :- (|>)) = datatype (ctr0 [] \/ ctr2 (:))

This introduces two functions with types

  nil  :: Term [a]
  (|>) :: Term a -> Term [a] -> Term [a]

Without polymorphic pattern bindings, we would have to write something like:

  nil = ctr0 0 []
  (|>) = ctr2 1 (:)

Notice that I must give each constructor a unique identifier manually.

Summary

My conclusion: polymorphic pattern bindings is a feature that is virtually never used, and not even necessary then. We should nuke them.