Re: [Caml-list] A shallow option type

[Andreas Rossberg <rossberg@mpi-sws.org>]

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