This gets to the heart of the problem for all type systems supporting deduction. Haskell is slightly better, but at a certain level of abstraction a function type can’t be separated from its implementation. https://brevzin.github.io/c++/2018/10/20/concepts-declarations/ …
-
Show this thread
-
C++ makes you express validity constraints with SFINAE, then write the same expression in the implementation. Haskell has Wadler’s Theorems for Free mechanism. Only functional logic languages really address unification, failure and backtracking rigorously.
2 replies 0 retweets 12 likesShow this thread -
My view after 20 years of floundering on type systems is that type deduction is as hopelessly unscalable as automated theorem proving, and that a language should expose functional logic constructs so programmers can write constraints naturally.
10 replies 5 retweets 35 likesShow this thread -
Replying to @TimSweeneyEpic
Millimeters times millimeters results in millimeters squared, validated at compile time.pic.twitter.com/5bKbAvUqiH
1 reply 0 retweets 0 likes
If you write a lengthy arithmetic function and use the wrong type somewhere along the way, the compiler will whack you.
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.