The OCaml runtime assumes for type-directed optimizations that all types are "separable". A type is "separable" if either all its inhabitants (the values of this type) are floating-point numbers, or none of them are.
(Note: This assumption is required for the dynamic float array optimization; it is only made if Config.flat_float_array is set, otherwise the code in this module becomes trivial -- see
This soundness requirement could be broken by type declarations mixing existentials and the "
@@unboxed" annotation. Consider the declaration
type any = Any : 'a -> any [@@unboxed]
which corresponds to the existential type "exists a. a". If this type is allowed to be unboxed, then it is inhabited by both
float values and non-
float values. On the contrary, if unboxing is disallowed, the inhabitants are all blocks with the
Any constructors pointing to its parameter: they may point to a float, but they are not floats.
The present module contains a static analysis ensuring that declarations annotated with "
@@unboxed" can be safely unboxed. The idea is to check the "separability" (in the above sense) of the argument type that would be unboxed, and reject the unboxed declaration if it would create a non-separable type.
Checking mutually-recursive type declarations is a bit subtle. Consider, for example, the following declarations.
type foo = Foo : 'a t -> foo [@@unboxed] and 'a t = ...
Deciding whether the type
foo should be accepted requires inspecting the declaration of
'a t, which may itself refer to
foo in turn. In general, the analysis performs a fixpoint computation. It is somewhat similar to what is done for inferring the variance of type parameters.
Our analysis is defined using inference rules for our judgment
Def; Gamma |- t : m, in which a type expression
t is checked against a "mode"
m. This "mode" describes the separability requirement on the type expression (see below for more details). The mode
Gamma maps type variables to modes and
Def records the "mode signature" of the mutually-recursive type declarations that are being checked.
The "mode signature" of a type with parameters
('a, 'b) t is of the form
('a : m1, 'b : m2) t, where
m2 are modes. Its meaning is the following: a concrete instance
(foo, bar) t of the type is separable if
foo has mode
bar has mode
Exception raised when a type declaration is not separable, or when its separability cannot be established.
type mode = Types.Separability.t =
Sep("separable") characterizes types that are indeed separable: either they only contain floating-point values, or none of the values at this type are floating-point values. On a type parameter, it indicates that this parameter must be separable for the whole type definition to be separable. For example, the mode signature for the type declaration
type 'a t = 'ais
('a : Sep) t. For the right-hand side to be separable, the parameter
'amust be separable.
Ind("indifferent") characterizes any type -- separable or not. On a type parameter, it indicates that this parameter needs not be separable for the whole type definition to be separable. For example,
type 'a t = 'a * booldoes not require its parameter
'ato be separable as
'a * boolcan never contain
floatvalues. Its mode signature is thus
('a : Ind) t.
Finally, the mode
Deepsep("deeply separable") characterizes types that are separable, and whose type sub-expressions are also separable. This advanced feature is only used in the presence of constraints. For example,
type 'a t = 'b constraint 'a = 'b * boolmay not be separable even if
'ais (its separately depends on 'b, a fragment of 'a), so its mode signature is
('a : Deepsep) t.
The different modes are ordered as*)
Ind < Sep < Deepsep(from the least demanding to the most demanding).
compute_decl env def returns the signature required for the type definition
def in the typing environment
env -- including signatures for the current recursive block.
Error exception is raised if no such signature exists -- the definition will always be invalid. This only happens when the definition is marked to be unboxed.
Variant (or record) declarations that are not marked with the "
@@unboxed" annotation, including those that contain several variants (or labels), are always separable. In particular, their mode signatures do not require anything of their type parameters, which are marked
Config.flat_float_array is not set, then separability is not required anymore; we just use
Ind as the mode of each parameter without any check.
type prop = Types.Separability.signature