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

[Rodolphe Lepigre]

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

Hi there,

You might also be interested in the PML language, which was the subject
of my (recently defended) thesis.

Roughly, the ideas of PML are the following:
 - start with an ML-like programming language (polymorphism, recursion, ...),
 - extend the type system with a way of proving program properties,
 - put everything together with subtyping.

The main point of subtyping in this framework is to obtain a practical
way of type-checking Curry-style programs, which is difficult.

Here is a (non-exhaustive) list of features:
 - a very general form of implicit (non-coercive) subtyping,
 - Curry-style quantifiers and dependent function type,
 - an equality type for specifying program properties,
 - control operators (interpreted with classical logic),
 - general recursion with termination checking,
 - inductive and coinductive types (sized types).

Relevant papers and implementation:
  http://lepigre.fr/files/docs/lepigre2017_pml2.pdf (examples in PML)
  https://github.com/rlepigre/phd/blob/master/manuscript_archived.pdf (thesis)
  https://github.com/rlepigre/pml (implementation of PML)

More stuff on subtyping (joint work with Christophe Raffalli) and the SubML
language (which has subtyping, but does not have dependent types, but PML is
base on the same ideas):
  http://lepigre.fr/files/docs/lepigre2017_subml.pdf (subtyping theory)
  https://github.com/rlepigre/subml (SubML language implementation)
  https://rlepigre.github.io/subml (SubML language, try it online)

I hope this helps!

Cheers,
Rodolphe
-- 
Rodolphe Lepigre <rodolphe.lepigre at inria.fr>
Inria (Deducteam), LSV, CNRS, Université Paris-Saclay, FRANCE
https://lepigre.fr