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
JT
@jntrnr
There may definitely be benefit here, but IME it's a minority that gravitate towards heavy use of macros/templates. You may end up optimising towards a relatively small crowd of developers. Are there non-meta programming examples where DT flourish?
2
1
Graydon Hoare
@graydon_pub
The significant uses I’m aware of all involve the logical reading of the types, deriving and passing ghost proof values to demonstrate system invariants. Which unfortunately quite expands the language design task to proof-assistant engineering, and limits the audience.
2
5
Brendan Zabarauskas
@brendanzab
To me it's something that is a possible future direction, but just having DTs seems more and more an inevitability these days for statically typed languages, if only to keep down the complexity (see the plethora of overlapping GHC extensions).
3
1
Graydon Hoare
@graydon_pub
GHC is a (glorious) research testbed; it’s not clear to me whether more than a handful of those extensions are usefully subsumed by DTs and/or whether mainstream users want them. I mean, I like DTs! Just expecting them to remain niche power tools for quite a while.
1
Graydon Hoare
@graydon_pub
I guess I’m also just worried that people will jam them into existing languages “because they’re cool” and thereby further restrict audience. It’s hard to shed a reputation for being inscrutable. I think budgeting complexity is important for adoption.
1
2