Add Foldable class

TODO.md

@@ -13,7 +13,7 @@
   - I can do `let f : ... = \ a b c => ...`. But it doesn't work for recursion and cases are awkward.
 - [x] Erasure checking happens at compile time and isn't surfaced to editor..
 - [ ] Erasure issue during AoC from case building replacing a non-erased value with erased.
-- [ ] Add Foldable?
+- [x] Add Foldable
 - [ ] Maybe return constraints instead of solving metas during unification
   - We already return non-meta constraints for work on the LHS.
   - We might get into a situation where solving immediately would have gotten us more progress?

src/Data/SortedMap.newt

@@ -220,3 +220,8 @@ foldMap f m ((a,b) :: xs) = case lookupMap a m of
 
 listValues : ∀ k v. SortedMap k v → List v
 listValues sm = map snd $ toList sm
+
+instance ∀ k. Foldable (SortedMap k) where
+  foldr f z m = foldr f z (listValues m)
+  foldl f z m = foldl f z (listValues m)
+

src/Prelude.newt

@@ -476,15 +476,23 @@ pfunc stringToInt : String → Int := `(s) => {
   return rval
 }`
 
--- TODO - add Foldable
+class Foldable (m : U → U) where
+  foldl : ∀ a b. (b → a → b) → b → m a → b
+  foldr : ∀ a b. (a → b → b) → b → m a → b
 
-foldl : ∀ A B. (B → A → B) → B → List A → B
+instance Foldable List where
-foldl f acc Nil = acc
+  foldl f acc Nil = acc
-foldl f acc (x :: xs) = foldl f (f acc x) xs
+  foldl f acc (x :: xs) = foldl f (f acc x) xs
 
-foldr : ∀ a b. (a → b → b) → b → List a → b
+  foldr f b Nil = b
-foldr f b Nil = b
+  foldr f b (x :: xs) = f x (foldr f b xs)
-foldr f b (x :: xs) = f x (foldr f b xs)
+
+instance Foldable SnocList where
+  foldl f acc Lin = acc
+  foldl f acc (xs :< x) = f (foldl f acc xs) x
+
+  foldr f b Lin = b
+  foldr f b (xs :< x) = foldr f (f x b) xs
 
 infixl 9 _∘_
 _∘_ : ∀ A B C. (B → C) → (A → B) → A → C