[TYPES] I: On Dependent types and Subtyping's consistency

[Stefan Monnier]

> I am trying to check if it is possible to do reflection (as in Java)
> using "type safe" languages and, therefore, I am wondering if there is
> a language having dependent types with subtyping (in particular, I'm
> not talking of subtyping as in types' universes, but as in record
> subtyping). All the infos I got was a paper by Luca Cardelli dated
> 2000/2001 but, since then, it seems that whether the type system is
> consistent or not is still an open problem

I'm not completely sure what is your concrete goal (after all,
all cases of reflection I know of are in languages which are already
type-safe, such as Common-Lisp, Java, ...), but I wanted to point out
that you may not need subtyping in your type system, because you can
translate a type-system such as that of Java to a language without
subtyping (e.g. using row-polymorphism).

See for example:

    Precision in Practice: A Type-Preserving Java Compiler.
    Christopher League, Zhong Shao, and Valery Trifonov.  In Proc. 12th
    International Conference on Compiler Construction (CC'03), Warsaw,
    Poland, April 2003.

Where they compile Java to something similar to Fω.
I don't think Chris found the time to cover Java reflection, but from
what I remember of discussions at the time it's not necessarily too hard
to add, especially if you're willing to pay the price of a bit of
runtime tests in there.

Also, since they don't rely on subtyping in their target language, it's
probably easier to add dependent types to it.


        Stefan