4 ms·

Lack of static typing is awesome in evolving a system I really don't follow your logic, here. Few things change more frequently while evolving/hacking together

Lack of static typing is awesome in evolving a system I really don't follow your logic, here. Few things change more frequently while evolving/hacking together software than the data structures and types. Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. If anything, it's the evolving/hacking process that's MOST prone to accumulating runtime type errors than any other process.

kazinator 11y ago
> Few things change more frequently while evolving/hacking together software than the data structures and types. I tend to agree; it is often correct. (Though sometimes we have solid data structures and types and are able to evolve things without changing them.) Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun. > Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong. Static programs also have run-time values that can be wrong. A static program that is supposed to calculate 42 might calculate 43, which has the correct type. To discover the cause, someone will have to sit down and think about the code. Code which has never been exercised by a test case (coverage) should still be regarded as garbage, in spite of passing type checking. It is not known to be correct. Type checked is not the same thing as correct. The graph of "type-value" in typical code is rather trivial. Take any moderately complex algorithm, and ignore what its operations are doing; just consider their input and output types. The resulting graph/tree is a lot simpler than what is going on with the values. Type problems are trivial. That is why it's even possible to move them to compile time and have static languages. Think about it: something that runs for hours or days in order to produce a result (and is not even known to terminate) can be entirely type-checked in a millisecond. We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking. Or it could sort them in descending order when the expected order is ascending: some test was reversed and the reverse test type checks because the operator is commutative. You still have to either prove your code if possible and feasible, else test it exhaustively if possible, or else test it imperfectly.
- Peaker 11y ago
  > We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. You can know a whole lot because it type-checked. What exactly you know depends on how you leveraged the type system. For example, if you define a red black tree as is defined here: https://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs#L26-L37 https://github.com/yairchu/red-black-tree/blob/master/RedBla... You know code will never generate trees that break the red/black invariants. The tree is guaranteed to be balanced by the type checking process. > The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking Unless you use a dependently-typed language. Consider this `sort` definition: sort : (in:List n a) -> (out:SortedList n a, IsPermutation in out) "List n a" is a list of length "n" of values of type "a". "SortedList n a" is a sorted list of length "n" of values of type "a". "IsPermutation a b" is a proof that a is a permutation of b (returned from sort). Here's how you can define a type like SortedList: type SortedList n a = exists min. SortedList' min n a data SortedList' min n a where Empty : SortedList' min 0 a Cons : LessOrEq x y -> (x:a) -> SortedList' y n a -> SortedList' x (1+n) a SortedList thus embeds a proof alongside each element that it is less than or equal to the lower-bound of the remaining list (i.e: the next element). Type-checking this guarantees that `sort` does the right thing, modulo resource-use/performance (or termination, depending on your type checker). Resource use (bounding) can also be type-checked, but requires leveraging the type system even more. These guarantees aren't free -- you have to write the types for them, and you have to prove them by instantiating values of these types. But you can opt in or out of each of these guarantees -- leverage the type system as much as you want. With dynamic typing, you just don't have this tool at your disposal at all. No flexibility to guarantee anything. You're forced to opt out completely.
  - AnimalMuppet 11y ago
    Please clarify something for me: Does that "proof" run a run time, or at compile time? If at compile time, how does it do so without running into something like the halting problem?
    - mokus 11y ago

kazinator 11y ago

> Few things change more frequently while evolving/hacking together software than the data structures and types. I tend to agree; it is often correct. (Though sometimes we have solid data structures and types and are able to evolve things without changing them.) Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun. > Changing a type in one place while forgetting to in N other places is an extremely common defect introduction method that is easily caught with static type systems. This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong. Static programs also have run-time values that can be wrong. A static program that is supposed to calculate 42 might calculate 43, which has the correct type. To discover the cause, someone will have to sit down and think about the code. Code which has never been exercised by a test case (coverage) should still be regarded as garbage, in spite of passing type checking. It is not known to be correct. Type checked is not the same thing as correct. The graph of "type-value" in typical code is rather trivial. Take any moderately complex algorithm, and ignore what its operations are doing; just consider their input and output types. The resulting graph/tree is a lot simpler than what is going on with the values. Type problems are trivial. That is why it's even possible to move them to compile time and have static languages. Think about it: something that runs for hours or days in order to produce a result (and is not even known to terminate) can be entirely type-checked in a millisecond. We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking. Or it could sort them in descending order when the expected order is ascending: some test was reversed and the reverse test type checks because the operator is commutative. You still have to either prove your code if possible and feasible, else test it exhaustively if possible, or else test it imperfectly.

Peaker 11y ago
> We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling. You can know a whole lot because it type-checked. What exactly you know depends on how you leveraged the type system. For example, if you define a red black tree as is defined here: https://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs#L26-L37 https://github.com/yairchu/red-black-tree/blob/master/RedBla... You know code will never generate trees that break the red/black invariants. The tree is guaranteed to be balanced by the type checking process. > The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking Unless you use a dependently-typed language. Consider this `sort` definition: sort : (in:List n a) -> (out:SortedList n a, IsPermutation in out) "List n a" is a list of length "n" of values of type "a". "SortedList n a" is a sorted list of length "n" of values of type "a". "IsPermutation a b" is a proof that a is a permutation of b (returned from sort). Here's how you can define a type like SortedList: type SortedList n a = exists min. SortedList' min n a data SortedList' min n a where Empty : SortedList' min 0 a Cons : LessOrEq x y -> (x:a) -> SortedList' y n a -> SortedList' x (1+n) a SortedList thus embeds a proof alongside each element that it is less than or equal to the lower-bound of the remaining list (i.e: the next element). Type-checking this guarantees that `sort` does the right thing, modulo resource-use/performance (or termination, depending on your type checker). Resource use (bounding) can also be type-checked, but requires leveraging the type system even more. These guarantees aren't free -- you have to write the types for them, and you have to prove them by instantiating values of these types. But you can opt in or out of each of these guarantees -- leverage the type system as much as you want. With dynamic typing, you just don't have this tool at your disposal at all. No flexibility to guarantee anything. You're forced to opt out completely.
- AnimalMuppet 11y ago
  Please clarify something for me: Does that "proof" run a run time, or at compile time? If at compile time, how does it do so without running into something like the halting problem?
  - mokus 11y ago