I have recently undertaken a study of all the uses of with in stdlib (there are 650-700 of them, for the sake of a ballpark figure), and discovered some surprising things as a result. Two things (at least) leap out:
- the use of
with on boolean subexpressions, in place of if_then_else_ (there are over 100 of these alone, sometimes but not always in the context of more complex pattern-matching analysis);
- the use of
with to introduce a name for a recursive call on a function, not subsequently analysed by pattern matching.
The purpose of this issue is to draw attention to such uses, and ask whether they should be replaced/refactored away in favour of 'simpler' definitions. The first seems now to be 'idiomatic' Agda: I'm certainly not arguing per se for uses of if_then_else_, but it is striking that we (seem to) have adopted a style self-consciously not like 'ordinary' functional programming, even when that is available.
A specimen example of the second case is given the following, in Data.List.Properties:
splitAt-defn : ∀ n → splitAt {A = A} n ≗ < take n , drop n >
splitAt-defn zero xs = refl
splitAt-defn (suc n) [] = refl
splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
... | (ys , zs) | ih = cong (Prod.map (x ∷_) id) ihwhose final defining clause could, much more straightforwardly, be replaced by
splitAt-defn (suc n) (x ∷ xs) = cong (Prod.map (x ∷_) id) (splitAt-defn n xs)
I have recently undertaken a study of all the uses of
withinstdlib(there are 650-700 of them, for the sake of a ballpark figure), and discovered some surprising things as a result. Two things (at least) leap out:withon boolean subexpressions, in place ofif_then_else_(there are over 100 of these alone, sometimes but not always in the context of more complex pattern-matching analysis);withto introduce a name for a recursive call on a function, not subsequently analysed by pattern matching.The purpose of this issue is to draw attention to such uses, and ask whether they should be replaced/refactored away in favour of 'simpler' definitions. The first seems now to be 'idiomatic' Agda: I'm certainly not arguing per se for uses of
if_then_else_, but it is striking that we (seem to) have adopted a style self-consciously not like 'ordinary' functional programming, even when that is available.A specimen example of the second case is given the following, in
Data.List.Properties:whose final defining clause could, much more straightforwardly, be replaced by
splitAt-defn (suc n) (x ∷ xs) = cong (Prod.map (x ∷_) id) (splitAt-defn n xs)