4 ms·
Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, defin
by garethrowlands 8y ago
Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, define its input to be of type `NonEmptyList`.
Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-basic.html https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...
- pron 8y agoThe power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).