Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007597OCamltypingpublic2017-07-24 08:182017-07-28 17:45
Assigned Tofrisch 
PlatformOSOS Version
Product Version4.04.2 
Target VersionFixed in Version 
Summary0007597: [@@unboxed] for single-constructor, single-field GADT introducing existential type
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 InformationI've tried hard to understand the discussion PR#606.

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 PR#606 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 MPR#7511 / PR#1133 which fixes something in 4.05 seems to go towards more restriction while I want less :-)
TagsNo tags attached.
Attached Files

- Relationships
related to 0007485acknowledged Adding an attribute for abstract types that are not float / lazy 

-  Notes
yallop (developer)
2017-07-24 08:32

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 |]
disteph (reporter)
2017-07-24 10:44

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 :-)

- Issue History
Date Modified Username Field Change
2017-07-24 08:18 disteph New Issue
2017-07-24 08:22 yallop Relationship added related to 0007485
2017-07-24 08:32 yallop Note Added: 0018130
2017-07-24 10:44 disteph Note Added: 0018131
2017-07-28 17:45 frisch Status new => resolved
2017-07-28 17:45 frisch Resolution open => duplicate
2017-07-28 17:45 frisch Assigned To => frisch

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker