Hi Marko, Ryan Wisnesky, Jan Hidders, and I have been jamming on the Algebraic Property Graphs paper, which formalizes that type system. It's at 17 pages; I hope to have it in a sharable state tomorrow after I add an intro section. Looking forward to your feedback. We have delved into the TP4 virtual machine specifically, as it is in flux until the spec comes out, but Ryan has laid out a strategy for bridging the gap between the type system and programming environments like Java, Python, CQL. I believe the same approach can be used for mm-ADT.
Responses inline. On Sun, May 26, 2019 at 4:34 PM Marko Rodriguez <[email protected]> wrote: > Hi, > > *** This email is primarily for Josh (and Kuppitz). > > I think we need Josh's type system core to mm-ADT. I’m facing the problem > of having to model both a “range” (legal schema) and a “codomain” (current > schema) of the referents of a reference. Let me explain with an example. > > Suppose that there is an SQL table called ‘people’ and the table is empty. > When I mm-ADT serves up a this table, it looks like this in mm-ADT: > > > [db][get,’people’] // *{name:@string, age:@int} > > This says that ‘people’ is a pointer to maps containing a name-key with a > string value and an age-key with an integer value. > > Now lets say I insert some rows into this table. Now, according to the > mm-ADT spec, every reference must have as much information as possible > about the referents. Thus, the people-reference pattern can change. Lets > assume it does and it now is: > > [db][get,’people’] // *{name:@string, age:!gt(20)&!lt(33)} > > We have lost information about the “schema.” This is not good as > compile-time write validation is not possible. > So far, I am thinking: yeah, dealing with schema changes can be tricky. Thus, I want to make a distinction between “range” and “codomain”. Here is > some bytecode: > > [db][define,’person’,{name:@string,age:@int}] > [db][create,’people’,*person] > > I define a type called person, where all such instances must match the > respective map-pattern. I then create a people-key on the db map that maintains a person-reference. > OK. I think by people-key you mean the primary key for the person type, i.e. the vertex id. Correct me if I am wrong. Now: > > [db][add,’people’,{name:marko,age:29}] > [db][add,’people’,{name:josh,age:32}] > ... > [db][get,’people'] // *person{name:@string, age:!gt(20)&!lt(33)} > [db][type,’person'] // {name:@string, age:@int} > > Thus, when I get the reference at people, I see the “codomain” of current > person referents, but when I get the person-type, I get the “range” of > legal person referents. > I see this as a type plus a constraint. And... you won't be surprised to hear me say this... you express it with a select statement: youngishPeople := σ_{age <= 20 ∧ age >= 33}(people) > In this way, “types” become central to mm-ADT, where schema is crucial in > specifying a referent range. > As you know, I would like to see types become central. With types come the possibility of type inference, as well as easier integration with the type systems of other frameworks. Anything which conforms to the simply typed lambda calculus, including extensions to product and coproduct types, will be in the native language of the TP4 VM. > —I have more to say on the necessity of multi-types (union of types) and > their role in pattern definitions. > I think you agree that with both products and coproducts in the type system, we can support functional pattern matching in the style of Haskell or Scala, which is a powerful feature that we just couldn't take advantage of in TP1..3, for lack of a strong type system. Josh > > Thoughts?, > Marko. > > http://rredux.com <http://rredux.com/> > > > > >
