Daniil Elovkov wrote:
The fact that structure is mixed with properties seems to put some limits on both doability and, even more, practilaty of encoding complex properties.
That's why phantom types, attached via a newtype wrapper, are so appealing. If we remove the wrapper, we get the original value to be used in other parts of the program. Adding the wrapper requires either a dynamic test or a special way of constructing a value. Please see the Non-empty list discussion and the example on Haskell Wiki.
in the paper "Strongly typed heterogeneous collections" you say, that the given approach only works for statically specified SQL query, I mean encoded in the Haskell program, not parsed from the untyped input string? (I've just flipped through it, but failed to find this place...) Either in case when data schema is statically known, or, even worse, when it's also dynamic.
Interesting, can all the assertions be proved in that case? Like correspondence between select field types and resultset record types.
Indeed, the assumption of the HList paper is that the query is embedded in a program (entered by the programmer alongside the code) and the database schema is known. This is quite a common use case. There are cases however when the database schema is dynamic and so is the query: that is, the query is received in a string or file, after the (part of the) code has been compiled. Then we need to typecheck that query. The best way of doing this is via Template Haskell. We read the query form the string, make an AST, and then splice it in. The latter operation implicitly invokes the Haskell typechecker. If it is happy, the result can be used as if the query were static to start with. Frederik Eaton used this approach for strongly-typed linear algebra. http://ofb.net/~frederik/stla/ In his system, the type of the matrix includes includes the matrix size and dimensions, so invalid operations like improper matrix multiplication can be rejected statically. And yet, his library permits matrices read from files.