[Prev][Next][Index][Thread]

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



Zhaohui Luo wrote:

> Java-conversions (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 beta-reduces 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 type-casting 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