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

[Gabriel Scherer]

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/
>