Re: subject reduction fails in Java

Benjamin Pierce [pierce@cs.indiana.edu] writes (approximately
>One possible way of formalizing this intuition is to alter the
>beta-reduction rule so that:
>  Object m (Object a1, Object a2) {
>    return (b ? a1 : a2);
>  }
>  Object o = m (i, h);
>is rewritten as 
>  Object o = (b ? (Object)i : (Object)h);

Or, more generally, with types A<B<C, g(x),and h(x,y) denoting arbitrary
expressions that involve their arguments:

B b f(A a1,A a2) {return(h(a1,a2));}
C o=g(f(x,y))

should always reduce to

C o=g((B) (h( ((A)a1) , ((A)a2) )) )

Isn't this just how the reduction _should_ be done in typed, lexically
scoped languages?  Because the language is lexically scoped, you cannot
substitute an expression without substituting the context in which it
was written, including types and bindings.


Matt Timmermans               | Phone:  +1 613 596-2233
Microstar Software Ltd.       | Fax:    +1 613 596-5934
3775 Richmond Road            | E-mail: mtimmerm@microstar.com
Nepean Ontario CANADA K2H 5B7 | Web: http://www.microstar.com