Re: [Caml-list] A shallow option type

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> Is it possible to somehow declare the constraint that 'a in 'a shallow
> must not be itself a 'b shallow?

If I understand correctly, this is not possible directly, and while
you could do that with a sufficiently clever layer of phantom types,
I'm not sure it is worth the additional complexity. In particular, you
would not be able to statically move from ('a shallow) to ('a) by the
imperative action of updating a reference (one would need a type
system with strong update, where state change may incur type change,
to do that).

I think that, given your constraints, the simplest solution is
probably to just use 'a, while informally specifying that it is not
always safe to use, and providing from the C side a null value of type
'a, so that you can dynamically test on the OCaml side that your
variable indeed is initialized.
(I suppose you need to expose yet-unitialized values to the OCaml
side, otherwise you wouldn't need to reason about nullability at all.)

On Sat, May 5, 2012 at 3:33 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> Hi,
>
> I wish there was an option type that would work without extra
> indirection (or more importantly without extra allocation of an ocaml
> value when setting it to something).
>
> Why? I'm interfacing with C in a multithreaded way. The data is
> allocated on the C side so it won't be moved around by the GC. The ocaml
> side will modify data and the C side will utilize it. Now if ocaml
> changes a multable 'a option then it will allocate a block for "Some x"
> and the GC will move that block around during compaction. Which means
> the 'a option can't be safely used without holding the runtime system
> lock. Which then means the threads can't run in parallel.
>
> What I want is a
>
>    type 'a shallow = NULL | 'a  (constraint 'a != 'b shallow)
>
> I have some ideas on how to implement this in a module as abstract type
> providing get/set/clear functions, which basically means I map None to a
> C NULL pointer and Some x to plain x. I know x can never be the NULL
> pointer, except when someone creates a 'a shallow shallow and sets Some
> None. That would turn into simply None.
>
> Is it possible to somehow declare the constraint that 'a in 'a shallow must
> not be itself a 'b shallow?
>
> MfG
>        Goswin
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>