I won’t @ them but limiting expressivity in order to limit cognitive load and keep codebases approachable is a totally legitimate move in language design. I’d even say essential. It’s all about balance, and expressivity _does_ have tradeoffs.https://twitter.com/SeanTAllen/status/1036236006872305665 …
-
-
Replying to @graydon_pub
In the case of generics, the cost of leaving out even simple generics has a high cognitive load cost. I have no problem with taking it slow and conservative; that's a reasonable place for them. But the koans and zealous arguments against generics disrupt the design process.
2 replies 1 retweet 10 likes -
Replying to @wycats
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.
2 replies 0 retweets 17 likes -
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
4. Case that programmer would like to bother with but couldn't figure out how to model. (this emphatically does not always imply that more power is needed, sometimes restrictions help programmers model things)
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.