New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Recursive yet unboxed #2188

Open
wants to merge 13 commits into
base: trunk
from

Conversation

Projects
None yet
4 participants
@rlepigre
Copy link
Contributor

rlepigre commented Dec 8, 2018

We (@gasche and I) give a new implementation of the unboxability check for single-constructor types, following theoretical investigations presented in our JFLA 2019 paper (which refines the work of @SimonColin as part of an internship with @gasche). Mutually-recursive type definitions can now contain unboxed declarations, which was not the case before.

@rlepigre rlepigre force-pushed the rlepigre:recursive-yet-unboxed branch from e32351f to 524a1aa Dec 8, 2018

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Dec 8, 2018

The history is not as clean as I would like, but we believe that the code is ready for review. I hope to rebase the PR later and clean the history in passing.

Below are two remarks that I wrote on the implementation.

.

We distinguish the notion of "unboxability" (of type definitions) and
"separability", with respect to the Config.flat_float_array setting:
separability is a semantic notion that is always well-defined
(and does not depend on Config.flat_float_array), but "unboxability"
only depends on separability when Config.flat_float_array is set.

Ideally, the typedecl_separability module would never depend on
Config.flat_float_array, and this flag would be tested outside, by the
caller. In practice, it is more regular (with respect to other
typedecl_* modules) to have the check in the module, but it is only at
the edge, in the compute_decl function that is exposed outside
(and also in the Types.Separability.default_signature function).

.

There is a strange duplication between Types.Separability.default_signature
and Types_separability.msig_of_external_type. They seem to do the same thing,
but they don't have access to (or use) the same information:

  • default_signature is used to construct type declarations from
    nothing; at this point, there is no immediacy information. On the
    other hand, it checks Config.flat_float_array and uses Ind instead
    of Deepsep when it is not set.

  • msig_of_external_type takes the declaration of the type as
    argument. In particular, it checks immediacy (immediate types
    are always separable).

I thought about this, and I don't see any way to do better than having
these two functions. Note that msig_of_external_type is not exposed
directly by the Typedecl_separability signature, but it is accessible
as the default field of Typedecl_separability.property.

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Dec 8, 2018

(cc @damiendoligez, @yallop and @Armael; you might be interested in this PR)

@Armael

This comment has been minimized.

Copy link
Member

Armael commented Dec 8, 2018

Don't count on me for this one, I won't have much time until a couple months.

Show resolved Hide resolved typing/typedecl_separability.ml Outdated
Show resolved Hide resolved testsuite/tests/typing-unboxed-types/test_flat.ml
Show resolved Hide resolved Changes Outdated
Show resolved Hide resolved typing/types.mli Outdated
Show resolved Hide resolved typing/types.mli Outdated
Show resolved Hide resolved typing/types.ml
separability cannot be established. *)

type mode = Types.Separability.t = Ind | Sep | Deepsep
(** The mode [Sep] ("separable") is used on type expressions that must be

This comment has been minimized.

@yallop

yallop Dec 11, 2018

Member

The comment phrases the mode as a requirement on arguments ("type expressions that must be separable"), and that's generally how it's used. But I'd prefer to see it defined more neutrally somewhere as a description of type expressions. One option is to document Types.Separability.t as a (representation of a) property of type expressions, and separately document Typedecl_separability.mode as a requirement on arguments, as it is currently.

This comment has been minimized.

@gasche

gasche Dec 20, 2018

Member

I rewrote this comment to include for each mode, then the type-expression view, and then the type-parameter view. I think the latter is necessary to give intuition (type expressions themselves, at the toplevel, must all be separable).

Show resolved Hide resolved typing/typedecl_separability.ml Outdated
@gasche

This comment has been minimized.

Copy link
Member

gasche commented Dec 11, 2018

@yallop: thanks! I fixed the easy issues, changes for the other are yet to come.

@gasche gasche force-pushed the rlepigre:recursive-yet-unboxed branch 2 times, most recently from 0211e96 to f9c6b26 Dec 11, 2018

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Dec 14, 2018

I rebased the PR history, it reads like a novel now. (cc @rlepigre)

@rlepigre

This comment has been minimized.

Copy link
Contributor

rlepigre commented Dec 14, 2018

@gasche: A bestseller for sure!

@gasche gasche force-pushed the rlepigre:recursive-yet-unboxed branch 2 times, most recently from 15c348c to a018864 Dec 20, 2018

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Dec 20, 2018

I rebased against the current trunk and finished taking into accounts the comments of @yallop's first review pass. Thanks!

@gasche gasche force-pushed the rlepigre:recursive-yet-unboxed branch from a018864 to 5e74e19 Dec 30, 2018

rlepigre and others added some commits Oct 4, 2018

typedecl_separability: destructure type definition to access unboxing…
… information

In the future, we could move the arity-related checks
(one constructor, one parameter) and error logic from typedecl.ml to
typedecl_separability.ml.
add separability signatures in type declarations
(this changes the .cmi format and thus requires a bootstrap,
to follow as a separate commit)

(includes bug fixes by Rodolphe Lepigre)
typedecl: use the new Separability implementation, remove old code
Because this changes the separability of standard library types, and
those separabilities are stored in the .cmi files, this commit changes
the .cmi files in the standard libraries in way that appear to require
a bootstrap (it looks like some part of the stdlib is built with
boot/ocamlc and others with ocamlc, and the two should produce/expect
the same .cmi exactly). The bootstrap will come as a separate commit.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment