Re: [TYPES] ?==?utf-8?q? ?==?utf-8?q? I: On D ependent types and Subtyping's consistency

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

You may also have a look at the page of Zhaohui Luo at Royal Holloway,
there are several papers on coercive subtyping, coherence problems etc
for dependent types.

https://www.cs.rhul.ac.uk/home/zhaohui/subtyping.html

Sergei Soloviev 
 
 
Le Mardi 12 Décembre 2017 13:09 CET, Sandro Stucki <[email protected]> a écrit: 
 
> [ 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 <[email protected]> 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
> > <[email protected]> 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 <[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/
> >>>