[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
An additional example is: "Pure Subtype Systems", POPL 2010 https://dl.acm.org/citation.cfm?id=1706334 Which shows that you can combine subtyping and dependent typing into a single relation. The PSS theory is currently incomplete -- you need a stratified universe of types to prove strong normalization. - DeLesley On Tue, Dec 12, 2017 at 4:09 AM, Sandro Stucki <sandro.stu...@epfl.ch> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > There are several instances of Pure Type Systems (PTS) combining > dependent types and subtyping in the literature. For example > > Subtyping dependent types > David Aspinall, Adriana Compagnoni. TCS, 2001 > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > Pure Type Systems with Subtyping > Jan Zwanenburg. TLCA 1999 > http://dx.doi.org/10.1007/3-540-48959-2_27 > > Unifying Typing and Subtyping > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > The latter two feature F-omeag-sub-like higher-order subtyping, but > none have polarized higher-order subtyping (in the style of Abel's > 2008 paper mentioned by Gabriel). > > Cheers > /Sandro > > On Tue, Dec 12, 2017 at 1:07 PM, Sandro Stucki <sandro.stu...@gmail.com> > wrote: > > There are several instances of Pure Type Systems (PTS) combining > > dependent types and subtyping in the literature. For example > > > > Subtyping dependent types > > David Aspinall, Adriana Compagnoni. TCS, 2001 > > http://www.sciencedirect.com/science/article/pii/S0304397500001754 > > > > Pure Type Systems with Subtyping > > Jan Zwanenburg. TLCA 1999 > > http://dx.doi.org/10.1007/3-540-48959-2_27 > > > > Unifying Typing and Subtyping > > Yanpeng Yang, Bruno C. d. S. Oliveira, OOPSLA 2017 > > http://i.cs.hku.hk/~bruno/papers/oopsla17.pdf > > > > The latter two feature F-omeag-sub-like higher-order (HO) subtyping, > > but none have polarized higher-order subtyping (in the style of Abel's > > 2008 paper mentioned by Gabriel). > > > > Cheers > > /Sandro > > > > On Tue, Dec 12, 2017 at 11:45 AM, Gabriel Scherer > > <gabriel.sche...@gmail.com> wrote: > >> [ 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 < > giacomo.berga...@unibo.it > >>> 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/ > >>> >