From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 1D9F87F8FC for ; Tue, 10 Jun 2014 16:13:08 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-50.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-50.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AogDAEkRl1ODbwiWnGdsb2JhbABZhySnfgaZEgGBCRYPAQEBAQEICwkJFCiEAwEBBAEjBFIFCwsaAgUhAgIPAQRJiE0IrGuaAYRwF4EqhCyIQDMHgnWBTASxJg X-IPAS-Result: AogDAEkRl1ODbwiWnGdsb2JhbABZhySnfgaZEgGBCRYPAQEBAQEICwkJFCiEAwEBBAEjBFIFCwsaAgUhAgIPAQRJiE0IrGuaAYRwF4EqhCyIQDMHgnWBTASxJg X-IronPort-AV: E=Sophos;i="4.98,1009,1392159600"; d="scan'208";a="79353211" Received: from ppsw-50.csi.cam.ac.uk ([131.111.8.150]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 10 Jun 2014 16:13:07 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from kingston.cl.cam.ac.uk ([128.232.64.15]:36037) by ppsw-50.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1WuMnS-0000bM-sH (Exim 4.82_3-c0e5623) (return-path ); Tue, 10 Jun 2014 15:13:06 +0100 From: Leo White To: Jordan W Cc: caml-list@inria.fr References: X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Tue, 10 Jun 2014 15:13:06 +0100 In-Reply-To: (Jordan W.'s message of "Mon, 9 Jun 2014 11:50:22 -0700") Message-ID: User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Row-polymorphic type declarations > 1. Does anyone know how can we later instantiate the polymorphic row vari= ables ".." with particular rows (both for obj > methods and variants). Any good docs on this? How do we assert that anoth= er type/expression is equivalent to 'a t with > 'a being a particular set of rows. > > Could someone give an example with a 2D point type > > type 'a twoDimensionalPoint constraint 'a =3D ;; > > How would we create another type threeDimensionalPoint that we assert is = a two dimensional point with the polymorphic > row variables being set to `z:int`? I understand type inference/checking = automates most of this, but I often like to > explicitly write type definitions to verify my own understanding of the p= rogram/inference. You can never get your hands on the row variable itself, you can only ever refer to polymorphic types containing row variables. For example, in your definition of `twoDimensionalPoint` you capture the row variable `..` by instead refering the the polymorphic type ``. Similarly, you cannot instantiate the row variable directly, but instead you must instantiate a polymorphic type containing the row variable. For your example, I can think of a few ways to specify this. 1. Using a constraint on a `twoDimensionalPoint`: type 'a threeDimensionalPoint =3D 'a twoDimensionalPoint constraint 'a =3D 2. Using two constraints on the type parameter: type 'a threeDimensionalPoint =3D 'a constraint 'a =3D 'a twoDimensionalPoint constraint 'a =3D ;; 3. Since your example uses object types, class types provide an alternative mechanism: class type twoDimensionalPoint =3D object method x: int method y: int end class type threeDimensionalPoint =3D object inherit twoDimensionalPoint method z: int end which allows you to use the `#t` syntax to refer to the polymorphic object types: let foo (p : #twoDimensionalPoint) =3D p#x + p#y let bar (p : #threeDimensionalPoint) =3D p#z + foo p A similar thing can also be achieved for polymorphic variants: type t =3D [`X of int] type s =3D [t | `Y of int] let foo (v : [> t]) =3D match v with | `X i -> i | _ -> 0 let bar (v : [> s]) =3D match v with | `Y i -> i | x -> foo x > 3. Also curious why annotations in arguments don't require acknowledgment= of row polymorphism > > =C2=A0 let f (o:) =3D o#x + o#y;; The row polymorphism is acknowledged by the `..` which represents the row variable. > 4. It appears there are two ways to write the row-polymorphic type annota= tion: > type 'a t =3D ([> `Red ] as 'a) and type 'a t constraint 'a =3D [> `Red ]= . Why are there two ways and what are the > advantages? They are completely equivalent. Regards, Leo