From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q45EmtOm007128
	for <caml-list@sympa-roc.inria.fr>; Sat, 5 May 2012 16:48:56 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AhoCAJ09pU+LEwExe2dsb2JhbABFgx6vViIBARYmBSKCDAEBAQMBOAIGAQE3AQQLCxguVwaIHAUEpnyEMQGOYQaKf4U9Y6kv
X-IronPort-AV: E=Sophos;i="4.75,536,1330902000"; 
   d="scan'208";a="142683670"
Received: from hera.mpi-sb.mpg.de ([139.19.1.49])
  by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 05 May 2012 16:48:50 +0200
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=mpi-sb.mpg.de; s=mail200803; h=From:To:In-Reply-To:Subject:
	References:Message-Id:Content-Type:Content-Transfer-Encoding:
	Mime-Version:Date:Cc; bh=NzO+mbfJwaQ5jHQCtGy5Y/cUsQdjOeIZhH3pfm6
	zDN0=; b=w+7h1+K350zxkpHGJMzrePnAtOoBg6wnuPe15FROqF0UcZuKv5z6YYz
	igje13/f1Nb1zCELN+kkQsz/7RpbQsftWJG55SzE9UmzL9Adkonffz1wlkoF5NgY
	XPvy2mdgaBnTzS/YX4khnLx+vJoLDBqAYpKpRC/vXjQ8NzSHJiIk=
Received: from newzak.mpi-klsb.mpg.de ([139.19.1.29]:53812)
	by hera.mpi-sb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtp (Exim 4.69) id 1SQgHu-0004H6-O6; Sat, 05 May 2012 16:48:48 +0200
Received: from mnch-4d04573f.pool.mediaways.net ([77.4.87.63]:62021 helo=[192.168.178.31])
	by newzak.mpi-klsb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16)
	(Exim 4.72) id 1SQgHu-0006NY-CJ; Sat, 05 May 2012 16:48:46 +0200
From: Andreas Rossberg <rossberg@mpi-sws.org>
To: Goswin von Brederlow <goswin-v-b@web.de>
In-Reply-To: <87r4uykb09.fsf@frosties.localnet>
References: <87r4uykb09.fsf@frosties.localnet>
Message-Id: <8A61AE0A-950A-4AE0-912F-2B7A233C7E8A@mpi-sws.org>
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v936)
Date: Sat, 5 May 2012 16:48:46 +0200
Cc: caml-list@inria.fr
X-Mailer: Apple Mail (2.936)
Subject: Re: [Caml-list] A shallow option type

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