From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <dra-news@metastack.com>
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=none autolearn=disabled 
	version=3.1.3
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id 2C8C7BC6B
	for <caml-list@yquem.inria.fr>; Tue, 28 Aug 2007 23:21:57 +0200 (CEST)
Received: from anchor-post-35.mail.demon.net (anchor-post-35.mail.demon.net [194.217.242.85])
	by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l7SLLuNS028315
	for <caml-list@inria.fr>; Tue, 28 Aug 2007 23:21:56 +0200
Received: from orion.metastack.com ([80.177.38.218])
	by anchor-post-35.mail.demon.net with esmtp (Exim 4.42)
	id 1IQ8VY-000CRF-HB
	for caml-list@inria.fr; Tue, 28 Aug 2007 21:21:56 +0000
Received: from countertenor (82-34-66-28.cable.ubr02.gill.blueyonder.co.uk [82.34.66.28])
	(authenticated bits=0)
	by orion.metastack.com (8.13.4/8.13.3) with ESMTP id l7SL5dWU023749
	(version=TLSv1/SSLv3 cipher=RC4-MD5 bits=128 verify=NO)
	for <caml-list@inria.fr>; Tue, 28 Aug 2007 22:05:40 +0100
From: "David Allsopp" <dra-news@metastack.com>
To: "'ocaml ml'" <caml-list@inria.fr>
References: <20070828131850.GA32264@pulp.rsise.anu.edu.au>
Subject: RE: [Caml-list] how to upset the ocaml type system....
Date: Tue, 28 Aug 2007 22:21:52 +0100
Organization: MetaStack Solutions Ltd.
Message-ID: <004c01c7e9b9$7460a1e0$017ca8c0@countertenor>
MIME-Version: 1.0
Content-Type: text/plain;
	charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Mailer: Microsoft Office Outlook 11
In-Reply-To: <20070828131850.GA32264@pulp.rsise.anu.edu.au>
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.3138
Thread-Index: AcfpsI/VdJ4TKFjkTTGMW6764rd3twAB9f3Q
X-Miltered: at concorde with ID 46D491F4.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; ocaml:01 worst-case:01 computes:01 checker:01 translated:01 caml-list:01 pair:01 pair:01 expression:02 languages:03 programming:03 let:03 let:03 types:05 exponential:05 

> are there any other examples that exhibit worst-case complexity ?

let pair = fun x -> (fun y -> (fun z -> ((z x) y)))
in
  let x1 = fun y -> (pair y) y
  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
            x5 (fun y -> y);;

This one computes much faster (by which I mean the type checker does get
there in a few minutes!) but demonstrates the exponential blow-up of the
length of a type compared with the code it comes from (the type of this
expression 131070 lines long on my console...). It is translated from
http://www.cl.cam.ac.uk/teaching/2006/Types/typ.pdf p. 29 (Slide 25) which
is itself from Mairson, H. G. (1990). Deciding ML typability is complete for
deterministic exponential time. (In Proc. 17th ACM Symposium on Principles
of Programming Languages, pp. 382--401.)


David