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=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id E89A5BB84 for ; Mon, 22 Sep 2008 01:17:02 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At4AAMpy1khCbwQZlGdsb2JhbACTHgEBAQEJCQwHEQSgRIFm X-IronPort-AV: E=Sophos;i="4.32,443,1217800800"; d="scan'208";a="17575470" Received: from out1.smtp.messagingengine.com ([66.111.4.25]) by mail1-smtp-roc.national.inria.fr with ESMTP; 22 Sep 2008 01:17:02 +0200 Received: from compute1.internal (compute1.internal [10.202.2.41]) by out1.messagingengine.com (Postfix) with ESMTP id A975815A9A0; Sun, 21 Sep 2008 19:17:01 -0400 (EDT) Received: from heartbeat1.messagingengine.com ([10.202.2.160]) by compute1.internal (MEProxy); Sun, 21 Sep 2008 19:17:01 -0400 X-Sasl-enc: Iwccg1NR13n5MKr66N6z+P6+AKSCWv8YI5VRGOMjEarP 1222039021 Received: from [192.168.1.10] (ALyon-157-1-17-129.w81-251.abo.wanadoo.fr [81.251.176.129]) by mail.messagingengine.com (Postfix) with ESMTPSA id B14A614DE5; Sun, 21 Sep 2008 19:17:00 -0400 (EDT) Date: Mon, 22 Sep 2008 01:10:26 +0200 (CEST) From: Martin Jambon X-X-Sender: martin@martin.ec.wink.com To: Andrej Bauer Cc: Angela Zhu , caml-list Subject: Re: [Caml-list] Ocaml type with constraints? In-Reply-To: <48D6C51E.5060901@andrej.com> Message-ID: References: <48D6C51E.5060901@andrej.com> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Spam: no; 0.00; ens-lyon:01 ocaml:01 andrej:01 ocaml:01 checker:01 undecidable:01 angela:98 .0.:98 wrote:01 wrote:01 compile:01 compiles:01 caml-list:01 int:01 jambon:01 On Mon, 22 Sep 2008, Andrej Bauer wrote: > Angela Zhu wrote: >> Hi, >> >> I want to define an OCaml type with constraints. >> For example: >> >> type item = Item of int * float;; >> >> If here this float type is for price of some item, and I want to make sure >> it is positive. In other words, if x = (xi, xf) of type item, >> I want to enforce, xf must >= 0. >> >> Is there a way to define OCaml type like this? > > No, because Ocaml type checker always check all the types at compile > time. It is an undecidable problem whether a given expression of type > float evaluates to a non-negative number. By the way, even float does not guarantee to have a number: 0./.0. compiles and runs happily. Martin -- http://mjambon.com/