3 ms·
OK, program in a language where an array's size is an immutable part of its type. No casting, no autoconversion, no manual conversion. Now write reusable functi
by cbd1984 11y ago
OK, program in a language where an array's size is an immutable part of its type. No casting, no autoconversion, no manual conversion. Now write reusable functions which operate on arrays.
Remember that a string is a kind of array, and inherits all of the same properties.
- kazinator 11y agoOr how about one in which "upper case letter" is a static type. A string of all upper case characters is statically declared; we don't have to iterate at run-time to check it character-by-character any more, wee! Division by zero is passe; we just define a type that excludes zero, and make the division operator's denominator of that type.
- capitalsigma 11y agoThere is a non-zero integral type in Haskell, I believe.
- possibilistic 11y agoThis feels like a straw man argument against static typing. No statically typed language I use suffers from this because they have great data structures and generics. Languages such as Rust that lean on inference are an absolute joy to program in.
- steveklabnik 11y agoActually, Rust arrays have the size as part of their type, and without type-level-integers, there is a lot of pain around them. :( That said, there's the solution: type level integers. (That also said, Rust's String type isn't an array, because it's mutable, so the size can't be a part of the type)
- chowells 11y agoFortunately, Liquid Haskell already exists. I wouldn't say it's production quality yet... But it's a work in progress, and achieves far more than you are requesting here.
- eru 11y agoYou can also go with Agda for full on dependent typing.
- PeCaN 11y agoOr Idris, which is (IMO) more practically useful than Agda.
- chowells 11y agoThe big advantage to liquid types, a la liquid haskell, is that you get far more inference than you can get in full dependent typing. I still think liquid haskell is too immature (Integer is not a good theory for Int, type classes aren't handled well, etc), but the promise is fascinating if the issues get worked out.
- incepted 11y agoThat's just an argument against languages with broken arrays. I'm guessing you've been doing a lot of Java lately? Even Java has a sane typing system if you stay away from arrays (use ArrayList for crying out loud) but beyond Java, there is a wealth of languages with very good static type systems (Scala, Kotlin, Ceylon).