Comment author: @ppedrot

Note that this would also simplify the code of Typeopt, removing a lot of hardwired non-float primitive types that could just be declared as so through attributes in the ML source instead.

Comment author: @xavierleroy

An attribute looks like a good way to express this information (contrast with the discussion in #5361). Still, it has to be checked by the type-checker. A proof-of-concept implementation as a pull request would be welcome.

Comment author: @gasche

ppedrot: a patch to disable the float-array optimization was proposed

#163

Have you tried measuring the performance of Coq using this patch? This seems to be the easiest way to evaluate the potential performance benefits for Coq of what you propose.

Comment author: @alainfrisch

In addition to optimizing array accesses, this would also allow more ocaml.unboxed types.

But I don't think we need to exclude lazy. Claiming that a type cannot be float should be enough, no?

Comment author: @alainfrisch

I think this would be a nice opportunity to clean up the handling of value representation for types. In Types.type_declaration, one would replace the type_immediate field by a field with type:

  type type_representation =
  | Int
  | Float
  | Lazy
  | Non_float  (* values of the type are never represented as floats *)
  | Addr       (* neither float nor lazy *)
  | Generic

The "subtyping" is obvious. An abstract type without manifest is by default Generic but can be annotated through some attribute. The representation would be inferred with something like Typedecl.compute_immediacy.

The logic currently in Typeopt to infer the representation (following unboxed types), the one in Ctype.maybe_poiter and the one in Typedecl.get_unboxed_type_representation (/and Typedecl.is_float) should probably be merged.

Comment author: @ppedrot

See #1261.

With flat-float-array (#1294), the possibility that a type might be float no longer slows down array accesses, so this feature no longer seems necessary.