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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 11082BC69 for ; Wed, 15 Aug 2007 05:03:09 +0200 (CEST) Received: from ipmail01.adl2.internode.on.net (ipmail01.adl2.internode.on.net [203.16.214.140]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l7F336oS003247 for ; Wed, 15 Aug 2007 05:03:08 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPIGwkZ5LGJp/2dsb2JhbAAN X-IronPort-AV: E=Sophos;i="4.19,262,1183300200"; d="scan'208";a="172836977" Received: from ppp121-44-98-105.lns10.syd6.internode.on.net (HELO [192.168.1.201]) ([121.44.98.105]) by ipmail01.adl2.internode.on.net with ESMTP; 15 Aug 2007 12:32:53 +0930 Subject: divergent type From: skaller To: caml-list@yquem.inria.fr Content-Type: text/plain Date: Wed, 15 Aug 2007 13:02:51 +1000 Message-Id: <1187146971.6765.22.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 46C26CEA.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 compiler:01 ocaml:01 -rectypes:01 val:01 polymorphism:01 val:01 recursion:01 pointers:01 variants:01 pointers:01 recursive:01 recursive:01 recursion:01 distinctions:01 Sorry for asking a general typing question not specifically related to Ocaml .. also, I don't really know how to ask the question properly (if I did I would know the answer too). I have a problem in Felix compiler with infinite types. For example the type of fun f(x:int)=>x,f x is (int * u) as u which cannot be represented. In Ocaml with -rectypes this is a legitimate type: # let rec x = 1,x;; val x : int * 'a as 'a = (1, (1,... which is representable because Ocaml uses boxing (intensional polymorphism).Smly: # let rec f x = 1, f x;; val f : 'a -> (int * 'b as 'b) = Felix supports type recursion through pointers, variants also allow it because they're modelled as pointers (boxed), and of course functions are boxed (closures). However some type equations (recursive types) have no solution at all: # let rec f x = f (x,x);; val f : ('a * 'a as 'a) -> 'b = The return type is divergent: Ocaml put 'b here, but it is a 'hack' the type of the value 'returned' is unrelated to the type of the value input. Note that this function CAN be modified to actually return a definite value: let rec f n x = if x <= 0 then () else f (n-1) (x,x) is convergent. (It is dependently type-able?) In any case there seem to be THREE kinds of type: 1. Ordinary types. 2. Finite Recursive types (eg lists) 3. Divergent types Perhaps someone can throw a bit more light on this? In Felix I need to detect the difference between an incidental recursion (a polymorphic function just happens to call itself for an unrelated/non-recursive purpose such as mapping a tuple: such 'recursion' always terminates because the input term is finite), a representable recursive type (such as a list), and an infinite expansion. And I note the distinctions are not representation independent (since Ocaml can handle recursive products whilst Felix cannot do so without using a pointer). Help! -- John Skaller Felix, successor to C++: http://felix.sf.net