Mastodon Feed: Post

dysfun@treehouse.systems ("gaytabase") wrote:

there are many ways to put dependent types on SQL queries. the part i've been most interested in recently is type-safe joins and the extra table that pops into scope when you do one.

well i think i've done that bit. from expressions are indexed by a scope of tables which have been mentioned, if you join, you provide a proof that the columns on both table you're joining to are the same type.

i've made a few different choices on this one. most notably, tables are not a normal record type, they're extensible record descriptors. this gives me the flexibility to e.g. synthesise a record for only some of the columns in a table, such as if you select a handful of named columns to reduce the returned data size.

i think you can see the general direction i'm aiming for. i don't know how much of it will end up being practical yet. one thing i think would be very difficult is making sure you can't generate invalid sql. the common cases are easy of course, but once you've started joining, there are aggregation rules you must satisfy for the query to be valid. enforcing those will be hard.