[Prev][Next][Index][Thread]
Re: Subject reduction fails in Java  coercions of Luo

To: Zhaohui Luo <Zhaohui.Luo@durham.ac.uk>

Subject: Re: Subject reduction fails in Java  coercions of Luo

From: Gang CHEN <Chen.Gang@ens.fr>

Date: Sat, 20 Jun 1998 19:59:22 +0200

CC: types@cs.indiana.edu

DeliveryDate: Sat, 20 Jun 1998 13:12:51 0500

References: <199806191756.MAA12569@shovelnose.cs.indiana.edu>
Zhaohui Luo wrote:
> Javaconversions (the widening conversions) can be regarded as what we
> have called "coercions". In the framework of coercive subtyping, if
> f:K>K', a:K0, and K0 <_c K (ie, K is a subtype via coercion c), then
>
> f(a) is computationally equal to (reduces to) f(c(a))
>
> In particular, ([x:K]b)(a) does not reduce to [a/x]b, but it reduces to
>
> ([x:K]b)(c(a)) (coercion insertion as reduction)
>
> which betareduces to [c(a)/x]b. In other words, reductions such as beta
> cannot be done directly when the argument's type is a proper subtype of
> the required type; instead, a coercion (or typecasting operation, or
> conversion in Java's term) has to be inserted (as a step of reduction)
> before the reduction (beta in the above example) can be done. ...
I agree with the main idea of coercion inference. But it is not clear why
coercion insertion takes place at run time? It seems less efficient than the
coercion inference at compile time .
> I am very interested in this and hope to get your further opinions. Do
> you know of other related work that uses the similar ideas to deal with
> these situations? (Please let me know if so.)
>
In my thesis (available at http://www.dmi.ens.fr/~gang), I have studied
coercive subtyping to the Calculus of Constructions(CC). It contains proofs of
the completeness of coercion and the completeness of coercion inference among
other things.
I have not changed the notion of reduction. In implementation, coercion
inference of a term should be done before its execution.
Regards.
Gang Chen