Goswin von Brederlow <goswin-...@web.de> writes:
> Andreas Rossberg <rossb...@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
--
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
