Merge pull request #150 from well-typed/improve-cata-ana

Generalise type signatures of cata- and anamorphisms.

Author: kosmikus

sop-core/CHANGELOG.md

@@ -1,3 +1,9 @@
+# 0.6.0.0
+
+* Generalise the type signatures of cata- and anamorphisms
+  to pass down the constraint dictionaries, as suggested
+  in #144.
+
 # 0.5.0.2 (2022-01-02)
 
 * Compatibility with GHC-9.0 and GHC-9.2.

sop-core/src/Data/SOP/NP.hs

@@ -1,4 +1,6 @@
-{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
 -- | n-ary products (and products of products)
 module Data.SOP.NP
   ( -- * Datatypes
@@ -713,15 +715,14 @@ ctraverse_POP = hctraverse
 --
 cata_NP ::
      forall r f xs .
-     r '[]
-  -> (forall y ys . f y -> r ys -> r (y ': ys))
+     SListI xs
+  => r '[]
+  -> (forall y ys . SListI ys => f y -> r ys -> r (y ': ys))
   -> NP f xs
   -> r xs
-cata_NP nil cons = go
-  where
-    go :: forall ys . NP f ys -> r ys
-    go Nil       = nil
-    go (x :* xs) = cons x (go xs)
+cata_NP nil cons =
+  ccata_NP topP nil cons
+{-# INLINE cata_NP #-}
 
 -- | Constrained catamorphism for 'NP'.
 --
@@ -733,10 +734,11 @@ cata_NP nil cons = go
 -- @since 0.2.3.0
 --
 ccata_NP ::
-     forall c proxy r f xs . (All c xs)
+     forall c proxy r f xs .
+     All c xs
   => proxy c
   -> r '[]
-  -> (forall y ys . c y => f y -> r ys -> r (y ': ys))
+  -> (forall y ys . (c y, All c ys) => f y -> r ys -> r (y ': ys))
   -> NP f xs
   -> r xs
 ccata_NP _ nil cons = go
@@ -759,7 +761,7 @@ ccata_NP _ nil cons = go
 ana_NP ::
      forall s f xs .
      SListI xs
-  => (forall y ys . s (y ': ys) -> (f y, s ys))
+  => (forall y ys . SListI ys => s (y ': ys) -> (f y, s ys))
   -> s xs
   -> NP f xs
 ana_NP uncons =
@@ -775,14 +777,15 @@ ana_NP uncons =
 -- @since 0.2.3.0
 --
 cana_NP ::
-     forall c proxy s f xs . (All c xs)
+     forall c proxy s f xs .
+     All c xs
   => proxy c
-  -> (forall y ys . c y => s (y ': ys) -> (f y, s ys))
+  -> (forall y ys . (c y, All c ys) => s (y ': ys) -> (f y, s ys))
   -> s xs
   -> NP f xs
 cana_NP _ uncons = go sList
   where
-    go :: forall ys . (All c ys) => SList ys -> s ys -> NP f ys
+    go :: forall ys . All c ys => SList ys -> s ys -> NP f ys
     go SNil  _ = Nil
     go SCons s = case uncons s of
       (x, s') -> x :* go sList s'

sop-core/src/Data/SOP/NS.hs

@@ -770,30 +770,29 @@ ctraverse_SOP = hctraverse
 --
 cata_NS ::
      forall r f xs .
-     (forall y ys . f y -> r (y ': ys))
-  -> (forall y ys . r ys -> r (y ': ys))
+     SListI xs
+  => (forall y ys . SListI ys => f y -> r (y ': ys))
+  -> (forall y ys . SListI ys => r ys -> r (y ': ys))
   -> NS f xs
   -> r xs
-cata_NS z s = go
-  where
-    go :: forall ys . NS f ys -> r ys
-    go (Z x) = z x
-    go (S i) = s (go i)
+cata_NS z s =
+  ccata_NS topP z s
 
 -- | Constrained catamorphism for 'NS'.
 --
 -- @since 0.2.3.0
 --
 ccata_NS ::
-     forall c proxy r f xs . (All c xs)
+     forall c proxy r f xs .
+     All c xs
   => proxy c
-  -> (forall y ys . c y => f y -> r (y ': ys))
-  -> (forall y ys . c y => r ys -> r (y ': ys))
+  -> (forall y ys . (c y, All c ys) => f y -> r (y ': ys))
+  -> (forall y ys . (c y, All c ys) => r ys -> r (y ': ys))
   -> NS f xs
   -> r xs
 ccata_NS _ z s = go
   where
-    go :: forall ys . (All c ys) => NS f ys -> r ys
+    go :: forall ys . All c ys => NS f ys -> r ys
     go (Z x) = z x
     go (S i) = s (go i)
 
@@ -802,9 +801,10 @@ ccata_NS _ z s = go
 -- @since 0.2.3.0
 --
 ana_NS ::
-     forall s f xs . (SListI xs)
+     forall s f xs .
+     SListI xs
   => (forall r . s '[] -> r)
-  -> (forall y ys . s (y ': ys) -> Either (f y) (s ys))
+  -> (forall y ys . SListI ys => s (y ': ys) -> Either (f y) (s ys))
   -> s xs
   -> NS f xs
 ana_NS refute decide =
@@ -816,15 +816,15 @@ ana_NS refute decide =
 -- @since 0.2.3.0
 --
 cana_NS :: forall c proxy s f xs .
-     (All c xs)
+     All c xs
   => proxy c
   -> (forall r . s '[] -> r)
-  -> (forall y ys . c y => s (y ': ys) -> Either (f y) (s ys))
+  -> (forall y ys . (c y, All c ys) => s (y ': ys) -> Either (f y) (s ys))
   -> s xs
   -> NS f xs
 cana_NS _ refute decide = go sList
   where
-    go :: forall ys . (All c ys) => SList ys -> s ys -> NS f ys
+    go :: forall ys . All c ys => SList ys -> s ys -> NS f ys
     go SNil  s = refute s
     go SCons s = case decide s of
       Left x   -> Z x