Attribute to mark immediate types#188
Conversation
There was a problem hiding this comment.
You have no tests where the module signature is separate from the module implementation, for example:
module type S = sig
type t [@@immediate]
end
module M_valid : S = struct type t = int end
module M_invalid : S = struct type t = string end
module F (M : S) : S = M
module FM_valid = F (struct type t = int end)
module FM_invalid = F (struct type t = string end)
There was a problem hiding this comment.
I've updated the file with the suggested tests. Thanks!
|
The first example is broken. Is it supposed to have |
|
I would just like to notice that this looks a lot like a small fragment of an effect system for types. |
|
@andrejbauer apologies, that was a typo. You also couldn't have |
|
If it was a typo, what is the correct example then? I don't get it, I think. Are you just propagating the information that a particular abstract type is "immediate" by hand? |
|
My understanding is that "is immediate" is an intensional property of type that was, so far, not expressible in type declarations/interfaces. This I think the only property of types (besides their definition, as the upper bound of the information lattice) that is expressible in signatures today is variance. We lack the way to express injectivity, contractivity, the fact of being an upper- or lower-bound of the subtyping lattice, immediateness, floatiness (those two are only motivated by performance rather than expressivity). Dependent type theories typically also try to propagate (strict) productivity or size information. I'm not sure we should consider this "propagating information by hand": it needs to be marked explicitly in the signature of abstract types (because only the programmer can decide on the intent of exposing or not those informations, making a compromise between freedom to change implementation vs. information provided by the interface), but then it is propagated by the type-checker in the normal way -- until the next abstraction boundary. |
|
@andrejbauer I updated the example in the PR comment above. And @gasche explains the reasoning quite well! |
I don't have a specific example to hand, but supporting multiple implementations which change from: type t = Foo | Barto: type t = Foo | Bar | Bazseems pretty useful. |
|
Is it theoretically possible to annotate other types with such attributes? Polymorphic arrays of immediate values (or non-float values) would be nice to have, for instance. |
This would require a kind system, which is something OCaml deliberately avoids. |
|
We discussed it at the developer meeting today. I supported the design and general approach, and there seemed to be consensus that we could merge it in trunk if there was solid evidence that this improves program performance. @xavierleroy thus asked for a convincing example of use of this feature in a representative OCaml program, with information on the performance effect of the change. @willcrichton or anyone else, would you be able to provide such a representative example (not a micro bench-mark)? The feature freeze for the next release should be in about a month, so you would need to hurry if you want it in the next release. |
|
@xavierleroy Xavier, do you need to see the actual source, or are performance numbers enough? We can probably generate performance results pretty easily, but much of it is for source that we can't easily release. |
|
Just some performance results, that would be perfect. Thanks! |
|
@yminsky do you have numbers now? |
|
Apologies. We let this slip, but @lpw25 will throw together a benchmark very shortly. |
|
We have an in memory database thing that uses integers for keys and some other stuff. This is used in production (i.e. not a toy example). Benchmarks for its main operations, without and with which gives an average improvement of just under 15%. |
|
@xavierleroy Are you satisfied with these numbers? |
|
Travis is failing, probably because you need to update the I talked with @xavierleroy and we're both OK to merge this. |
|
@diml is going to do the rebase and then push it directly. |
|
I squashed the commits and rebased them on the current trunk. We'll reread the result tomorrow |
|
Merged manually (50dd38d) |
ghost
closed this
* reintegrate toplevel and remove hilite fmt dependency * add basic regexp-based syntax highlighting in toplevel * resize on tab completion * hide try button * scroll output on completion * highlight double-quoted strings * fix multiple matches when highlighting * add changes entry
12 participants
This pull request adds support for a new attribute
[@@immediate]which marks a type as a immediate, or a non-pointer.Types marked as immediates won't activate the GC's write barrier upon mutation (as they are not pointers and cannot induce a new pointer from the major to minor heap), which can significantly boost performance in programs relying heavily on mutable state. This feature already exists in the compiler, but it currently does not extend to abstract types. For example:
In the above module, modifications to
Foo.xwill invoke the write barrier because the compiler doesn't know thattis necessarily immediate, even though it is implemented as such. However, if you update the module to reflect that:Then subsequent mutations to
Foo.xwill not call the write barrier. For example, running such mutations in a tight loop:On my machine, the version without the attribute takes 0.51s and the version with the attribute takes 0.14s.
The feature was designed similarly to how variance is implemented in the typechecker, albeit substantially simpler. One can add a check on a type alias or definition:
Which will produce the error message:
And one can assert the immediacy of an abstract type, which will be checked during ascription:
Will cause the error: