On 16 April 2004 12:26, Alastair Reid wrote:

What I'd like to see is a general facility for defining strict types. That is, types whose values will never be thunks so let binding causes evaluation (as in ML) and use as a subexpression (which is not under a lambda) causes evaluation (as in ML). The GHC syntax seems too restrictive for this. Maybe something like this:

strict_data Int# = Int# Int -- declare a strict Int type

The typechecking issues would be the same as for GHC's unboxed types: there are two kinds of typevar * and # and never the twain shall meet. (I think GHC plays some neat tricks to ease the pain of this restriction?)

Yes, GHC has a separate kind for unlifted types. Unlifted types have kind #, so you can't pass something of unlifted type to a polymorphic function or store it in a polymorphic data structure, because ordinary type variables have kind *. I think there's a small superkind relationship, so kind *# is a superkind of both * and #, which is useful for things like the return type of 'error'. Do you want your strict types to be truly unlifted? GHC could usefully take advantage of that knowledge.

A semantically correct (but maybe a bit slow) implementation would be easy enough:

1) let-bind all strict non-atomic subexpressions. 2) float strict variable bindings out to nearest enclosing lambda (float out any lazy variable bindings if required) 3) Use 'seq' to force all the strict var thunks.

For example:

insert :: a -> (Int#,[a]) -> (Int#,[a])

insert x (cnt,xs) = (cnt+1,x:xs) ===> insert x (cnt,xs) = let cnt'=cnt+1 in seq cnt' $ (cnt',x:xs)

You have some kind of implicit coercion between Int and Int#. How does the type system work here? In GHC you can't put Int# in a pair, of course. Cheers, Simon