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 ED522BB84 for ; Fri, 19 May 2006 21:10:20 +0200 (CEST) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k4JJAIZZ012403 for ; Fri, 19 May 2006 21:10:20 +0200 Received: from rosella (ppp28-237.lns1.syd6.internode.on.net [59.167.28.237]) by smtp1.adl2.internode.on.net (8.13.6/8.13.5) with ESMTP id k4JJA9Yt095952; Sat, 20 May 2006 04:40:09 +0930 (CST) (envelope-from skaller@users.sourceforge.net) Subject: Re: [Caml-list] compiler bug? From: skaller To: Jacques Carette Cc: caml-list@yquem.inria.fr In-Reply-To: <446DF6C0.4090000@mcmaster.ca> References: <20060517231426.30289.qmail@web32203.mail.mud.yahoo.com> <446CABCA.8000906@inria.fr> <446CB021.6000009@mcmaster.ca> <1147976357.25630.27.camel@rosella.wigram> <446CC2C1.5040801@mcmaster.ca> <1148003249.25630.29.camel@rosella.wigram> <446DF6C0.4090000@mcmaster.ca> Content-Type: text/plain Date: Sat, 20 May 2006 05:10:08 +1000 Message-Id: <1148065808.15638.56.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 446E181A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; compiler:01 bug:01 haskell:01 untyped:01 well-typed:01 syntax:01 untyped:01 rewrites:01 ocaml:01 statically:01 metaocaml:01 statically:01 manipulates:01 semantics:01 semantics: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 Fri, 2006-05-19 at 12:48 -0400, Jacques Carette wrote: > skaller wrote: > > >>>What about high level optimisations? > >>> > >>>Felix supports this: > >>> > >>> reduce revrev[t] (x:list[t]): rev (rev x) => x; > >>> > >>> > >>Haskell (GHC to be precise) allows that too. But is syntactic > >>term-rewriting, in other words it is *untyped*. > >It's well typed. x:list[t] means x is of type list[t]. > > > > > The *result* is well-typed. What is the 'type' of the rule (ie the > 'function' reduce) ? > reduce acts on the programming language syntax, > not on semantic values. Yes, but so what? Originally you said it was *untyped*. As if it were like a macro which rewrites all terms rev (rev x) to x but this is not the case. The thing is Felix ALSO has macros which are indeed untyped: macro fun f(x) = x + x; so f x is replaced by x + x everywhere the f is in scope. So when you later said "Ocaml is great because it is statically typed. MetaOCaml is wonderful because it is statically typed. Adding an untyped layer to a typed language seems like a definite step backwards (i.e. a hack).. " I think you're missing the point: I'd agree with that comment and also agree it applied to Felix macros, because they are indeed manipulations of untyped terms. Macro processing is done first, before typing. But 'reduce' is done after typing, it manipulates typed terms: it isn't adding an *untyped* layer to the system, on the contrary the semantics implied are actually *beyond* ordinary static typing. We have learned: rev ^ 2 = id (revrev) and this property of 'rev' is a constraint on its semantics (but of course not a complete specification). What one might say is that the mechanism is somewhat ad hoc rather than being systematic. The problem here, if any, you yourself pointed out in private email some time ago -- there's no assurance the rules are actually reductions: one or more such rules may well diverge. -- John Skaller Felix, successor to C++: http://felix.sf.net