A nice example of parametricity is that a function signature like fn sort<T: Ord>(slice: &mut [T]) must be a permutation since you can't make new T values (without invoking UB). So a seemingly weak postcondition like is_sorted(slice) is actually a sufficient specification, assuming parametricity. Similarly, even if you're returning a new sequence, e.g. fn sort<T: Ord>(slice: &[T]) -> Vec, you'd only need to add result.len() == slice.len() to the postcondition.
=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social
text/geminiThis content has been proxied by September (ba2dc).