HoSql Type System proof-of-concept

Well, even “nugget”-sized posts proved to be beyond my ability, these days. You see, I’m in a new job, with everything that goes with that. It’s exciting, but super-exhausting, and invigorating, but frustrating, and would have given me zillion things to blog about, had I time to do that. I’m back in the JVM, as you probably understood by my love affair with Scala. But this post is not about that. This post is, actually, a continuation of the one about Higher-Order SQL, triggered by my discovery of Yeti.

Yeti is a strict language of the ML family (syntactically not close to Standard ML, though), with a characteristic that suits me very much: it supports structures in its typesystem, which is of the Hindley-Milner variety. Which means that, some of the work for the “Higher-Order SQL” typesystem has already been done (the unification part — the constraint satisfaction part, I still have to do myself). How does this work? I’ll draw upon Yeti and papers on strongly-typed query languages to try and answer that.

Yeti supports structures, otherwise known as records. Staying informal, a structure type is a collection of labeled types. For example, the type of {bar="3", foo=3}, in Yeti, is {bar is string, foo is number} (that’s actually the way the REPL shows it). If you read how structures behave in Yeti, it will probably remind you of HList in Haskell (at least if you know as little Haskell as I do). BTW, even though Scala is not a functional-first language, its malleability has given opportunities for lots of functional explorations: check out HList in Shapeless by Miles Sabin, a fellow described by Dick Wall as “not being comfortable unless he’s programming with his hair on fire”. Here, I managed to slip a bit of Scala in, again.

We can use structure types to simulate relation types, if we forget, for a moment, that relations are sets of structures. Enclosing everything inside a set wouldn’t add anything to our discussion.

Let’s compile a cookbook of HoSQL expressions together with static types and the Yeti expressions I used to coerce the compiler to perform the needed unifications. Newlines cannot be used in the REPL, nor are they always produced in the output, but I’ll insert some manually to wrap the expressions conveniently.

Projection. In HoSQL, you don’t have to always use projection, like in SQL. But Yeti does not have an empty structure type, so I’ll be jumping past the from x, with x completely unconstrained, expression. It would just result in an unconstrained type. Apart from that, the dot-star shortcut can only be used as a syntactic shortcut for known relations, and is not part of HoSQL. I never intended HoSQL to represent syntactic abstractions.

HoSQL:

select x.a, x.b from x

Type:

{.a is 'a, .b is 'b} -> {a is 'a, b is 'b}

Ignore the dots; dots just mean inferred fields, while their absence means provided ones. In our case, one might interpret the dots as meaning that the input might have other fields, which we care not about, while the output is just what we inferred.

Yeti session:

> do x: {a=x.a, b=x.b} done
<code$> is {.a is 'a, .b is 'b} -> {a is 'a, b is 'b}

Unifying this with an actual relation produces a more specific type. I’m using a structure literal to generate the intended type, here, and this is the equivalent of a first-order term, which can be used to generate SQL (the actual value shown here, of course, is immaterial).

Type:

{a is number, b is string}

Yeti session:

> do x: {a=x.a, b=x.b} done { a=0, b="", c=0 }
{a=0, b=""} is {a is number, b is string}

Selection.

HoSQL:

from x where x.a>3 and length(x.b)>4

Type:

{.a is number, .b is string} -> {a is number, b is string}

Yeti session:

> do x: if x.a==0 and x.b=="" 
> then {a=x.a, b=x.b} else {a=x.a, b=x.b} fi done
<code$> is {.a is number, .b is string} -> {a is number, b is string}

The specific expressions are immaterial, inasmuch as we just care that they constrain the types appropriately.

Union. The good part begins here.

HoSQL:

select x.a, x.b from x
union
select y.a, y.b from y

Type:

{.a is 'a, .b is 'b} -> {.a is 'a, .b is 'b} -> {a is 'a, b is 'b}

Yeti session:

> do x y: if x.a==y.a and x.b==y.b 
> then {a=x.a, b=x.b} else {a=y.a, b=y.b} fi done
<code$> is {.a is 'a, .b is 'b} -> {.a is 'a, .b is 'b}
 -> {a is 'a, b is 'b}

Join. And the good part continues.

HoSQL:

x inner join y on x.a = y.a

Type:

('b is {.a is 'a}) -> {.a is 'a} -> {x is 'b, y is {.a is 'a}}

Yeti session:

> do x y: if x.a==y.a then {x, y} else {x, y} fi done
<code$> is ('b is {.a is 'a}) -> {.a is 'a} -> {x is 'b, y is {.a is 'a}}

Recursive CTE. But the best part is here.

HoSQL:

let t = 
 select x.a, x.b from x
 union
 select t.a+1, t.b-1 from t where t.b>0
t

Type:

{.a is 'a, .b is number} -> {a is 'a, b is number}

Yeti session:

> f x = if x.b==0 then { a=x.a, b=x.b } else f x fi
f is {.a is 'a, .b is number} -> {a is 'a, b is number} = <code$f>

These are the building blocks for most queries (and you can see how the little I left out can work in that point of view). This was just a demonstration of real-life unification of structure types at work. I believe that adding value constraints to the typesystem can build on top of that, without disturbing the waters. Next time, I hope I can return to the “nuggets” and continue the face-off with a demonstration of mixed-site variance in Kotlin.

Advertisements