Skip to content
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

[@@unboxed] for single-constructor, single-field GADT introducing existential type #7597

Closed
vicuna opened this Issue Jul 24, 2017 · 2 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Jul 24, 2017

Original bug ID: 7597
Reporter: disteph
Assigned to: @alainfrisch
Status: resolved (set by @alainfrisch on 2017-07-28T15:45:00Z)
Resolution: duplicate
Priority: normal
Severity: feature
Version: 4.04.2
Category: typing
Related to: #7485

Bug description

[@@unboxed] looked like a great feature, but very often I can't use it because of abstract types. Here is my ml file for a minimal example:

type _ para = C
type t = H : _ para -> t [@@unboxed]

That's great, but when I want to hide the definition of _ para in the mli, i.e.

type _ para
type t = H : _ para -> t [@@unboxed]

...I get rejected.
And what's even more puzzling is that the error message talks about floats, which has nothing to do with what I had in mind:
I just want to remove the boxing because in general I'm just using a GADT for more precise typing, nothing computational.

Additional information

I've tried hard to understand the discussion #3007.

It seems that my mli is rejected because there is a danger that my abstract type might be an float? (or is it an unboxed float that would be dangerous?).

Again, I don't care much about floats here and I don't use them in my project, whether boxed or unboxed :-) So it seems desirable to me that the issue of floats doesn't pollute the otherwise great feature of not boxing a single-constructor, single-field GADT introducing an existential type.
Of course I'm sure there is a very good reason that this might be incompatible with other great features about floats, in which case I'd be happy to annotate my abstract type para with something like

type _ para [@@non_float]

as suggested in #3007 following the remark
"Another direction to avoid current limitations of the check would be to allow marking (abstract) types that they are known to hold no float values (whatever their type parameters are instantiated to)."

Is there currently a workaround that I have missed?

On the contrary, the #7511 / #3325 which fixes something in 4.05 seems to go towards more restriction while I want less :-)

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 24, 2017

Comment author: @yallop

In OCaml the functions that construct arrays check whether their arguments are represented as floats, and use a different (unboxed) array representation if they are. For that reason it's not safe to give float values and non-float values the same type. Here's an example of what happens if you do:

# [| Obj.repr 0.0; Obj.repr 0 |];;
Segmentation fault

Here the array constructor determines that the first argument is a float, so it tries to unbox the second argument as a float, too.

Your example is similar. With the following definitions,

type _ para
type t = H : _ para -> t [@@unboxed]

the type 'para' might be defined as follows:

type 'a para = 'a

Then, in the following code, both array elements would have the same type, but the first would have float representation, so the array constructor would try to unbox the second (non-float) argument as a float:

[| H 0.0; H 0 |]

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 24, 2017

Comment author: disteph

Ah, I see. Thanks for the explanation!
From 0007485, I understand there is some hope that an attribute might be introduced, which would provide what I need.
I'll be waiting for this eagerly :-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.