From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 75900BBC4 for ; Sun, 22 Jan 2006 04:17:24 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0M3HNVg016093 for ; Sun, 22 Jan 2006 04:17:23 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id EAA23746 for ; Sun, 22 Jan 2006 04:17:23 +0100 (MET) Received: from ash25e.internode.on.net (ash25e.internode.on.net [203.16.214.182]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0M3HLPR016090 for ; Sun, 22 Jan 2006 04:17:22 +0100 Received: from rosella (ppp21-250.lns2.syd7.internode.on.net [59.167.21.250]) by ash25e.internode.on.net (8.13.5/8.13.5) with ESMTP id k0M3Gurl080253; Sun, 22 Jan 2006 13:47:10 +1030 (CST) (envelope-from skaller@users.sourceforge.net) Subject: Re: [Caml-list] Coinductive semantics From: skaller To: Andrej.Bauer@andrej.com Cc: Caml list In-Reply-To: <43D27F18.9030102@andrej.com> References: <43C51C33.2000206@andrej.com> <1137031853.3681.138.camel@rosella> <43C661AF.2080404@andrej.com> <1137102848.3681.268.camel@rosella> <1137163342.3681.533.camel@rosella> <1137594157.8943.106.camel@rosella> <20060120004948.GA2490@coruscant.stwing.upenn.edu> <43D0B413.1060806@andrej.com> <20060120185911.GA22920@coruscant.stwing.upenn.edu> <1137790790.15137.39.camel@rosella> <43D27F18.9030102@andrej.com> Content-Type: text/plain Date: Sun, 22 Jan 2006 14:16:55 +1100 Message-Id: <1137899816.885.45.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 43D2F943.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43D2F941.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 andrej:01 andrej:01 algebra:01 rec:01 rec:01 bool:01 associative:01 notation:01 bool:01 pointer:01 pointer:01 arrays:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 On Sat, 2006-01-21 at 19:36 +0100, Andrej Bauer wrote: > skaller wrote: > > How would you decode an Andrej sum without a conditional > > control transfer? > > The control is a consequence of the fact that natural numbers are an > inital algebra Hmm .. > rec x f 0 = x > rec x f (n+1) = f (rec x f n) Yeah. Of course, natural numbers subsume bool: the switch is right there already. Thanks! FYI in Felix 0,1,2 .. etc are types given by n = 1 + 1 + .. + 1. Not quite natural numbers (since + isn't strictly associative). For any sum t a variant has notation like case 5 of t in particular the components of bool = 2 are names false = case 1 of 2 and true = case 2 of 2. The underlying representation is a tagged pointer, with the pointer optimised away if no variant has a (non-unit) argument. Since the tag is an int, the run time representation of a unit sum is just an int. I also have arrays t ^ n = t * t * t * .. * t. In principle, the j'th component is found by indexing function: prj: t ^ n * n -> t Unlike 'normal' array indexing .. this is entirely safe. BTW I learned this trick from Pascal, which never needs array bounds checks -- you have to check conversion int ==> n of the index instead. What I don't know how to do is extend the collection of fixed length array types, kind of like (lim n-> inf) Sum (t ^ n) Of course I know how to *implement* this infinite sum. (Which in practice isn't infinite of course) The problem is that I have to somehow convert from a run time dynamic type (the array bound is a type!) to an integer with a 'super switch'. Rougly the projection for the above limit is typematch .. with .. ... | 5 => let j = check 5 i in a.[j] ... in other words its an infinite switch over all the fixed length array types. Clearly for this particular case the implementation is just to do an dynamic array bounds check the way Ocaml does. But this is very unsatisfying, and in particular provides no way to optimise away gratuitous checks at compile time. In other words, you can't compose these things. I'm not sure my rant really explains what I'm looking for: basically I don't know enough theory to turn the purely algebraic finite array types -- fairly useless in practice -- into variable length arrays required in practice. [By variable I mean the length is an immutable dynamic type, not that you can change the length of the array] It would be really nice -- in BOTH Felix and Ocaml -- to have safe arrays. Unlike lists, functions like combine and split then make sense. -- John Skaller Felix, successor to C++: http://felix.sf.net