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

[Giacomo Bergami]

 A little clarification on the definition of reflection I have in mind (quoting from Wikipedia, https://en.wikipedia.org/wiki/Reflection_(computer_programming)):

>> Discover and modify source-code constructions (such as code blocks, classes, methods, protocols, etc.) as first-class objects at runtime.

In my case, I'm aware that I cannot change a definition of a type at runtime (it won't be safe at all), but sometimes I'd like to transform it into another type while I perform some data operations (and then, create a new type from a previous one). Some operations (like the ones that can be carried out in Java and in some other frameworks) are directly provided by the user, and the user might just (implicitly) define a type while performing data manipulations. So the notion of subtyping seems to be to partially solve the problem of "generating a different type from the previous one" for the relational model (SQL over Relational Database Management Systems). For the XML model, I sense that something like CDuce may be used (http://www.cduce.org/), but all these approaches strictly depend on the data model of choice (for instance, I'm currently working on graph databases...)

I'm also providing a short reply to the people that previously sent some infos that I managed to check within my (little) spare time from main research (thanks by the way for your continuous suggestions). For all the remaining suggestions I'm just slowly reviewing them (My main research field are [graph] databases, and I have knowledge of type theory from my master degree studies). 


@Sergei Soloviev 
I sense that these solutions are very near to something that I'm looking for, even though they state that there is still some more work to do. In particular, I'm referring to  I \lambda <= conclusions:
> We already have a sound and complete algorithmic system and we **believe** it is decidable, though we do not have the proof **yet**. 
Hope that they'll found a proof soon :)


@Matthieu Sozeau
UR seems to be like a start, but it doesn't have the subtyping notion (correct me if I'm wrong. See above.). 


@Ryan Wisnesky 
I would like that group by operations would be represented (agreed, I could exted your paper work to add grouping functions, but those are not represented for the moment). Moreover, I also have Spivak's book on Category Theory, but there are no insight on nested representations (and hence, no reference on group by operations). That's why I was planning to design an ad-hoc language for data "manipulations".

       Giacomo Bergami


Da: Matthieu Sozeau <matthieu.sozeau at gmail.com>
Inviato: giovedì 14 dicembre 2017 13:34
A: Giacomo Bergami
Cc: Stefan Monnier; types-list at lists.seas.upenn.edu
Oggetto: Re: [TYPES] I: On Dependent types and Subtyping's consistency
  


Hi,

 I might be far off but it sounds close to what A. Chlipala's Ur/web language is doing, and it does have a limited form of dependent types, expressive type-level programming with records and a type-safe interface  to SQL.


  http://www.impredicative.com/ur/


Best,
-- Matthieu


On Tue, Dec 12, 2017 at 5:45 PM Giacomo Bergami <giacomo.bergami2 at unibo.it> wrote:
  [ The Types Forum,  http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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