Conversation

This Tweet is from a suspended account. Learn more
JT
@jntrnr
Not sure if this rhetorical, but I'd be happy to chat strategy. I suspect your best bet would be to a tool that shows the value of dependent types quickly. What is the biggest benefit in having them, and how does the tool/lang show that. Lots to explore from there.
1
Brendan Zabarauskas
@brendanzab
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.
2
2
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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
Show replies