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".
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`?
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
--
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