From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 894BCBC57 for ; Tue, 3 Aug 2010 17:47:13 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlgCANLWV0zZSMDjkWdsb2JhbACgERUBAQEBCQsKBxEDH8N5hTkE X-IronPort-AV: E=Sophos;i="4.55,309,1278280800"; d="scan'208";a="64996289" Received: from fmmailgate02.web.de ([217.72.192.227]) by mail1-smtp-roc.national.inria.fr with ESMTP; 03 Aug 2010 17:47:13 +0200 Received: from smtp02.web.de ( [172.20.0.184]) by fmmailgate02.web.de (Postfix) with ESMTP id C230916D455D9; Tue, 3 Aug 2010 17:47:12 +0200 (CEST) Received: from [78.43.204.177] (helo=frosties.localdomain) by smtp02.web.de with asmtp (TLSv1:AES256-SHA:256) (WEB.DE 4.110 #24) id 1OgJhw-0001ii-00; Tue, 03 Aug 2010 17:47:12 +0200 Received: from mrvn by frosties.localdomain with local (Exim 4.72) (envelope-from ) id 1OgJhw-00005S-8w; Tue, 03 Aug 2010 17:47:12 +0200 From: Goswin von Brederlow To: bluestorm Cc: Lukasz Stafiniak , caml-list@inria.fr Subject: Re: [Caml-list] Conditionals based on phantom types References: Date: Tue, 03 Aug 2010 17:47:12 +0200 In-Reply-To: (bluestorm's message of "Mon, 2 Aug 2010 10:02:41 +0200") Message-ID: <87r5if4s1r.fsf@frosties.localdomain> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: goswin-v-b@web.de X-Sender: goswin-v-b@web.de X-Provags-ID: V01U2FsdGVkX1+Ej4mTdjQmJQHrg85BxQP69djDJbp7j7/Td5w6 IRuqGeQ/iOAyZfZ93glmMwRv9NLPKSMQZLyAb8RIzEWV3yeFAE IqVj16Uv8= X-Spam: no; 0.00; conditionals:01 lukasz:01 val:01 typecheck:01 assertion:01 bug:01 submodule:01 submodule:01 assertion:01 compiler:01 mfg:98 typing:01 typing:01 assert:01 caml-list:01 bluestorm writes: > Two remarks on Lukasz suggestion : > >>   val add : 'a t -> 'a t -> 'a t >> [..] >>   let add (_,x) (_,y) = x +. y > > This does not typecheck. I suggest the following : > > let add (ux, x) (uy, y) = > assert (ux = uy); > (ux, x +. y) > > While the assertion does not seem necessary at first (correct units > are guaranteed by typing !), it may be helpful in case of bug inside > the Units module or signature, wich breaks the typing invariant. If > you're planning to do relatively elaborate things inside the Units, I > strongly recommend to use any kind of dynamic checking available, at > least during development. This is something is understood late in my > own phantom-type project (Macaque), and would have been very useful > for debugging. I tend to hide the phantom tpyes in a submodule with just the bare minimum of function (creation and access) included and then use the submodule in the actual module. That way the phantom types are verified in the actual module too. Instead of assertion failures at runtie you get compiler errors. MfG Goswin