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

Reply via email to