From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id C1610BBAF for ; Mon, 26 May 2008 21:45:42 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqUAAN6vOkhTkhUIhmdsb2JhbACBVZBlAQEBCgUGBxMDmXs X-IronPort-AV: E=Sophos;i="4.27,543,1204498800"; d="scan'208";a="26627325" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 26 May 2008 21:45:42 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m4QJjfUB015590 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Mon, 26 May 2008 21:45:42 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqUAAN6vOkhTkhUIhmdsb2JhbACBVZBlAQEBCgUGBxMDmXs X-IronPort-AV: E=Sophos;i="4.27,543,1204498800"; d="scan'208";a="26627324" Received: from smtp.dslgb.com (HELO cht-smtp-002.bulldogdsl.com) ([83.146.21.8]) by mail4-smtp-sop.national.inria.fr with ESMTP; 26 May 2008 21:45:41 +0200 Received: by cht-smtp-002.bulldogdsl.com (Postfix, from userid 1002) id 57FF31E41B0; Mon, 26 May 2008 20:45:40 +0100 (BST) Received: from [192.168.123.191] (host-84-9-233-86.dslgb.com [84.9.233.86]) by cht-smtp-002.bulldogdsl.com (Postfix) with ESMTP id D15DF1E4193; Mon, 26 May 2008 20:45:36 +0100 (BST) Message-ID: <483B135E.7010002@ed.ac.uk> Date: Mon, 26 May 2008 20:45:34 +0100 From: Jeremy Yallop User-Agent: Mozilla-Thunderbird 2.0.0.14 (X11/20080509) MIME-Version: 1.0 To: Robert Fischer Cc: caml-list@inria.fr Subject: Re: [Caml-list] Question about type unification References: <20080526122204.GA6727@annexia.org> <20080526192157.3e75c121@orange.fr> <483B0F81.1020907@fischerventure.com> In-Reply-To: <483B0F81.1020907@fischerventure.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 483B1365.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; unification:01 compiler:01 denotes:01 denotes:01 constructors:01 wrote:01 abstract:01 caml-list:01 functions:01 constructor:01 constructor:01 data:02 string:02 string:02 module:03 Robert Fischer wrote: > How is the compiler magically getting from the float to a string value? Can someone break down > what's actually happening here for me? Type aliases are analogous to functions. If you have a variable "f" that denotes a pure function and some values u1 ... un and v1 ... vn then to determine whether f u1 ... un is equal to f v1 ... vn you call the function (twice) by substituting u1 ... un and v1 ... vn for the parameters. If you have a constant function f = fun _ ... _ = v then any application of the function will give the same result (v) regardless of the values of the arguments. Analogously, if you have a type constructor "t" that denotes a type alias and some types s1 ... sn and t1 ... tn then to determine whether (s1, ... sn) t is equal to (t1, ... tn) t you "call" the type alias by substituting s1 ... sn and t1 ... tn for the type parameters. If you have a "constant" type alias in which none of the type parameters appear on the right hand side of the definition type ('a1, ... 'an) t = e a1...an not in fv(e) then any application of the type constructor will give the same result (e) regardless of the values of the arguments. Nominal types are analogous to constructors. (By "nominal" I mean record and sum types, or types made abstract using a module signature.) If you have a data constructor "C" and some values u1 ... un and v1 ... vn then to determine whether C u1 ... un is equal to C v1 ... vn you check whether ui is equal to vi for each i. Analogously, if you have a type constructor "s" that denotes a nominal type and some types s1 ... sn and t1 ... tn then to determine whether (s1, ... sn) s is equal to (t1, ... tn) s you check whether si is equal to ti for each i. In Richard's example "t" denotes a type alias. Thus to determine whether unit t is equal to string t we look at the definition of t: type 'a t = float then replace each 'a that occurs on the right hand side first with "unit" and then with "string" and compare the results. In this case "'a" doesn't appear at all on the right hand side of the definition so we compare "float" with "float", and find that the two are equal, i.e. "unit t" and "string t" denote the same type (float). Jeremy.