@@ -9,13 +9,17 @@
9 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
9 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
11+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
11+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
12− mapping from `a` to natural numbers. For example, there is an implementation
12+ mapping from `a` to `Nat`. For example, there is an implementation for lists,
13− `Sized (List a)` where `size = length`.
13+ where `size = length`.
15 The function `sizeAccessible` then proves well-foundedness of the relation
15 The function `sizeAccessible` then proves well-foundedness of the relation
16 `Smaller x y = LT (size x) (size y)`, which allows us to use strong
16 `Smaller x y = LT (size x) (size y)`, which allows us to use strong
17 induction conveniently with any type that implements `Sized`.
17 induction conveniently with any type that implements `Sized`.
19+ In practice, this allows us to write functions that recurse not only on
20+ direct subterms of their arguments but on any value
21+ with a (strictly) smaller `size`.
19 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
23 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
21## Tool Updates
25## Tool Updates