Re:Strong typing, a hill I'm willing to die on
by bluGill on Wednesday October 04, 2023 @11:50AM
(#37766942)
Unit tests and types solve somewhat different problems. You can force a unit test to check everything a type system does with effort (mostly by throwing wrong types at your API and verifying you get an error), but I'm not sure how you would use the type system to enforce sort() actually sorts. Sure sort can take a listOfFoo and return a sortedListOfFoo - but that doesn't verify sortedListOfFoo is actually sorted - and in many cases I want an API that is find with listOfFoo but should handle sortedListOfFoo as well.
[ Parent
| on HN ]
Re:Strong typing, a hill I'm willing to die on
by skulk on Wednesday October 04, 2023 @12:09PM
(#37767241)
With dependent types you can encode any proposition in first-order logic (?). You can indeed define an array type that is necessarily sorted. It won't be pretty but it's possible.
More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...