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, [EMAIL PROTECTED] <[EMAIL PROTECTED]>:
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe