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.
-
-
I wouldn't have predicted gradual types or linear/region typing being mainstream, either.
-
I’m not sure this forms an argument for dependent types, though. Academia is extremely bad at predicting what is going to be relevant; e.g. substructural typing was basically considered dead until Rust came along.
- 5 more replies
New conversation -
-
-
I’d also put the odds of no other mainstream language having Rust-style lifetimes in the next 20 years at 50%. Static typing moves *very* slowly in practice. It’s not even clear the direction of the trend: Go is an example of a successful backlash against PLT in general.
-
Agreed re Go: I think the most likely next set of mainstream languages will be somewhat anti-types again; even those safety-focused, might be more automata-baed, or immutable-dataflow or such. Taste & patience for type-system adventures seems to be quite cyclical.
- 2 more replies
New conversation -
-
-
Scala already has dependent types. Rust seems likely to have integer-dependent types. And, for a hot take: Typescript has dependent types.
-
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.
- 3 more replies
New conversation -
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.