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 65C0F7EE25 for ; Fri, 25 Oct 2013 01:23:23 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArcBADmraVKFBoIFnGdsb2JhbABZhzq7LIE1DgEBAQEBCBQJPIIlAQEEASMEHAE1AgMLCQIODAIYDgICVwYTiAEFjAGaZ3aDYwKFYokNB4EpjXEzB4JqNYENiUCOTZU6 X-IPAS-Result: ArcBADmraVKFBoIFnGdsb2JhbABZhzq7LIE1DgEBAQEBCBQJPIIlAQEEASMEHAE1AgMLCQIODAIYDgICVwYTiAEFjAGaZ3aDYwKFYokNB4EpjXEzB4JqNYENiUCOTZU6 X-IronPort-AV: E=Sophos;i="4.93,565,1378850400"; d="scan'208";a="38681899" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 25 Oct 2013 01:23:14 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4EBAA63A5; Fri, 25 Oct 2013 08:23:14 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id CAC802564; Fri, 25 Oct 2013 08:23:13 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 69548251A; Fri, 25 Oct 2013 08:23:13 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 7.0 \(1816\)) From: Jacques Garrigue In-Reply-To: Date: Fri, 25 Oct 2013 08:23:12 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> References: To: Peter Frey X-Mailer: Apple Mail (2.1816) Subject: Re: [Caml-list] Equality between abstract type definitions 2013/10/25 7:57=E3=80=81Peter Frey =E3=81=AE=E3=83=A1= =E3=83=BC=E3=83=AB=EF=BC=9A > Please consider the following two definitions of map which I would have > considered equal.=20=20 >=20 > exception Empty >=20 > type 'a t =3D Cons of 'a * (int -> 'a t) * int >=20 > let null =3D Cons( Obj.magic None, (fun _ -> assert false), max_int )=20 >=20 > let map (f: 'a -> 'b) (t: 'a t) : 'b t =3D > if t =3D=3D null then null else match t with (Cons( h, fn, p )) -> > let rec aux h1 p1 =3D > try match fn p1 with (Cons (h2,_, p2)) ->=20 > (Cons(f h1, aux h2, p2 )) > with Empty -> (Cons(f h1, fn, p1)) in > aux h p >=20 > let map : 'a 'b. ( 'a -> 'b ) -> 'a t -> 'b t =3D fun f t ->=20 > if t =3D=3D null then null else match t with (Cons( h, fn, p )) -> > let rec aux h1 p1 =3D > try match fn p1 with (Cons (h2,_, p2)) -> (Cons(f h1, aux h2, 2 )) > with Empty -> (Cons(f h1, fn, p1)) in > aux h p >=20 > The second one gives the error below; no surprise. >=20 > Error: This definition has type 'b. ('b -> 'b) -> 'b t -> 'b t > which is less general than 'a 'b. ('a -> 'b) -> 'a t -> 'b t >=20 > Why is the first definition accepted?=20=20 Here is the type inferred for the first definition: val map : ('b -> 'b) -> 'b t -> 'b t =3D As you can see, types for =E2=80=98a and =E2=80=98b are merged. In OCaml, type variables used in type annotations are just unification vari= ables: the type checker is allowed to merge them or instantiate them. This is useful when you want to indicate that two things have the same type, without writing the type by hand. In the second example you use an explicit polymorphic type, which does not allow instantiating =E2=80=98a and =E2=80=98b, so you get an error. Jacques Garrigue=