[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
An older work in which you have a limited form of intersection types is:
G. Castagna and G. Chen: Dependent types with subtyping and late-bound
overloading. Information and Computation, vol. 168, n. 1, pag. 1-67,
2001. https://www.irif.fr/~gc/papers/infcomp99.pdf
and you may be also interested in
AC96b. D. Aspinall and A. Compagnoni. Subtyping dependent types. In
Proc. 11th Annual Synposium on Logic
in Computer Science, IEEE, pages 86–97, 1996
Beppe
On 12/12/17 11:45, Gabriel Scherer 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/
