Re: [Caml-list] compiler bug?

[skaller <skaller@users.sourceforge.net>]

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 <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net