[Haskell-cafe] Re: practicality of typeful programming

[Daniil Elovkov]

Thank you,
yes, I absolutely didn't question the usefulness of typeful
programming to _some_ degree. What is interesting is where the limits
are. And I have a feeling that they are quite close.

The very idea of how proofs are supplied in typeful Haskell and
dependently typed languages seems to put a serious burden on the
programmer. Epigram authors stated 'pay as you go' (if I remember the
wording right). That's true, but still, (awfully sorry if the
following is rubbish) when I choose to garantee the sortedness of the
list, I introduce quite a bit of stuff to define the appropriate list
type and have to deal with it since then, even if I don't care about
that property in other places. Same with typeful haskell (but not
always, I think).

The fact that structure is mixed with properties seems to put some
limits on both doability and, even more, practilaty of encoding
complex properties.

Oleg, do I remember it right that in your (with Lammel and Schupke)
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.


2007/6/16, oleg at pobox.com <oleg at pobox.com>:
>
> Daniil Elovkov wrote:
> > I've recently asked some questions here about some little type hackery
> > implementing an embedded dsl. But now I wonder if it's worth the
> > effort at all...
>
> Yes it is. Typed embedded DSL are quite useful and widely used. For
> example, Lava (high-level hardware description language) uses phantom
> types to prevent the designer from building meaningless circuits
> (e.g., connecting a Bool and an Int wires).
>         http://citeseer.ist.psu.edu/69503.html
>
> There are other such hardware design languages which profitably use
> types (which ought to be popularized more). Using types can decrease
> the amount of error checking in the implementation.
>
>         I highly recommend the following _very_ good thesis on this
> topic:
>         Morten Rhiger
>         Higher-Order Program Generation
>         http://www.brics.dk/DS/01/4/index.html
>
>