From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.0 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 30877BC69 for ; Wed, 14 Nov 2007 17:57:10 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAFO3OkfRVYT0kmdsb2JhbACPAwIBAQcEBBMWgRE X-IronPort-AV: E=Sophos;i="4.21,417,1188770400"; d="scan'208";a="19294037" Received: from an-out-0708.google.com ([209.85.132.244]) by mail4-smtp-sop.national.inria.fr with ESMTP; 14 Nov 2007 17:57:09 +0100 Received: by an-out-0708.google.com with SMTP id c24so53721ana for ; Wed, 14 Nov 2007 08:57:08 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding; bh=6U9XqCS/ulBtX6ZXEd69qgk+D5/bykqk+pHUeiCIAUM=; b=k16fJ5DC7hgGJkzzPrbv700u4fG0UEyfOGrxZ7fuToIIKA9RvMM2Ol8Maa9FLBlzrCJ1KJKlLr9IHu7LZ8RXkLx0hVm7C8wrog6vTnjPAMsi6mr4x3Yp8lCMq7v/qLEFlhN0F9un1FsSAW0DEhJW7D7NIy1bP9pa7zfB5bzZLd8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding; b=ZchRR1TLEO8DKpaQpg/xxVRp3lrTiHskKsX1bQD0abwMYCUyEZ9htQfN7chyZaNVzCTYBDTcoa9hhp0YqJ5aQHabtT/id35Ql6BTPr/09q6aiJVjilBmoeg0Z0fJI8hG2Y9mx/vQ9gp97RxBN79f88hUJIMN8aTz45I39JDdcWE= Received: by 10.100.194.17 with SMTP id r17mr9771905anf.1195059428130; Wed, 14 Nov 2007 08:57:08 -0800 (PST) Received: from ?192.168.0.7? ( [69.152.94.247]) by mx.google.com with ESMTPS id d38sm972225and.2007.11.14.08.57.05 (version=SSLv3 cipher=RC4-MD5); Wed, 14 Nov 2007 08:57:06 -0800 (PST) Message-ID: <473B28DF.2050705@gmail.com> Date: Wed, 14 Nov 2007 10:57:03 -0600 From: Edgar Friendly User-Agent: Thunderbird 2.0.0.9 (X11/20071031) MIME-Version: 1.0 To: Pierre Weis Cc: caml-list Subject: Re: [Caml-list] Compiler feature - useful or not? References: <473A363F.2080301@gmail.com> <891bd3390711131608g48b584a4n6b0ccab95d7de3f3@mail.gmail.com> <20071114075827.GA24058@yquem.inria.fr> In-Reply-To: <20071114075827.GA24058@yquem.inria.fr> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; compiler:01 weis:01 compiler:01 abbreviation:01 abbreviation:01 literals:01 invariants:01 low-level:01 casts:01 invariants:01 coercions:01 edgar:98 'from':98 wrote:01 abstract:01 Pierre Weis wrote: > In the next version of the compiler, you will have an extension to the > definition of types with private construction functions (aka ``private'' > types) that just fulfills your programming concern: in addition to usual > private sum and record private type definitions, you can now define a type > abbreviation which is private to the implementation part of a module (see > note 1). > At first glance, this improvement does satisfy my concerns, but I think it still falls short of optimal in ways that seem easy to fix. > Since the values of a private type are concrete, it is much easier for the > programmer to use the values of the type abbreviation. > This concerns me - I'd like to require explicit casting/coercion to create or use the internal value of the abstract type, maybe with an exception for literals. Could you elaborate on this? > This solution does not require any additional tagging or boxing, only the > usage of injection/projection function for the type. As for usual private > types, the injection function is handy to provide useful invariants (in the > row type example case, we get ``a row value is always a positive integer''). > With a bit of low-level support, I imagine it not difficult to implement the following: type row = private int constraint (fun i -> i >= 0) such that the compiler uses the provided constraint function to check any (x :> row) casts, throwing an exception(?) on false. This solution wouldn't involve the module system just to have positive integer types, and gets rid of the function call overhead on 'from'. > In addition, the private abbreviation is publicly exposed in the interface > file. Hence, the compiler knows about it: it can (and effectively does) > optimize the programs that use values of type row in the same way as if the > type row were defined as a regular public abbreviation. > Does this mean I can do: let one (r:row) = r+1 let onea (r : row) = r = 1 let two (r:row) (i:int) = r+i let three : row -> string = function 3 -> "three" | _ -> "not three" > Last but not least, being an instance of the identity function, the from > projection function is somewhat generic: we can dream to suppress the burden > of having to write it for each private type definition, if we find a way to > have it automatically associated to the new private type by the compiler. > The use case for this feature is restricted construction to enforce invariants, no? Anything more complex should probably be totally abstract and not simply private. In which case, the constraint keyword seems an effective way to tell the compiler what to do, and just let :> coercions do their magic. E.