[Haskell-cafe] Re: practicality of typeful programming

[oleg at pobox.com]

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.