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 777297F0A3 for ; Sat, 22 Aug 2015 11:23:06 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.217.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yallop@gmail.com designates 209.85.217.169 as permitted sender) identity=mailfrom; client-ip=209.85.217.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-lb0-f169.google.com) identity=helo; client-ip=209.85.217.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-lb0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BCAgBRPthVlanZVdFeg29pBoMfrmyNRIYDAoEiB0wBAQEBAQESAQEBAQcNCQkfMIQjAQEBAwESEQQZARsdAQMBCwYFCw0CAiYCAiIBEQEFARwGEyKHdgEDCgigEoEvPjGLQIFsgnmKNQoZJw1XhQABAQEHAQEBARgBBQ6BFIo1hQoHgmmBQwWVNIUFh2uCEJZxEiOBFxeEDT0zgkwBAQE X-IPAS-Result: A0BCAgBRPthVlanZVdFeg29pBoMfrmyNRIYDAoEiB0wBAQEBAQESAQEBAQcNCQkfMIQjAQEBAwESEQQZARsdAQMBCwYFCw0CAiYCAiIBEQEFARwGEyKHdgEDCgigEoEvPjGLQIFsgnmKNQoZJw1XhQABAQEHAQEBARgBBQ6BFIo1hQoHgmmBQwWVNIUFh2uCEJZxEiOBFxeEDT0zgkwBAQE X-IronPort-AV: E=Sophos;i="5.15,727,1432591200"; d="scan'208";a="143503944" Received: from mail-lb0-f169.google.com ([209.85.217.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Aug 2015 11:23:05 +0200 Received: by lbcbn3 with SMTP id bn3so56021684lbc.2 for ; Sat, 22 Aug 2015 02:23:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=h5fY7SkJlPsS3pZ3CNBEXsts93SjLj9bEhs6SieFyyk=; b=qKKf3pZqxKmNiN2FNDBGXrb08PQvcRQvNFVi3bWkXUvVAxP0Qz/XVUBe22oTpRifG8 AfmrURPSrMYXPCiFPZZ0sq/+Oye/ArM6FsBx0/tCuzLCV7k1rN0/Bee3dHfY8IKhjT78 ouVT4jdEmlkEKq51PWOnD5u2NZvNesvKgDQkLdH4dUvPTOsGvMzCywFyl65HqWp9Zr05 wXG+FHmkBWeQZadYjN153L9kRD1LOA6T31nCupUICJvjkcT5o7/VVSOFPM2tMMX5dHs3 CRTdkQ9lbLNaLJ9ImI1AuX2ftHZTog8d7HLx4ytLm2Qd5oKK32knWggzeqB7uY4FeAC/ V0PA== MIME-Version: 1.0 X-Received: by 10.112.204.162 with SMTP id kz2mr11949395lbc.115.1440235384775; Sat, 22 Aug 2015 02:23:04 -0700 (PDT) Received: by 10.25.140.87 with HTTP; Sat, 22 Aug 2015 02:23:04 -0700 (PDT) In-Reply-To: <55D827DB.3010506@tu-berlin.de> References: <55D827DB.3010506@tu-berlin.de> Date: Sat, 22 Aug 2015 10:23:04 +0100 Message-ID: From: Jeremy Yallop To: =?UTF-8?Q?Christoph_H=C3=B6ger?= Cc: caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Expansion of type-constructors in ctype.ml On 22 August 2015 at 08:42, Christoph H=C3=B6ger wrote: > 1. In the case of equality, it seems fairly simple. Iff the path of two > constructors is the same and both argument lists are equal, the types > are equal, right? "If", but not "iff", unless you expand first. Consider type 'a t =3D unit Then 'int t' and 'float t' should be considered equal, since they both expand to 'unit', even though the argument lists are unequal > 2. In the case of unification, if both paths are the same, the argument > lists are of the same length, we can directly unify the arguments, right? Again, you need to expand the path first. Consider the following function, using the same definition of 't' as above: fun (a : 'a) (b : 'b) -> let c : 'a t =3D () and d : 'b t =3D () in ignore [c; d]; The last line involves unifying the types 'a t and 'b t. Unifying the type arguments 'a and 'b results in the following type for the function: 'a -> 'a -> unit Expanding 't' before unifying means that 'a and 'b are not unified, and the function can be given the more general type: 'a -> 'b -> unit