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.
-
-
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
I wouldn't have predicted gradual types or linear/region typing being mainstream, either.
2 replies 0 retweets 0 likes -
Replying to @jntrnr @brendanzab and
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.
3 replies 0 retweets 1 like -
I feel if there’s an opening for dependent types in practice, it’s as a sublanguage that augments a simpler system. Like a more powerful way to jump out of the Rust type system to prove what are now “unsafe” code blocks correct.
1 reply 0 retweets 3 likes -
The key aspect being that most programmers don’t have to interact with the more powerful system—the dependent types are basically private implementation details that never leak out into the public interface.
1 reply 0 retweets 2 likes -
Replying to @pcwalton @brendanzab and
@brendanzab mentioned something similar earlier in this thread. You'd need to hammer out how to be usable, but that seems a promising direction.1 reply 0 retweets 0 likes
It’s mostly an economic problem, IMO. Most software can’t afford to spend developer time/expertise on proving correctness. The software that *can* afford it tends to be core infrastructure, because it’s widely depended on.
-
-
Basically there’s a natural layering of dynamic (e.g. Python/Obj-C), to simple static (e.g. Go/Java), to complex static (e.g. Rust/C++/C) as you go further down the stack. You could even throw in Intel’s mind-bogglingly thorough verification at the very bottom ;)
0 replies 0 retweets 2 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
"The software that *can* afford it tends to be core infrastructure" now if only the converse were true we'd actually be getting somewhere!
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.