[Haskell-cafe] Re: practicality of typeful programming

[Daniil Elovkov]

Hello Oleg

2007/6/28, oleg at pobox.com <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.

Yes, but phantom types seem to only solve rather simple problems.

In HList, every (needed) list function had to be lifted to the type
level. No phantom type will let us work with an HList like an ordinary
list, with ordinary list functions, right?

> > 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.om files.
>  ... <snip>

Well, it is expected to be _hard_. AnimalSchema is a type defined in
the program. I really believe this particular thing is doable.

But how acceptable is the price? It takes a lot of effort. It is
enough non-trivial to be a good subject for a scientific paper. But
how _practical_ is it?