Re: [Caml-list] A shallow option type

[Goswin von Brederlow <goswin-v-b@web.de>]

Goswin von Brederlow <goswin-v-b@web.de> writes:

> Andreas Rossberg <rossberg@mpi-sws.org> writes:
>
>> On May 5, 2012, at 15.33 h, Goswin von Brederlow wrote:
>>> What I want is a
>>>
>>>    type 'a shallow = NULL | 'a  (constraint 'a != 'b shallow)
>>
>> This is a form of negation, which cannot be expressed in conventional
>> type systems. Just consider what it should mean in the presence of
>> type abstraction: if you have
>>
>>   M : sig
>>     type t
>>     ...
>>   end
>>
>> would `M.t shallow` be a legal type? You couldn't decide that properly
>> without requiring that _every_ abstract type in every signature is
>> annotated with a constraint saying that it is "not shallow".
>
> True, so abstract types would have to be forbidden too becauseit can't
> be decided wether they are save or not. Since 'a shallow is an abstract
> type that would also forbid 'a shallow shallow.
>
> So "constraint 'a != <abstract>" would be the right thing.
>
>>> 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.
>>
>> And how do you know that nobody else implements a _different_ type,
>> say shallow2, that does the same thing? And a third party then
>> constructs a value of type `int shallow2 shallow`?
>
> I don't and I can't. But such a type would be abstract so wouldn't be
> allowed by the above (reject abstract types).

Actualy this could be solved. The problem of a int shallow2 shallow is
that both would be using NULL for None. But nobody says I must use
NULL. All it needs is a bit pattern that can't be a valid value. Any
pointer will do:

#include <caml/mlvalues.h>

static value nil = Val_unit;

CAMLprim value caml_shallow_null(value unit) {
    (void)unit; // unused
    return &nil;
}

Now if shallow2 uses my &nil as well that would be a serious bug in
shallow2 and pretty hard to do.

>> It seems to me that what you want effectively is a special case of non-
>> disjoint union. Unfortunately, those are known to come with all kinds
>> of problems, such as not being compositional.
>>
>> /Andreas
>
> What I want is to have an array of
>
>     type t ={ ... }  (* Unit.t *)
>
> and a matrix of
>
>     type tile = { ... mutable unit : Unit.t option; }
>
> that I can safely access from a C thread in parallel with ocaml without
> having to look the runtime system or individual tiles (the array and
> matrix would both be created outside the ocaml heap).
>
> The problem I have is that
>
>     tile.unit <- Some unit
>
> will allocate an option block on the heap and accessing that from C
> while the GC runs causes a race condition.
>
>
> What I don't want to do is use
>
>     type tile = { ... mutable unit : Unit.t; }
>     tile.unit <- Obj.magic 0
>
> since then trying things out in the toplevel causes segfaults when the
> pretty printer prints the tile.unit and it would be easy to forget to
> compare the tile.unit to Obj.magic 0 on every use. I know my shallow
> type is basically nothing else but it adds a level of savety to it.
>
> Idealy I would even love to write
>
>     match tile.unit with
>       | NULL -> ()
>       | unit -> do_something unit
>
> I guess some camlp4 magic could be used to transform such a match into
>
>     match Shallow.as_option tile.unit with
>       | None -> ()
>       | Some unit -> do_something unit
>
> or similar constructs.
>
> MfG
>         Goswin

MfG
        Goswin