I think lots of the initial value will come in type-directed meta programming. Lots of examples from Haskell and Rust and C++ that seem awkward and hacky are nice and beautiful with DTs.
Conversation
Brendan, can you give an example of how DT helps meta programming, contrasted to Haskell?
1
Haskell has a lot of good extensions already for doing type-directed code generation, like type class induction, type families, generics, and GADTs, type level literals, etc.
1
This allows you to build cool libraries, like Servant, Bound, and database libraries. Unfortunately all those features feel disjointed (due to them being added on later), contributing to a steep learning curve, making it hard for most programmers to use these features themselves.
1
An interesting insight is that many of these facilities can be greatly simplified by moving to dependent types. This allows you to use regular old functions at the type level, instead of having a separate type language with slightly different syntax and semantics.
1
I'm probably not being very precise here, and glossing over a bunch of stuff, but that's the general idea at least. There's been good work being done in bringing DTs to Haskell, and hopefully it will simplify things there. But it's a challenging thing to retrofit.
1
You can see more interesting examples in this paper: cs.ru.nl/~wouters/Publi - also in 's 'Type Driven Development' book. Here's an interesting example of typesafe printf in Idris too: youtube.com/watch?v=fVBck2
1
1
For me I'm super interested in how compile time evaluation can be used in a systems programming language setting. It's super handy to be able to use statically known array lengths for example. And be able to make DSLs that can be evaluated away at compile time.
1
These require some more things beyond pure dependent types (which usually just means types that depend on values), but building off that initial foundation helps greatly.
1
Thanks for your comments. Type level stuff in Haskell has always felt convoluted to me to the point that I often just avoid it. For my own practical DSL work, a Haskell run time error isn't a big deal if it is only a part of another compilation step. Just not very elegant.
1
1
Understandable that the status quo seemed ick. It's slowly getting better in Haskell thankfully - lots of good folks are working on improving it, but it's just not there yet...
E.g. for github.com/zwizwa/asm_too I'm representing signal types as values because code generation depends on bit length a lot. I could not figure out how to do it at the type level. Any tips?
1
Hum not sure. Perhaps way could be to use a GADT for your opcodes, and give them each type signatures? Or have a type family that converts an Opcode into a type - not sure if you can use data constructors at the type level in Haskell yet though 🙄.
1
Show replies