From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 33CBFBBBB for ; Sun, 22 Jan 2006 16:36:13 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0MFaCdO018539 for ; Sun, 22 Jan 2006 16:36:12 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA31732 for ; Sun, 22 Jan 2006 16:36:11 +0100 (MET) Received: from ash25e.internode.on.net (ash25e.internode.on.net [203.16.214.182]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0MFa9O8018535 for ; Sun, 22 Jan 2006 16:36:11 +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 k0MFZnIV048062; Mon, 23 Jan 2006 02:06:00 +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: <43D37955.90408@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> <1137899816.885.45.camel@rosella> <43D37955.90408@andrej.com> Content-Type: text/plain Date: Mon, 23 Jan 2006 02:35:48 +1100 Message-Id: <1137944149.8961.103.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 43D3A66C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43D3A66A.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 compilers:01 compiler:01 compiler:01 inserting:01 runtime:01 arrays:01 categorical:01 nat:01 nat:01 ocaml:01 wrote: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 Sun, 2006-01-22 at 13:23 +0100, Andrej Bauer wrote: > skaller wrote: > If everyone believed in type theory, compilers would be easy to write. LOL! > Every time a programmer wanted to address an element of an array, he > would provide not just the index k but also the proof p that k is a > valid index. Compiler would just have to check that p is a valid proof > (easy when p is a formal proof). But programmers don't want to do that. Actually some of us would like to do it .. however this is moving past my real problem. I'm willing to accept that the typing may end up being unsound in the sense the compiler cannot prove what it needs to: this is actually easy to fix, by simply inserting a runtime check. Also, in this particular case (arrays) the run time representation is already known (literally it is the same as a variant, where the discriminant tag is the array length). This is very nice, since you can actually match on it against particular constant lengths. My problem is more categorical: given your explanation that this is a dependent typing thing, how do I represent such typing in the compiler? If the type of the *value* of the array bound is a unitsum, what is the type of the store containing that value? In particular if I have a match: match somearray_of_float with | (case 1 of NAT) data => ... // 0 elements | (case 2 of NAT) data => ... // 1 elements | (case ?n of NAT) data => // n-1 elements what is NAT? At present my type system only has terms like: type t = [ | `tuple of t list | `sum of t list | `unitsum of int ... so they're all just constants. How do I modify the type system to allow for a variable? Do I have to actually put executable terms into the type terms? That would account for construction, what about destructors (pattern matches)? Clearly the match has to get out a run time representation of the length .. but it isn't an integer: I mean, the encoding at run time is certainly an integer .. but what is the type ascribed to this value? I called it NAT above .. what, categorically, is NAT? BTW: I think all this analysis could apply to Ocaml too. -- John Skaller Felix, successor to C++: http://felix.sf.net