Implementation plan for top-level unlifted bindings in Core
See also
1. The opportunity
Currently Core does not allow a top-level binding to have an unlifted type, with the sole
exception of top-level string literals. See Note [Core letrec invariant]
in GHC.Core.
There are a couple of reasons for this:
-
Unboxed values are, well, unboxed. So they can't live at the top level of a compiled binary. Example:
module M where { f :: Float# = 3.0# } module X where { import M; main = print (foo f) }
Here
f :: Float#
should be represented by an unboxed floating point number. But in the compile M it would presumably be a pointer to a statically allocated float. Maybe do-able, but woudl be real work. -
If the RHS of the binding is not a head-normal form, we'd need to do startup-time initialisation to evalute these bindings. Exampe:
module M where { n :: Int# = factorial 3# }
We'd need to compute
factorial 3#
eagerly, because anInt#
cannot be represented by a thunk.
However, now that we have boxed, unlifted data types, it's a shame that we cannot allow
data T :: UnliftedType = Nil | Cons Int# T
myT :: T
myT = Cons 3# myT1
myT1 :: T
myT1 = Cons 4# Nil
These are simply static data structures. Why not allow them at top level?
2. The proposal
The proposal is to loosen the invariants on Core for top level bindings, as follows:
- Allow a top-level binding for a boxed unlifted type if it is fully static.
A top-level binding is fully static if it is the application of a data constructor (worker) in which:
- every argument is trivial (a type, literal, coercion, or variable), and
- if an argument is a variable
v
, and that argument is marked strict in the data con declaration, thenv
is also fully static. (See 3.2 and 3.3 below.)
Note that Ids from another module are not considered fully static. (If we exported LFInfo we could make this more liberal. But even then we need to watch out for bindings imported from hs-boot files and perhaps backpack signatures.)
For now at least, this proposal applies only to Core; but in the future one could imagine allowing it source Haskell.
3. Implementation considerations
But how do we compile this subset? We want to avoid generating bindings with entry code; the Cmm closures we generate should be fully realized at compile time. To achieve that we can perform a kind of ANF transformation which gives each constructor in the nested expression its own binding. In STG all these bindings will be trivial applications of data constructors, which can be compiled to Cmm with cgTopRhsCon which emits the fully realized closures we want. Concretely, it should behave the similar to how lifted top-level data constructors are currently compiled:
data Nat = Zero | Succ Nat
x = Succ (Succ Zero)
Which produces this Cmm:
[section ""data" . Zero_closure" {
Zero_closure:
const Zero_con_info;
}]
[section ""data" . x1_rzL_closure" {
x1_rzL_closure:
const Succ_con_info;
const Zero_closure+1;
const 3;
}]
[section ""data" . x_closure" {
x_closure:
const Succ_con_info;
const x1_rzL_closure+2;
const 3;
}]
3.1 Pointer tagging
There is one wart related to tag info which we must be wary of. If a pattern matching unlifted bindings requires tag info, but that might not be available if the match and binding are in separate modules and optimizations are disabled (or perhaps even a certain flag is set).
It is not obvious how that could happen, because unlifted top-level bindings are still not allowed in the source language (but we do have plans to allow it in the future) which means you can't export or import them from modules. However, I believe a lifted wrapper function could get inlined across a module boundary which then introduces such a problematic cross-module pattern match.
In such cases we must ensure that tag info is always available. I currently think that will be the case, because inlining requires enabling optimizations which in turn will ensure tag info is available. But maybe there are still ways this could happen inadvertently. In such cases we could disallow these top-level unlifted bindings.
3.2 Strict arguments (and pointer tagging)
A second wrinkle concerns missing tag info on banged lifted arguments of unlifted data types. Consider this program:
type Box :: UnliftedType -> Type
data Box a = Box a
type UMaybe :: Type -> UnliftedType
data UMaybe a = UJust !a | UNothing
{-# OPAQUE y #-}
y :: Int
y = sum [0..100]
x :: Box (UMaybe Int)
x = Box (UJust y)
Suppose we were to float that UJust y
to the top level. We get this:
y :: Int
y = sum [0..100]
x2 :: UMaybe Int
x2 = UJust y
x1 :: Box (UMaybe Int)
x1 = Box x2
x :: Box (UMaybe Int)
x = case y of { I# _ -> x1 } -- This eval is added by the wrapper for `UJust`
We have an invariant, established by the STG-rewrite pass, that the strict arguments of a
data constructor are always properly tagged. The STG-rewrite pass adds an eval to x2
thus:
x2 :: UMaybe Int = \r [] case y of y' { __DEFAULT -> UJust [y']; };
x1 :: Box (UMaybe Int) = Box! [x2];
x :: Box (UMaybe Int) = \u [] case y of { I# _ -> x1<TagProper>; };
And now x2
is no longer a data-constructor application, disobeys the invariant of Section 2.
To avoid this, we currently only allow floating out unlifted data constructor workers if their strict arguments are fully static, which guarantees they won't be expanded in Stg.
3.3 Transitively check lifted strict arguments
It is necessary to transitively check the fully static property for lifted strict arguments of data constructors. That is because those arguments can themselves have strict arguments which therefore may need to be expanded in Stg. For example consider this program:
data S a = MkS !a -- Lifted
data T a :: UnliftedType = MkT !a
t :: T (S Int)
t = MkT s
s :: S Int
s = MkS y
y :: Int
y = factorial 200
The t
binding is a top-level unlifted binding. At first glance, it seems to satisfy the conditions for being fully static. However, it uses the variable s
in its strict argument, so it will be expanded in Stg as follows:
s = case y of y' -> MkS y'
And in turn this would cause t
to be expanded:
t = case s of s' -> MkT s
Which is problematic. To avoid this we have formulated the invariant such that we only allow top-level unlifted bindings if strict arguments are themselves also fully static, transitively.