agda
A 'better' (less strict) `Data.List.Base.tails`?
Working on #2258 suggests the following:
tails : List A → List (List A)
{- compared to the original
tails [] = [] ∷ []
tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
-}
tails xs = xs ∷ go xs
where
go : List A → List (List A)
go [] = []
go (_ ∷ xs) = xs ∷ go xs
which has the advantage that tails xs observably produces a non-empty list (moreover, one whose head is the argument xs), without having to do a subsidiary pattern-match on xs.
Similar remarks apply to eg inits and scanl, and as with moving scanr to Data.List.NonEmpty, perhaps these functions should, too.
I agree. The beauty of dependently-typed programming is that we can now express this "emergent knowledge" in the types, so that it doesn't have to be rediscovered by later code.
While we can't force people to ditch their Lisp-Scheme-ML-Haskell flavoured FP, at least we can provide them with the tools to do so once they see the light!
