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.5 required=5.0 tests=AWL,DATE_IN_PAST_06_12 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 53DA8BC6B for ; Tue, 28 Aug 2007 22:28:40 +0200 (CEST) Received: from sympodial.rsise.anu.edu.au (sympodial.rsise.anu.edu.au [150.203.208.213]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l7SKSawg031646 for ; Tue, 28 Aug 2007 22:28:39 +0200 Received: from localhost (localhost [127.0.0.1]) by sympodial.rsise.anu.edu.au (Postfix) with ESMTP id 375A181D8 for ; Wed, 29 Aug 2007 06:28:35 +1000 (EST) X-Virus-Scanned: Debian amavisd-new at rsise.anu.edu.au Received: from sympodial.rsise.anu.edu.au ([127.0.0.1]) by localhost (backend1.rsise.anu.edu.au [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 4Cham7LLCEsB for ; Wed, 29 Aug 2007 06:28:28 +1000 (EST) Received: from pulp.rsise.anu.edu.au (pulp.rsise.anu.edu.au [150.203.208.49]) by sympodial.rsise.anu.edu.au (Postfix) with ESMTP for ; Wed, 29 Aug 2007 06:28:12 +1000 (EST) Received: by pulp.rsise.anu.edu.au (Postfix, from userid 1560) id BA0B8A0FFCB; Tue, 28 Aug 2007 23:18:50 +1000 (EST) Date: Tue, 28 Aug 2007 23:18:50 +1000 From: Pietro Abate To: ocaml ml Subject: how to upset the ocaml type system.... Message-ID: <20070828131850.GA32264@pulp.rsise.anu.edu.au> Mail-Followup-To: Pietro Abate , ocaml ml MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline X-Operating-System: GNU/Linux X-Organization: Research School of Information Science and Engineering (Australian National University) User-Agent: Mutt/1.5.13 (2006-08-11) X-Miltered: at discorde with ID 46D48574.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 inference:01 worst-case:01 unification:01 blog:98 blog:98 polymorphic:01 typing:01 algorithm:01 philosophy:02 let:03 let:03 examples:07 exhibit:07 fun:08 hi all, the other day I was looking for a fringe case to show me the worst complexity of the type inference algorithm... I think I found what I was looking for: let x1 = fun x -> (x,x) in let x2 = fun y -> x1 ( x1 y ) in let x3 = fun y -> x2 ( x2 y ) in let x4 = fun y -> x3 ( x3 y ) in let x5 = fun y -> x4 ( x4 y ) in let x6 = fun y -> x5 ( x5 y ) in let x7 = fun y -> x6 ( x6 y ) in x7 ( fun z -> z ) ;; are there any other examples that exhibit worst-case complexity ? pietro ps: the example is from the paper "polymorphic unification and ML typing" from kannellakis -- ++ Blog: http://blog.rsise.anu.edu.au/?q=pietro ++ ++ "All great truths begin as blasphemies." -George Bernard Shaw ++ Please avoid sending me Word or PowerPoint attachments. See http://www.fsf.org/philosophy/no-word-attachments.html