I can't say I agree. The cognitive load of any static typing discipline is in mentally modelling the dynamic (unspecified-by-typing) residue; the residue-model gets simpler the fancier the types get, but nonlinearly. Balance is load of residue vs. load of the types themselves.
-
-
Replying to @graydon_pub @wycats
To me, the nonlinearity is the key here. Residue is already off the cliff of undecidability, so meaningful chunks are quite hard to take out of it. Whereas simpler type systems impose dramatically-less load than more-complex ones (which themselves often fall off same cliff).
1 reply 0 retweets 2 likes -
Replying to @graydon_pub @wycats
Many users have experienced "my program is simple, but type system is so complex that I can't for the life of me get it to typecheck" which is .. a thing you want to reserve for only the gravest / most-pervasive problems if you want anyone to have the patience to use the thing.
2 replies 1 retweet 11 likes -
Replying to @graydon_pub
Again, of course this is true. But type systems that in practice lean a lot on dynamic casts are playing a shell game with complexity that at least in my experience doesn't result in a type system that is as cognitively as simple as the formal model would imply.
2 replies 0 retweets 0 likes -
Replying to @wycats
This "just moving complexity around" stance is also a koan, to reuse your previous term. There are a couple other huge cliffs in type-system complexity (eg. dependent types) that eliminate a whole lot more "dynamic casts"; why not apply that reasoning there?
2 replies 0 retweets 1 like -
Replying to @graydon_pub @wycats
If you look at the possible dynamic errors in a real ML program, few would be eliminated by dependent types.
2 replies 0 retweets 0 likes -
Could you elaborate w.r.t. what you have in mind? Of course dependent types can in principle be used to encode and prove any property; so I guess you mean something more specific?
2 replies 0 retweets 0 likes -
I think that if we look at possible dynamic errors in an ML program, we'd get a few different cases: 1. Impossible/violates preconditions but type system can't prove it (fixed w/ dep types) 2. Dynamic error in outside world (file not found) 3. Case we don't want to bother with.
4 replies 0 retweets 2 likes -
(W.r.t. 2, you could plausibly characterize this as being a symptom of "the type system stops at the process/OS boundary"; but of course changing that is a whole other can of worms.)
1 reply 0 retweets 0 likes -
Sort of, but also you don't really want to prove that you can only run this program if the file system has a particular configuration -- dynamic errors are the right thing.
2 replies 0 retweets 0 likes
There are probably some of these cases that are reasonable. For example, I really like having AbsolutePath vs RelativePath in my systems but very few standard libraries work this way
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.