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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 9B3187ED25 for ; Fri, 19 Jul 2013 17:32:34 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.132; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.132; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-32.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.132; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-32.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArkBANZa6VGDbwiElGdsb2JhbABbxFSBEBYOAQEBAQcNCQkUBSOCJAEBAQMBJxM/BQsLDhMlDwEESYgdBq8diAeQDweDfgOsPQ X-IPAS-Result: ArkBANZa6VGDbwiElGdsb2JhbABbxFSBEBYOAQEBAQcNCQkUBSOCJAEBAQMBJxM/BQsLDhMlDwEESYgdBq8diAeQDweDfgOsPQ X-IronPort-AV: E=Sophos;i="4.89,702,1367964000"; d="scan'208";a="21715112" Received: from ppsw-32.csi.cam.ac.uk ([131.111.8.132]) by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Jul 2013 17:32:34 +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]:38600) by ppsw-32.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.156]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1V0CfZ-0004F2-1Z (Exim 4.80_167-5a66dd3) (return-path ); Fri, 19 Jul 2013 16:32:33 +0100 From: Leo White To: Ivan Gotovchits Cc: caml-list@inria.fr References: <877ggmx2pc.fsf@golf.niidar.ru> 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: Fri, 19 Jul 2013 16:32:33 +0100 In-Reply-To: <877ggmx2pc.fsf@golf.niidar.ru> (Ivan Gotovchits's message of "Fri, 19 Jul 2013 14:29:35 +0400") Message-ID: <87mwpitvji.fsf@kingston.cl.cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Subject: Re: [Caml-list] GADT: equal functions typechecks differently > type 'a pool = { > set : Set.t; > min : int; > max : int; > } > type 'a id = int > The difference between id and pool is that 'a id is equal to 'b id for any types 'a and 'b, since they are both equal to int, while 'a pool only equals 'b pool if 'a equals 'b. For example: # let f (x: int id) : float id = x;; val f : int id -> float id = # let f (x: int pool) : float pool = x;; Characters 35-36: let f (x: int pool) : float pool = x;; ^ Error: This expression has type int pool but an expression was expected of type float pool Type int is not compatible with type float Interestingly, 'a pool is a subtype of 'b pool for any 'a and 'b, so the following definition is allowed: # let f (x: int pool) : float pool = (x :> float pool);; val f : int pool -> float pool = This is why: > # let of_tid: type t1 t2. t1 sys -> tid -> t2 id option = > fun sys1 (Id (sys2,id)) -> > match try_sys_equal (sys1,sys2) with > | Some Eq -> Some id > | None -> None;; > val of_tid : 't1 sys -> tid -> 't2 id option = is accepted, but > let of_tpool: type t1 t2. t1 sys -> tpool -> t2 pool option = > fun sys1 (Pool (sys2,pool)) -> > match try_sys_equal (sys1,sys2) with > | Some Eq -> Some pool > | None -> None;; > Characters 158-162: > | Some Eq -> Some pool is disallowed. We could, however, write this function using subtyping: # let of_tpool: type t1 t2. t1 sys -> tpool -> t2 pool option = fun sys1 (Pool (sys2,pool)) -> match try_sys_equal (sys1,sys2) with | Some Eq -> Some (pool :> t2 pool) | None -> None;; val of_tpool : 't1 sys -> tpool -> 't2 pool option = Note that these functions are not really using any of the GADT constraints. They don't need to since any 'a id can be used as a t2 id and any 'a pool can be subtyped into a t2 pool. Regards, Leo