[ new ] null method in Foldable (#832)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>

libs/base/Control/Monad/Either.idr

@@ -112,6 +112,8 @@ Foldable m => Foldable (EitherT e m) where
   foldr f acc (MkEitherT e)
     = foldr (\x,xs => either (const acc) (`f` xs) x) acc e
 
+  null (MkEitherT e) = null e
+
 public export
 Traversable m => Traversable (EitherT e m) where
   traverse f (MkEitherT x)

libs/base/Data/List1.idr

@@ -117,6 +117,7 @@ Monad List1 where
 export
 Foldable List1 where
   foldr c n (x ::: xs) = c x (foldr c n xs)
+  null _ = False
 
 export
 Show a => Show (List1 a) where

libs/base/Data/Vect.idr

@@ -407,6 +407,9 @@ public export
 implementation Foldable (Vect n) where
   foldr f e xs = foldrImpl f e id xs
 
+  null [] = True
+  null _ = False
+
 --------------------------------------------------------------------------------
 -- Special folds
 --------------------------------------------------------------------------------

libs/contrib/Data/SortedMap.idr

@@ -254,11 +254,6 @@ export
 values : SortedMap k v -> List v
 values = map snd . toList
 
-export
-null : SortedMap k v -> Bool
-null Empty = True
-null (M _ _) = False
-
 treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
 treeMap f (Leaf k v) = Leaf k (f v)
 treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@@ -289,6 +284,9 @@ export
 implementation Foldable (SortedMap k) where
   foldr f z = foldr f z . values
 
+  null Empty = True
+  null (M _ _) = False
+
 export
 implementation Traversable (SortedMap k) where
   traverse _ Empty = pure Empty

libs/contrib/Data/SortedSet.idr

@@ -34,6 +34,8 @@ export
 Foldable SortedSet where
   foldr f e xs = foldr f e (Data.SortedSet.toList xs)
 
+  null (SetWrapper m) = null m
+
 ||| Set union. Inserts all elements of x into y
 export
 union : (x, y : SortedSet k) -> SortedSet k
@@ -69,7 +71,3 @@ keySet = SetWrapper . map (const ())
 export
 singleton : Ord k => k -> SortedSet k
 singleton k = insert k empty
-
-export
-null : SortedSet k -> Bool
-null (SetWrapper m) = SortedMap.null m

libs/prelude/Prelude/Interfaces.idr

@@ -217,6 +217,9 @@ interface Foldable (t : Type -> Type) where
   foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
   foldl f z t = foldr (flip (.) . flip f) id t z
 
+  ||| Test whether the structure is empty.
+  null : t elem -> Bool
+
 ||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
 ||| Consequently, the final value is wrapped in the same `Monad`.
 public export

libs/prelude/Prelude/Types.idr

@@ -180,6 +180,8 @@ public export
 Foldable Maybe where
   foldr _ z Nothing  = z
   foldr f z (Just x) = f x z
+  null Nothing = True
+  null (Just _) = False
 
 public export
 Traversable Maybe where
@@ -272,6 +274,8 @@ public export
 Foldable (Either e) where
   foldr f acc (Left _) = acc
   foldr f acc (Right x) = f x acc
+  null (Left _) = True
+  null (Right _) = False
 
 public export
 Traversable (Either e) where
@@ -341,6 +345,9 @@ Foldable List where
   foldl f q [] = q
   foldl f q (x::xs) = foldl f (f q x) xs
 
+  null [] = True
+  null (_::_) = False
+
 public export
 Applicative List where
   pure x = [x]

tests/typedd-book/chapter07/Tree.idr

@@ -19,3 +19,6 @@ Foldable Tree where
   foldr f acc (Node left e right) = let leftfold = foldr f acc left
                                         rightfold = foldr f leftfold right in
                                         f e rightfold
+
+  null Empty = True
+  null _ = False