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

[Giacomo Bergami]

> \varepsilon : S_1 -> S_2 such that S_2 <: S_1

p.s. If I have that the type system is consistent, then I can also provide side proofs within my "programming-language-proof-assistant" and check whether my data manipulation function \varepsilon actually does what I expect.
________________________________________
Da: Types-list <types-list-bounces at LISTS.SEAS.UPENN.EDU> per conto di Giacomo Bergami <giacomo.bergami2 at unibo.it>
Inviato: martedì 12 dicembre 2017 15:27
A: Stefan Monnier
Cc: types-list at lists.seas.upenn.edu
Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency

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

Actually, my goal are data manipulation using a type safe system. I'm going to provide some practical examples and some definitions (forgive the abuse of notation).

a) Dependent Type language is required because I want to express operations that manipulate data at the schema level which, in type theory, corresponds to  type manipulation.  I would like that one of my functions within the programming language takes a type as an input, and manipulates it as an output type  (maybe homotopy type theory comes here in help...?) This comes in help in the data integration scenario, where data translation are provided.

The usage of dependent types in relational database scenarios has some examples in this Idris book: https://www.manning.com/books/type-driven-development-with-idris

b) Subtyping is required when I know that an operation, such as an embedding, increases the schema of my relation, and hence i want to express the property:

\varepsilon : S_1 -> S_2 such that S_2 <: S_1

Counterwise, the projection operator reduces the schema of my elements, and hence

\pi : S_1 -> S_2 such that S_2 :> S_1

In particular, I'm referring to Java libraries like Apache Spark and jOOQ which perform the aforementioned operations in a language which doesn't have dependant types.

My relational database (after a SQL query) might generate a set of tuples (then, list of terms) of a given  schema at the programming level side (all the returned terms have the same type) which is "untyped" (the result provided by the Java  JDBC interface has no explicit final schema, it is generally a ResultSet). The library freely assumes by using reflection that the type you provided can be matched by a given field of the database, and hence all the provided terms can be converted into a given class.

On the other hand, I would like that the programming language extracts the database metadata (the schema information) and generates a new type at runtime (reflection) and then assures that all the data operations (term operations) provide some operations as expected at the database level. Then, given that some data manipulation operations, check if the typecast to the given class is possible (subtyping).

Maybe I'm talking sci-fi, but that is something that I require to create a query language which is correct, and such query language requires a programming language in which to express such constraints. Reflection helps when I want to do some magic, but is not always "correct" and it is more "making educated guesses".

Thanks to you all for the papers' suggestions, I'm taking my time to check all the proposed ones.
     Giacomo
________________________________________
Da: Stefan Monnier <monnier at iro.umontreal.ca>
Inviato: martedì 12 dicembre 2017 14:45
A: Giacomo Bergami
Cc: types-list at lists.seas.upenn.edu
Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency

> 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

I'm not completely sure what is your concrete goal (after all,
all cases of reflection I know of are in languages which are already
type-safe, such as Common-Lisp, Java, ...), but I wanted to point out
that you may not need subtyping in your type system, because you can
translate a type-system such as that of Java to a language without
subtyping (e.g. using row-polymorphism).

See for example:

    Precision in Practice: A Type-Preserving Java Compiler.
    Christopher League, Zhong Shao, and Valery Trifonov.  In Proc. 12th
    International Conference on Compiler Construction (CC'03), Warsaw,
    Poland, April 2003.

Where they compile Java to something similar to Fω.
I don't think Chris found the time to cover Java reflection, but from
what I remember of discussions at the time it's not necessarily too hard
to add, especially if you're willing to pay the price of a bit of
runtime tests in there.

Also, since they don't rely on subtyping in their target language, it's
probably easier to add dependent types to it.


        Stefan