3 ms·

> As long as your < operator works That's not true. sort() can be broken in many different ways. For instance sort([3, 7, 5]) -> [1, 2, 3] The result it s

> As long as your < operator works That's not true. sort() can be broken in many different ways. For instance sort([3, 7, 5]) -> [1, 2, 3] The result it sorted and has the correct length, but it's wrong.

lmm 12y ago
The parametricity (edit: thanks imaginenore, I misremembered the name) theorem implies that a generic sort function written in a safe subset of the language could never do that though.
- Robin_Message 12y ago
  Is that the idea that since the code should neither invent new values, nor duplicate values, it will always end up returning a permutation? It seems like inventing values not being possible is fine, but duplicating a value seems very plausible - what safe subset of Java would ensure that doesn't happen?
  - lmm 12y ago
    Maybe http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#linear-checker http://types.cs.washington.edu/checker-framework/current/che... ? (I've used other parts of the checkers framework, but not that one yet)
- imaginenore 12y ago
  The parameterization theorem doesn't imply such thing. http://en.wikipedia.org/wiki/Smn_theorem http://en.wikipedia.org/wiki/Smn_theorem
  - Chinjut 12y ago
    That's different from what is being referred to, which is (very briefly) described at http://en.wikipedia.org/wiki/Parametricity#History http://en.wikipedia.org/wiki/Parametricity#History. Edit: Ah, I didn't realize that there was an edit involved in the post you were referring to. At any rate, things are hopefully now clear to all.
fnord123 12y ago
Terasort handles this by taking a sum of md5sums for each value. The teravalidate program then checks that all the items are in order and that the checksum is the same. It's so unlikely that could generate data that passes teravalidate but not really be correct that it would probably be an important work of computational science in it's own right.

lmm 12y ago

The parametricity (edit: thanks imaginenore, I misremembered the name) theorem implies that a generic sort function written in a safe subset of the language could never do that though.

Robin_Message 12y ago
Is that the idea that since the code should neither invent new values, nor duplicate values, it will always end up returning a permutation? It seems like inventing values not being possible is fine, but duplicating a value seems very plausible - what safe subset of Java would ensure that doesn't happen?
- lmm 12y ago
  Maybe http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#linear-checker http://types.cs.washington.edu/checker-framework/current/che... ? (I've used other parts of the checkers framework, but not that one yet)
imaginenore 12y ago
The parameterization theorem doesn't imply such thing. http://en.wikipedia.org/wiki/Smn_theorem http://en.wikipedia.org/wiki/Smn_theorem
- Chinjut 12y ago
  That's different from what is being referred to, which is (very briefly) described at http://en.wikipedia.org/wiki/Parametricity#History http://en.wikipedia.org/wiki/Parametricity#History. Edit: Ah, I didn't realize that there was an edit involved in the post you were referring to. At any rate, things are hopefully now clear to all.

fnord123 12y ago

Terasort handles this by taking a sum of md5sums for each value. The teravalidate program then checks that all the items are in order and that the checksum is the same. It's so unlikely that could generate data that passes teravalidate but not really be correct that it would probably be an important work of computational science in it's own right.