[Haskell-cafe] practicality of typeful programming

[Daniil Elovkov]

Hello folks

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...

The thing is enforcing static constraints turns out to be quite time
consuming, even for 'reasonble' things. The dsl I'm writing will not
primarily be used from Haskell sources, rather more likely be input to
the interpreter, and hence dynamic analysis after parsing will occur
any way. On the other hand, enforcing them excludes some errors...

To give you a flavour, classical example, I could represent
expressions simply by 'data Exp'
or by 'data Exp a' where a is the type of expression and 4 + "str" is illegal,
or by 'data Exp s a' where a is the same and s is an additional
property, like some kind of things the expression mentions, and there
are restrictions on how Exp s1 and Exp s2 can combine. And s is not
otrhogonal with a. There may be more properties.

I'd like to hear your thoughts on how practical it is, and to which
extent, to use typeful programing for statically enforcing
constraints, in real-life applications, where readability and
maintainability matter.