More speed please!

[Simon Peyton-Jones]

I'm not sure how to make progress with this thread (see below).  On the one hand there is an interesting idea here.  On the other, I don't want to put more ad-hoc-ery into GHC.

What this cries out for is a notion of strict function *in the types*.  So if
        f :: !Int -> Int
then you know that f is strict, and you can use call-by-value.  GHC has no such notion at the moment. The bangs in constructors are very specific to constructors, and handled in an ad-hoc way.

Duncan wants to make them more first class, which is good.  But that would mean making !T into a Core type, not just a source-language annotation on data constructors.  Doing this in a systematic way is attractive, but slippery. Ben Rudiak-Gould has spent quite a bit of time thinking about it.  There are many questions; e.g: can ! appear to the right of an arrow?  inside tuples (!a,!b)?  inside lists [!a]?  Can a polymorphic function be called at a bang-type? etc

Anyway, I'm inclined to make haste slowly on this one.  If someone feels like working out the details, the way lies open. Alternatively, the ad-hoc solution might be so important that it's worth implementing despite its ad-hocery.

Simon

| -----Original Message-----
| From: Duncan Coutts [mailto:duncan.coutts at worc.ox.ac.uk]
| Sent: 17 March 2007 07:23
| To: Simon Peyton-Jones
| Cc: glasgow-haskell-users at haskell.org
| Subject: RE: More speed please!
|
| On Fri, 2007-03-16 at 17:49 +0000, Simon Peyton-Jones wrote:
| > | newtype Put a = Put {
| > |         runPut :: (a -> {-# UNPACK #-} !Buffer -> [B.ByteString])
| > |                      -> {-# UNPACK #-} !Buffer -> [B.ByteString]
| > |     }
|
| > Now you are proposing that
| >
| >         data Bar a = MkBar (!a -> a)
| >
| > means this:
| >
| >         MkBar f = :MkBar (\x. x `seq` f x)
| >
| > That is, even if the argument to MkBar is a lazy function, when you take a MkBar apart you'll find a
| strict function.
|
| Right.
|
| And then after this semantic change we can do tricks like changing the
| calling convention of this function so that it takes that strict
| argument as its unpacked components.
|
| > I suppose you can combine the two notations:
| >
| >         data Baz a = MkBaz !(!a -> a)
| > means
| >         MkBaz f = f `seq` :MkBaz (\x. x `seq` f x)
|
| I suppose so.
|
| > Interesting.  Is that what you meant?  An undesirable consequence would be that
| >         case (MkBar bot) of MkBar f -> f `seq` 0
| > would return 0, because the MkBar constructor puts a lambda inside.
| > This seems bad.  Maybe you can only put a ! inside the function type
| > if you have a bang at the top (like MkBaz).
|
| Hmm, yes I see.
|
| Well that seems like a reasonable restriction. In my original example I
| was using newtype rather than data (which of course is like data with !
| on the only component).
|
| Afterall, in practise I think the main use of this semantic change will
| be to take advantage of faster calling conventions and so we'd be
| perfectly happy with being strict in function itself.
|
| Duncan