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 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 04E51BC69 for ; Fri, 16 Nov 2007 18:43:46 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHNlPUdA6aq9kmdsb2JhbACPDQEBAQEHBAQp X-IronPort-AV: E=Sophos;i="4.21,427,1188770400"; d="scan'208";a="5903211" Received: from rn-out-0910.google.com (HELO rn-out-0102.google.com) ([64.233.170.189]) by mail3-smtp-sop.national.inria.fr with ESMTP; 16 Nov 2007 18:43:47 +0100 Received: by rn-out-0102.google.com with SMTP id s46so161156rnb for ; Fri, 16 Nov 2007 09:43:45 -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=jUgOsuH6q361Cm9XPaWehcaXhAmRGfAUzQOs52yQUro=; b=LdcCr0uXvaPxXoQdUyDnOTBIoOklZuZUhiJOttQZJc5iFRO3tTeS1Cc/sasgirARobrQvxM3mrTLUNIvd6gZdWAFP6ZDDNXMNM6sbWM4VEzRekeumfwIT+m6xw52CZEHti7bTHgnC8jl5vcxgQA0aKoH/juvUSiLE70OGfGumfQ= 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=Xwy6obMsASoROO3EoyIMpTB/58Lt7441O/RB/6phBXo6B+VkqoIRhEHPwq7A74VV5gN/e6RMTCDhaCDFWXFecvUdawtJxU35XPFXToeYbZUebeh/LB36IQg29AUQVXDH4kA84cINsbL+LpUX5VFxwb7SqRceFuTzNS9cf7s4ZZo= Received: by 10.70.92.18 with SMTP id p18mr3503861wxb.1195235024648; Fri, 16 Nov 2007 09:43:44 -0800 (PST) Received: from ?192.168.0.7? ( [69.152.94.247]) by mx.google.com with ESMTPS id i6sm4741032wxd.2007.11.16.09.43.42 (version=SSLv3 cipher=RC4-MD5); Fri, 16 Nov 2007 09:43:43 -0800 (PST) Message-ID: <473DD6CC.20108@gmail.com> Date: Fri, 16 Nov 2007 11:43:40 -0600 From: Edgar Friendly User-Agent: Thunderbird 2.0.0.9 (X11/20071031) MIME-Version: 1.0 To: Fernando Alegre Cc: Martin Jambon , caml-list , Alain Frisch Subject: Re: [Caml-list] Compiler feature - useful or not? References: <20071114143524.GA4423@yquem.inria.fr> <473B249D.9040703@frisch.fr> <20071114184352.GB28796@yquem.inria.fr> <473BE750.9060301@frisch.fr> <20071115132649.GB15754@yquem.inria.fr> <891bd3390711151630x238b8eddod5b7462d0fa1c735@mail.gmail.com> <473D61A3.9090708@frisch.fr> <20071116173105.GA12079@gato.physics.und.nodak.edu> In-Reply-To: <20071116173105.GA12079@gato.physics.und.nodak.edu> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; compiler:01 parametrized:01 compiler:01 camlp:01 compile-time:01 runtime:01 runtime:01 ocaml:01 edgar:98 wrote:01 integer:01 caml-list:01 coercion:01 coercion:01 constraint:01 Fernando Alegre wrote: > Even better would be to have a "parametrized finite" type. This would > really need to be built into the compiler, as I don't think it can > actually be emulated by either camlp4 or the C interface. > > The idea is very simple: add a primitive "n finite" type to the > language, where n is a positive integer constant. > > For example: > > type bit = 2 finite > > type mod3 = 3 finite > > Then, fill the type by coercion so that "(x :> n finite)", where both x > and n are known to be constant at compile-time and 0 <= x < n, becomes a > value of type "n finite". > > This should be pretty straightforward to implement, and it may simplify > code that depends on types such as "T1 | T2 | T3 | T4" > > I don't know how much it would be possible to relax the constraint above > while maintaining the typesystem sound. Does anybody whether this is > a known problem? > > Thanks, > Fernando > To implement these types (as well as what I've just proposed), the interface between the type system and the runtime will have to change. As Jacques pointed out, a coercion, being a type-level action, cannot generate any code, and in order to do runtime coercion to a restricted type, you need value checks to ensure a valid value. I hope that it won't hurt my brain too much to see what can be done to create such a bridge between the type system and the code generator, even if INRIA never accepts the idea into the official OCaml distribution. If you'd like to look at how another language implemented these ideas, look here: http://www.adapower.com/rm95/RM-3-5-4.html E.