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=HTML_MESSAGE, UNPARSEABLE_RELAY autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id A2A43BC0A; Thu, 21 Dec 2006 05:10:30 +0100 (CET) Received: from imr8.us.db.com (imr8.us.db.com [160.83.65.200]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBL4ASfg018843 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=FAIL); Thu, 21 Dec 2006 05:10:30 +0100 Received: from sdbo1005.db.com by imr8.us.db.com id kBL4ARtB021963; Wed, 20 Dec 2006 23:10:27 -0500 In-Reply-To: To: "Tom Cc: caml-list , caml-list-bounces@yquem.inria.fr Subject: Re: [Caml-list] What is "principal typing"? MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.5.5 CCH1 March 07, 2006 From: Jeff Polakow Message-ID: Date: Wed, 20 Dec 2006 23:10:24 -0500 X-MIMETrack: Serialize by Router on sdbo1005/DBNA/DeuBaInt/DeuBa(Release 6.5.4 HF129|May 12, 2005) at 12/20/2006 11:10:27 PM, Serialize complete at 12/20/2006 11:10:27 PM Content-Type: multipart/alternative; boundary="=_alternative 0016ECBE8525724B_=" X-Miltered: at concorde with ID 458A0934.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; polakow:01 polakow:01 typings:01 typable:01 typings:01 typable:01 inference:01 inference:01 lncs:01 jbw:01 lncs:01 jbw:01 2380:98 2002.:98 2002.:98 This is a multipart message in MIME format. --=_alternative 0016ECBE8525724B_= Content-Type: text/plain; charset="ISO-8859-1" Content-Transfer-Encoding: quoted-printable Hello, There are two notions, often conflated, which you might be referring to: principal types and principal typings. The following is taken from [1] which is worth reading if you're interested in this topic. Principal Types Given: a term M typable with type assumptions A. There exists: a type sigma representing all possible types for M in A. Principal Typings Given: a typable term M. There exists: a judgement A |- M : tau =1C representing all possible typings for M. Principal types, which ML has, are useful because, for a given context, there is a most general type for any typeable term. This is a useful property to have for languages which attempt type inference. Principal typeings, which ML does not have, are useful because they allow for compositional type inference (i.e. each piece of the program can be analyzed separately). [1] J. B. Wells. The essence of principal typings. In Proc. 29th Int'l Coll. Automata, Languages, and Programming, volume 2380 of LNCS, pages 913-925. Springer-Verlag, 2002. (http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typing= s:ICALP-2002.pdf) --Jeff --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden. --=_alternative 0016ECBE8525724B_= Content-Type: text/html; charset="ISO-8859-1" Content-Transfer-Encoding: quoted-printable
Hello,

  There are two notions, often conflated,  which you might be referring to: principal types and princ= ipal typings. The following is taken from [1] which is worth reading if you're interested in this topic.

    Principal Types
      Given: a term M typable with type assumptions A.
      There exists: a type sigma representing all possible types for M in A.

    Principal Typings
      Given: a typabl= e term M.
      There exists: a judgement A |- M : tau =1C representing all possible typings for M.

Principal types, which ML has, are u= seful because, for a given context, there is a most general type for any typeable term. This is a useful property to have for languages which attempt type inference.

Principal typeings, which ML does no= t have, are useful because they allow for compositional type inference (i.e. each piece of the program can be analyzed separately).

[1] J. B. Wells. The essence of prin= cipal typings. In Proc. 29th Int'l Coll. Automata, Languages, and Programming, volume 2380 of LNCS, pages 913-925. Springer-Verlag, 2002. (http://www.macs= .hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:ICALP-2002.pdf= )

--Jeff
---

This e-mail may contain confidential and/or privileged information. If= you
are not the intended recipient (or have received this e-mail in error)=
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in th= is
e-mail is strictly forbidden.
--=_alternative 0016ECBE8525724B_=--