Study the possibility of using liquid haskell to encode check constraints

[theobat]

At a very theoretical level sql check constraints are refinement types, thus it should be pretty straightforward to translate one system into the other, but I have no idea whether this is a feasible given both liquid haskell and beam idiosyncrasies feature or completely impossible ...

[kmicklas]

I'm not sure that refinement types are applicable to SQL CHECK constraints, as refinement types express a static guarantee about input expressions, while CHECK constraints express a runtime check against actual values. The other issue is that Beam tries to stick to fairly standard Haskell (and doesn't even use Template Haskell for example). However I think it would be totally possible to expose some way to write CHECK constraints using Beam's query combinators as part of your database definition. Someone just needs to work out the API for it! (Note that beam-migrate already has limited support for CHECK constraints but not using the query combinators.)

[theobat]

Wow my original message is quite impenetrable... I must have been tired

Insofar as you can encode check constraints in domain types it's strictly equivalent (c.f. https://www.postgresql.org/docs/current/sql-createdomain.html). But I agree that it's not only check constraints at this stage it's type embedded check constraints. This could be generalized though, because sql table schema are type definitions.

The fact that you can dynamically make queries to change the check behavior, is similar to the fact that you can make queries to change SQL tables schema dynamically, although this library maps haskell (static) types to SQL (dynamic) types so I don't see a contradiction here, it's just an addition on static guarantees (that you can violate at runtime nonetheless, but it's still useful).

But then:

The other issue is that Beam tries to stick to fairly standard Haskell (and doesn't even use Template Haskell for example)

This is totally understandable... And I believe it's part of its strength

Anyway I don't have time to implement this (plus I lack skills), I just dreamt of a full-stack type checking (including refinement types) in a typical client server app ... (I don't think it's good to have check constraints blowing up in your face at run time)

[3noch]

I don't think it's good to have check constraints blowing up in your face at run time

One annoying thing is that, in general, constraints can refer to other parts of the database. So your refinement system would potentially need to first load portions of the database in order to even do the check. Obviously some constraints are simple and can be done without this, but it definitely makes the general problem much harder and refinement types seem less helpful since they can only cover a small set of cases.

[theobat]

One annoying thing is that, in general, constraints can refer to other parts of the database.

Oh interesting I didn't know that, I thought it was restricted to a table, do you happen to have an example ?

So your refinement system would potentially need to first load portions of the database in order to even do the check.

As long as the entire database schema is encoded in haskell this should not be a problem..

[3noch]

Well constraints yes. Check constraints in particular are more restrictive but you can use user-defined functions in your check constraints and those would be difficult to clone in Haskell. You also have intersection with column defaults where you can construct a set of fields that break a check constraint but do not mention the field that causes them to break.

Basically, this is a really complex problem and I'm not sure refinement types is even that good of a fit. To me what feels more natural is possibly a way to compile certain check expressions to SQL and reuse them as some sort of validation function. You can use the type system to track whether or not a particular set of fields has been validated or not. This is effectively poor-man's refinement types but with much less effort.

[theobat]

Ok I'll admit I didn't put much thought into the problem. My idea was that, we should be able to transfer proofs in the way it's feasible between haskell and liquid haskell, but for the entire stack (SQL, html forms etc etc). Every pure validation function is effectively a refined type constructor in my opinion (that also goes for the front end). Nowadays, even in haskell, most proofs of behavior are lost after their computation...

To me what feels more natural is possibly a way to compile certain check expressions to SQL and reuse them as some sort of validation function. You can use the type system to track whether or not a particular set of fields has been validated or not. This is effectively poor-man's refinement types but with much less effort.

My idea here was to completely remove check errors occurrence at the database level and move them at the API level (in case of a typical CRUD app scenario).
I understand using refinement types is out of scope for this library, and I also understand refinement types are complex and cumbersome when some simple validation does the job.