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

[Sandro Stucki]

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.stucki at 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.scherer at 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.bergami2 at 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/
>>>