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 discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 17F6ABC0A; Thu, 21 Dec 2006 22:03:10 +0100 (CET) Received: from imr6.us.db.com (imr6.us.db.com [160.83.65.199]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBLL38xj021145 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL); Thu, 21 Dec 2006 22:03:09 +0100 Received: from sdbo1005.db.com by imr6.us.db.com id kBLL33jh001532; Thu, 21 Dec 2006 16:03:04 -0500 (EST) 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: Thu, 21 Dec 2006 16:02:57 -0500 X-MIMETrack: Serialize by Router on sdbo1005/DBNA/DeuBaInt/DeuBa(Release 6.5.4 HF129|May 12, 2005) at 12/21/2006 04:03:04 PM, Serialize complete at 12/21/2006 04:03:04 PM Content-Type: multipart/alternative; boundary="=_alternative 0073A0B08525724B_=" X-Miltered: at discorde with ID 458AF68C.004 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; polakow:01 polakow:01 inference:01 typable:01 lambda:01 subtyping:01 subtyping:01 subtype:01 trivial:01 inference:01 typable:01 lambda:01 subtype:01 trivial:01 sans-serif:98 This is a multipart message in MIME format. --=_alternative 0073A0B08525724B_= Content-Type: text/plain; charset="US-ASCII" Hello, > Could you give some concrete example of a type inference engine and > a typable term, but which does not have a principal type? > Here is a silly example. Consider a simply typed lambda calculus with subtyping on base types (e.g. int < real) but no structural subtyping (i.e. no subtype relation between functions). Then things like the identity function have no principal type. There are less trivial systems out there where, usually involving subtying and/or type classes, where principal types either don't exist or were tricky to figure out. But I am several years removed from actively thinking about this stuff and can't recall off hand more specific details. -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 0073A0B08525724B_= Content-Type: text/html; charset="US-ASCII"
Hello,

> Could you give some concrete example of a type inference engine and
> a typable term, but which does not have a principal type?
>  
Here is a silly example. Consider a simply typed lambda calculus with subtyping on base types (e.g. int < real) but no structural subtyping (i.e. no subtype relation between functions). Then things like the identity function have no principal type.

There are less trivial systems out there where, usually involving subtying and/or type classes, where principal types either don't exist or were tricky to figure out. But I am several years removed from actively thinking about this stuff and can't recall off hand more specific details.

-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 0073A0B08525724B_=--