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
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
Show replies