Recent searches
Search options
If your new statically-typed language doesn’t have generics then I don’t want it. Not being able to have CustomMap[K, V] is the same thing as not having String vs Int, just at one level of nesting.
I understand generics make things harder, and even more complicated, but they’re part of making things maintainable. Otherwise, you’re trapping users into writing down some of the things they know about their types but not others, and writing more code to deal with that lack as a result.
If I can’t have generic types, I’d rather go back to dynamic typing everywhere, so that there are fewer weird breaks in the language.
(This is a subtweet, but probably a generalized one.)
…Someone else is going to turn around and say this about dependent types though *glances pointedly at a particular set of friends*
@jrose
I’m totally with you on this. Every form of static verification has •some• horizon past which it either can’t reach at all or becomes too onerous to be worth it, and how far out that horizon reaches is not as important as how ragged its boundary is. You want the domain of a static type system to be something you can reason about cleanly, something that innocent refactorings aren’t constantly wandering across, and static types without generics just ain’t that.
@jrose I think part of the long-term appeal of dependent types is their Golden Hammer promise that this family of tradeoffs doesn’t have to exist, that this horizon can extend to infinity. I’m…skeptical. Good and fascinating things there, but I’m not going to bet in favor of that grandiose promise.
@inthehands @jrose it just makes the boundary extremely fuzzy, where the boundary is primarily defined by how much effort goes into pushing it.
@inthehands @jrose I don’t believe any type system can extend this horizon to infinity. There will exist correct programs that can’t be proved correct within the type system. (Waves hands in the general direction of Gödel and https://perl.plover.com/yak/CHI/)
@ben_lings @jrose You don’t even need to wave your hands as far as Gödel: the theorem that no static type system can be both sound and complete without being uncomputable does the trick.
AIUI (which is not very well), dependent type research makes the case that yes, while this is technically true, it is possible to cover the non-pathological cases we actually want for practical purposes if we just push the envelope of automated theorem provers far enough. That’s the thing I’m skeptical of.
@inthehands @jrose another dimension I think is really nice to get right is: when I do have a program that would work but the static type system isn't big enough to express the argument why, how hard is it to change the program so that it does fit into the set of programs that the static type system understands?
My experience with TypeScript for example is that I am extremely chill about the places where I get false positives because it's rarely hard to rearrange my code to make its soundness visible to the compiler. This is one of the chief aspects in which I think TS is specifically very nice to use.