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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 0FC48BBAF for ; Fri, 7 May 2010 11:42:34 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnUCAM9840uBrw8EnGdsb2JhbACDF5p3FQEBAQEBCAsICREiqnGQWIEmgwFuBINh X-IronPort-AV: E=Sophos;i="4.52,347,1270418400"; d="scan'208";a="50193842" Received: from ext.lri.fr ([129.175.15.4]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 07 May 2010 11:42:33 +0200 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id 716F7A470D; Fri, 7 May 2010 11:42:33 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Frsd95wSvtdP; Fri, 7 May 2010 11:42:33 +0200 (CEST) Received: from lri4-139 (lri4-139 [129.175.4.139]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id 504ADA46F2; Fri, 7 May 2010 11:42:33 +0200 (CEST) Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes To: "Anthony Tavener" Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Subtyping structurally-equivalent records, or something like it? References: Date: Fri, 07 May 2010 11:42:32 +0200 MIME-Version: 1.0 Content-Transfer-Encoding: Quoted-Printable From: AUGER Organization: ProVal Message-ID: In-Reply-To: User-Agent: Opera Mail/10.10 (Linux) X-Spam: no; 0.00; subtyping:01 lri:01 0200,:01 verbose:01 val:01 val:01 paris-sud:01 lri:01 umr:01 orsay:01 phane:98 clearer:01 caml-list:01 int:01 int:01 Le Sun, 02 May 2010 04:59:48 +0200, Anthony Tavener = a =C3=A9crit: > Wow! Thanks St=C3=A9phane... that was a little piece of magic I was > hoping for. It's a bit verbose, but at least it doesn't affect > performance and it allows all the control over types I need. > > I now see I didn't really grok phantom types whenever they were > mentioned. A bit of "in one ear and out the other". Now I have > better grasp on yet another feature of the language. > > > I know I read that one before, Dario... that title about NASA > is familiar! Too bad I didn't remember it was a solution to the > problem I was now having. Thank-you for that link -- an > excellent description of the problem and a nice solution. > > > Ah, great stuff... that looks like something to consider too, > Sylvain! There's plenty of material on phantom types but I never > made the connection that they were what I was looking for. > > > Thank-you everyone for the help and clear explanations! I'm > going to go play with this now. :) > > Anthony Tavener Just one last thing about this thread: It is not really related to type checking, but more on a way to convince the programmer that it uses rightfully a = force and not a position; it is the use of labels. Imagine you have this function: (** [next_position p v dt] is the next position of an object on position= = [p] with a speed [v] in a time [dt] *) val next_position: kinematic -> kinematic -> float -> kinematic as far as you have the documentation next to you, you won't make mistake= = between the two `kinematic'; but if you don't have it, then you may not recall if you have to write = `next_position v p dt' or `next_position p v dt' but now, imagine you have: (** [next_position p v dt] is the next position of an object on position= = [p] with a speed [v] in a time [dt] *) val next_position: pos:kinematic -> speed:kinematic -> laps:float -> = kinematic then you just have to use the right labels to make it work: `next_position ~speed:v ~pos:p ~laps:dt'. As I said, this is not a type checking solution, but it can make the = program clearer and allows the user to forget parameters order (but he = needs to memorize label names) Just beware with higher order: # let g ~x ~y =3D x - y;; val g : x:int -> y:int -> int =3D # let app (f: y:int -> x:int -> int) a b =3D f ~x:a ~y:b;; val app : (y:int -> x:int -> int) -> int -> int -> int =3D # app g;; Error: This expression has type x:int -> y:int -> int but an expression was expected of type y:int -> x:int -> int -- = C=C3=A9dric AUGER Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay