ReXT

[Richard Samuelson]

Dear Ryan,

I am very interested in the rext command, which you recently incorporated into CQL. Is there a document where you explore its functionality? All I can find is this page

https://www.categoricaldata.net/help/RExt.html

which is limited in scope. For example it does not seem to play well with custom types. For example, the file

options
dont_validate_unsafe = true
require_consistency = false


typeside T = literal {
imports
sql

functions
    isLess : Integer, Integer -> Boolean}


schema S = literal : T {
entities
table

attributes
value : table -> Integer}


query Q = simple : S {
from
t : table

where
isLess(t.value, "1") = true

attributes
value -> t.value}


query R = rext identity S Q

returns the error below. Does this mean that I need to add additional equations to the tyneside T?

Error in query R: java.lang.RuntimeException: Anomaly: not equal: (inr (id0, value) isLess 1) and true

[Ryan Wisnesky]

RExt (Right Kan extensions of queries) is indeed new and undoubtedly has errors; thanks for finding this one! The best place to look is the built-in example called “Rext”, which has a bunch of test cases and examples.

> --
> You received this message because you are subscribed to the Google Groups "Categorical Data" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to categoricalda...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/categoricaldata/51042d8d-6b23-4e13-8418-fa13731c3f2an%40googlegroups.com.

[Richard Samuelson]

The issue, here, seems to be with the built-in sql typeside. If I use my own typeside  T, defined below, then the code runs :).

typeside T = literal {
external_types
    Boolean -> "java.lang.Boolean"
   Integer -> "java.lang.Integer"
 
external_parsers
    Boolean -> "x => java.lang.Boolean.parseBoolean(x)"
   Integer -> "x => java.lang.Integer.parseInt(x)"

external_functions
    isLess : Integer, Integer -> Boolean = "(x, y) => x < y"
}

[Ryan Wisnesky]

Sounds about right, under the hood CQL has to special case all kinds of constructions to interoperate with SQL’s simplistic NULL handling and 3-valued logic. Most likely, the Rext internal code is not aware of these special cases, generating the anomalies.

> To view this discussion on the web visit https://groups.google.com/d/msgid/categoricaldata/e2f8d360-5c7e-4c20-9a9c-5244dfa51f0dn%40googlegroups.com.

[Ryan Wisnesky]

Hi Richard,

I’ve pushed a new version of CQL (cql.jar only, didn’t update cqlAlt.jar) that partially addresses this issue. There was a now-fixed error in the Rext code, but that wasn't the only problem.

The following code works just fine now:

typeside T = literal {
types Integer Boolean
constants "1" : Integer true : Boolean

functions
isLess : Integer, Integer -> Boolean}
schema S = literal : T {
entities
table
attributes
value : table -> Integer}
query Q = simple : S {
from
t : tablewhere
isLess(t.value, "1") = true
attributes
value -> t.value}

query id = identity S

query R = rext identity S Q

As does the above code with the following type side:

typeside T = literal {
imports sql

external_functions
isLess : Integer, Integer -> Boolean = "(x,y)=>java.util.Optional.of(true)"
equations
forall x y . isLess(x,y) = true
}

However, if you omit the equation in T, you still get an anomaly:

Error in query R: java.lang.RuntimeException: Anomaly: not equal: (inr (id0, value) isLess 1) and true

I’m not sure if this is due to an inherent limitation of how CQL’s theorem proving works in a mixed user-defined-function / axiom environment, or if this is a programming error, but I’ll continue to investigate.

Ryan

> On Aug 9, 2024, at 11:15 AM, Richard Samuelson <richard.h...@gmail.com> wrote:
>

> To view this discussion on the web visit https://groups.google.com/d/msgid/categoricaldata/e2f8d360-5c7e-4c20-9a9c-5244dfa51f0dn%40googlegroups.com.

[Ryan Wisnesky]

I’ve pushed a new jar that fixes the anomaly in the (an?) original example too. The underlying issue there was indeed SQL specific, that “true” and “1” were being picked up as function symbols rather than “nullable values” in the SQL typeside for CQL, all of which has to do with SQL’s null handling.