[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
There is a language with dependent types and subtyping (including contravariant functions) in: Normalization by Evaluation for Sized Dependent Types Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) http://www.cse.chalmers.se/~abela/icfp17-long.pdf However, subtyping there is not "higher-order" in the sense of having type-indexed parameters themselves indicate a variance (you cannot abstract over all covariant parametrized types) -- pi-types only track relevant and irrelevant abstraction. In contrast, see the "higher-order subtyping" for F-omega-sub in Polarized Subtyping for Sized Types Andreas Abel, 2008 http://www.cse.chalmers.se/~abela/mscs06.pdf For higher-order subtyping in dependent systems, the two references I know of happen to be also mentioned on the nLab wiki: https://ncatlab.org/nlab/show/directed+homotopy+type+theory they are the work by Harper and Licata on directed type theory (and Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. 2-Dimensional directed dependent type theory Robert Harper, Dan Licata, 2011 http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf Dependently Typed Programming with Domain-Specific Logics Dan Licata, 2011 http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance Andreas Nuyts, 2015 http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami <[email protected] > wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hello Everyone, > > 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 ( http://lucacardelli.name/Papers/Dependent% > 20Typechecking.US.pdf ). > Therefore, I'm wondering if there are any advances on this > regard: moreover, it seems to be that no proof assistant supports this > technology. > Thanks in advance for any reply, > > Giacomo Bergami > Ph.D Student > University of Bologna > https://jackbergus.github.io/ >
