CategoricalData / CQL

Categorical Query Language IDE
http://categoricaldata.net
299 stars 22 forks source link

java.util.concurrent.ExecutionException: catdata.LocException #33

Closed Skyfold closed 5 years ago

Skyfold commented 5 years ago

I ran into an exception (that I assume should just be an error) when playing around with the "Query" Example code. The error I get is reproduced below:

Error in  Q: java.util.concurrent.ExecutionException: catdata.LocException

The only thing I changed was man to bla in query Q, entity GoodMatch, after foreign_keys, line 38 (foreign_keys for_man -> {bla -> m}). I wanted to know if man had any special significance since it is not an attribute nor a foreign_keys of either schema. The code that causes the error is reproduced below:

(If possible I would like to know what the identifier man refers to and what foreign_keys for_man -> {man -> m} means. I assume it is saying the foreign_keys for_man maps to the selected m of type Man that satisfies the where clause.)

typeside Ty = literal { 
    java_types
        String = "java.lang.String"
        Bool = "java.lang.Boolean"
    java_constants
        String = "return input[0]"
        Bool = "return java.lang.Boolean.parseBoolean(input[0])"
}

schema Source = literal : Ty {
    entities
        Man Woman
    attributes
        fav_book_m : Man -> String
        fav_book_w : Woman -> String
        name_m : Man -> String
        name_w : Woman -> String
        paying : Man -> Bool
} 

schema Target = literal : Ty {
    entities
        Male GoodMatch PayingGoodMatch
    foreign_keys
        is_a : PayingGoodMatch -> GoodMatch
        for_man : GoodMatch -> Male
    attributes
        man_name : Male -> String
        woman_name : GoodMatch -> String
} 

query Q = literal : Source -> Target {
 entity
    GoodMatch -> {
        from m:Man w:Woman
        where fav_book_m(m) = fav_book_w(w)
        attributes woman_name -> name_w(w)
        foreign_keys for_man -> {bla -> m}
    } 

 entity 
    Male -> {
        from man:Man
        attributes man_name -> name_m(man)
    } 

 entity 
    PayingGoodMatch -> {
        from man:Man woman:Woman
        where fav_book_m(man) = fav_book_w(woman)
             paying(man) = true
        foreign_keys is_a -> {m -> man w -> woman}   
    } 

} 

instance I = literal : Source {
    generators
        a d e g : Woman
        b c f h : Man
    multi_equations
        paying -> {b true, c false, f true, h true}
        name_m -> {b bob, c charlie, f frank, h henry}
        name_w -> {a alice, d doris, e ellie, g gina}
        fav_book_m -> {b book1, c book1, f book2, h book3}
        fav_book_w -> {a book1, d book2, e book2, g book4}      
} 

instance J = eval Q I

instance I0 = literal : Source {
    generators
        a0 d0 e0 : Woman
        b0 c0 f0 : Man
    multi_equations
        paying -> {b0 true, c0 false, f0 true}
        name_m -> {b0 bob, c0 charlie, f0 frank}
        name_w -> {a0 alice, d0 doris, e0 ellie}
        fav_book_m -> {b0 book1, c0 book1, f0 book2}
        fav_book_w -> {a0 book1, d0 book2, e0 book2}        
} 

transform h = literal : I0 -> I {
    generators
        a0 -> a d0 -> d e0 -> e b0 -> b c0 -> c f0 -> f
} 

transform k = eval Q h

transform kk = coeval Q k
wisnesky commented 5 years ago

Turns out you found a null pointer dereference in the type inference algorithm. This file now generates the error "Not an entity or type: bla".

In a query Q : S -> T, for each foreign key f : A -> B in T, there must be an assignment from the FOR-bound variables of Q(B) to expressions using the FOR-bound variables of Q(A). In fact, Q(A) and Q(B) are S-instances (you can get them using the "frozen" keyword), and the foreign_keys clauses in Q must define a natural transformation Q(B) -> Q(A) (which you can also get using "frozen"), a tricky and powerful condition checked by the automated theorem prover.

This story repeats at the level of attributes, where each attribute att : A -> t in T must induce the Yoneda embedding y(t) -> Q(A), where y(t) is the "representable instance" associated with t, which consists of a single generator of type t. Fortunately, in practice attributes clauses are much more intuitive than the above description suggests.

The concept of a "frozen instance" recurs in many data models, including the relational model. It's a pretty handy idea often employed by database theorists and dating back to the 70s.