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=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 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 EF008BC69 for ; Thu, 15 Nov 2007 07:32:51 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHJ2O0fUGyodimdsb2JhbACOfwEBAQgEBhERB4EP X-IronPort-AV: E=Sophos;i="4.21,419,1188770400"; d="scan'208";a="19322415" Received: from smtp3-g19.free.fr ([212.27.42.29]) by mail4-smtp-sop.national.inria.fr with ESMTP; 15 Nov 2007 07:32:51 +0100 Received: from smtp3-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp3-g19.free.fr (Postfix) with ESMTP id 2A06617B54D; Thu, 15 Nov 2007 07:32:51 +0100 (CET) Received: from [192.168.0.4] (rke75-3-82-229-183-156.fbx.proxad.net [82.229.183.156]) by smtp3-g19.free.fr (Postfix) with ESMTP id F0E3117B54C; Thu, 15 Nov 2007 07:32:50 +0100 (CET) Message-ID: <473BE750.9060301@frisch.fr> Date: Thu, 15 Nov 2007 07:29:36 +0100 From: Alain Frisch User-Agent: Thunderbird 2.0.0.6 (Windows/20070728) 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> <473AEC04.3030303@frisch.fr> <20071114143524.GA4423@yquem.inria.fr> <473B249D.9040703@frisch.fr> <20071114184352.GB28796@yquem.inria.fr> In-Reply-To: <20071114184352.GB28796@yquem.inria.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; frisch:01 frisch:01 compiler:01 weis:01 well-typed:01 ill-typed:01 subtypes:01 type-checker:01 wrote:01 abstract:01 clearer:01 integer:01 integer:01 defines:01 caml-list:01 Pierre Weis wrote: > - a value of type row is in fact a concrete integer (it is not hidden in any > way), But you cannot apply integer operations to it, so it is not a normal concrete integer, right? > - a value of type row can only be created by the make function defined in the > implementation of the module that defines the private type, > - a value of type row can be projected out of type row to a value of type int > with a ``no-op'' identity function (I called it from in the example). > > So, no: a value of type row is not of type int and you need a marker to > indicate the projection (for the time being the marker is a (identity) > function call to let the implemention as simple as possible, but a sub-typing > constraint makes sense and we can provide it if this is considered clearer). Now I'm lost :-) Can you show an example where replacing all "type t = private ..." definitions by "type t" changes a well-typed program into an ill-typed one? I understand that if private types create real subtypes (w.r.t. :>) then they are different than abstract types, but otherwise, I don't see the difference for the type-checker. -- Alain