[Haskell-cafe] Re: If wishes were horses...

[Max Bolingbroke]

On 12 March 2010 10:38, Ketil Malde <ketil at malde.org> wrote:
> What should the type look like?  If memory serves, Clean allows bangs in
> type signatures, something like:
>
>  foldl' :: (a -> b -> a) -> !a -> [b] -> a
>
> but I thought it just added a seq under the hood,

Thats my understanding too.

I did look briefly at this, and I *think* its pretty straightforward
to have a system of segregated strict and non-strict types, with a
type constructor ! which "unlifts" a non-strict type to a strict one.
In this system, the choice of whether to build a thunk at a let
binding / application site is made based on the kind of the bound
thing. You have a kind system like:

k ::= * | ! | k -> k

(* is standard lifted types, ! is unlifted type)

And then the type constructor ! has kind "* -> !". You have to allow
the (->) to have several kinds (a bit of a wart):

(->) :: * -> * Lazy argument, result is enclosed in a thunk at the
call site (unless at focus of evaluation)
(->) :: * -> ! Lazy argument, result is evaluated eagerly at the call site
(->) :: ! -> * Strict argument, result is enclosed in a thunk at the
call site (unless at focus of evaluation)
(->) :: ! -> ! Strict argument, result is evaluated eagerly at the call site

You can then write signatures like this:

eq :: !a -> !a -> Bool

But what do the type quantifiers look like? The only reasonable answer is:

eq :: forall (a :: *). !a -> !a -> Bool

Quantifying over type variables of kind * would have to be the default
to retain backwards compatibility.

This is a bit annoying you will only be able to instantiate any
polymorphic Haskell function at lazy types, unless you explicitly
wrote it with the "strict" type signature explicitly. So you need e.g.
a strict and a non-strict identity function. This seems to really be
necessary because in general the code generated for the two
alternatives won't be the same, so to get true "strictness
polymorphism" you need 2^n copies of the code, where n is the number
of type variables in the signature.

There are probably some tricks you can play to ameliorate this blow up
(strictness "dictionaries" anyone?) but it looks hard.

Nonetheless, I think a system with segregated strict/non-strict types
could be workable and interesting. I heard tell that JHC may have some
prior art in this area..

Cheers,
Max