We're not mainstream. We could be in the business of attracting mainstream folk. How do we do that, when we're so weird, and when so many people tell us that we're worthless? Asks a dependently typed functional programmer.
-
-
Replying to @pigworker
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 reply 0 retweets 0 likes -
Replying to @jntrnr @pigworker
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 replies 0 retweets 2 likes -
Replying to @brendanzab @pigworker
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 replies 0 retweets 1 like -
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 replies 0 retweets 5 likes -
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 replies 0 retweets 1 like -
Replying to @brendanzab @graydon_pub and
Hate to be that guy, but I’d put money on no mainstream language having dependent types in the next 20 years.
3 replies 0 retweets 1 like -
Replying to @pcwalton @brendanzab and
Scala already has dependent types. Rust seems likely to have integer-dependent types. And, for a hot take: Typescript has dependent types.
1 reply 0 retweets 1 like -
I may be wrong but these all seem like superficial/circumscribed cases of DT: either (a) pushing type-identity testing to runtime, or else only evaluating identity of types with simple value-dependencies like (b) lexical paths or (c) marked constants that are fully reduced.
2 replies 0 retweets 1 like -
Replying to @graydon_pub @pcwalton and
If
@pcwalton said that full dependent types as in Agda won't be mainstream very soon I'd probably agree. But I think a system where terms can appear in types and where type equality requires reduction is dependently typed. And that's Typescript (and the others).2 replies 0 retweets 1 like
Yeah, I was thinking Agda/Idris style.
-
-
Replying to @pcwalton @graydon_pub and
I think dependent types will appear in mainstream languages in a non-standard form, just like affine types ended up as the rust ownership system and not adding linear function types to C++.
0 replies 0 retweets 0 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.