Lysxia/first-class-families
1
1
Fork 0
mirror of https://github.com/Lysxia/first-class-families.git synced 2024-09-11 19:47:12 +03:00
Code Issues Projects Releases Wiki Activity

Update doctests for GHC 9.8

Browse Source
This commit is contained in:
Li-yao Xia 2024-04-02 18:43:27 +02:00
parent 6a160ebb54
commit ea7dad4d39
7 changed files with 207 additions and 196 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Fcf/Class/Bifunctor.hs
View File

@ -25,15 +25,16 @@ import Fcf.Combinators (Pure)
-- >>> import Fcf.Combinators (Flip)
-- >>> import Fcf.Data.Nat (Nat, type (+), type (-))
-- >>> import Fcf.Data.Symbol (Symbol)
-- >>> import Numeric.Natural (Natural)
-- | Type-level 'Data.Bifunctor.bimap'.
--
-- === __Example__
--
-- >>> data Example where Ex :: a -> Example -- Hide the type of examples to avoid brittleness in different GHC versions
-- >>> :kind! 'Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat))
-- 'Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)) :: Example
-- = 'Ex '(3, 3)
-- >>> :kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
-- Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example
-- = Ex '(3, 3)
data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
-- (,)
@ -50,7 +51,7 @@ type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))
-- === __Example__
--
-- >>> :kind! Eval (First ((+) 1) '(3,"a"))
-- Eval (First ((+) 1) '(3,"a")) :: (Nat, Symbol)
-- Eval (First ((+) 1) '(3,"a")) :: (Natural, Symbol)
-- = '(4, "a")
data First :: (a -> Exp b) -> f a c -> Exp (f b c)
type instance Eval (First f x) = Eval (Bimap f Pure x)
@ -63,7 +64,7 @@ type instance Eval (First f x) = Eval (Bimap f Pure x)
-- === __Example__
--
-- >>> :kind! Eval (Second ((+) 1) '("a",3))
-- Eval (Second ((+) 1) '("a",3)) :: (Symbol, Nat)
-- Eval (Second ((+) 1) '("a",3)) :: (Symbol, Natural)
-- = '("a", 4)
data Second :: (c -> Exp d) -> f a c -> Exp (f a d)
type instance Eval (Second g x) = Eval (Bimap Pure g x)

84
src/Fcf/Class/Foldable.hs
View File

@ -55,8 +55,12 @@ import Fcf.Data.Bool (type (&&), type (||))
import Fcf.Data.Nat (Nat, type (+))
-- $setup
-- >>> import Fcf.Combinators (Flip)
-- >>> import Fcf.Core (Eval)
-- >>> import Fcf.Combinators (Flip, Pure)
-- >>> import Fcf.Class.Ord (type (<))
-- >>> import Fcf.Class.Monoid (type (.<>))
-- >>> import Fcf.Data.Nat (type (+))
-- >>> import Numeric.Natural
-- | Type-level 'Data.Foldable.foldMap'.
data FoldMap :: (a -> Exp m) -> t a -> Exp m
@ -86,9 +90,9 @@ type instance Eval (FoldMap f ('Right x)) = Eval (f x)
--
-- ==== __Example__
--
-- >>> :kind! FoldMapDefault_ Pure '[ 'EQ, 'LT, 'GT ]
-- FoldMapDefault_ Pure '[ 'EQ, 'LT, 'GT ] :: Ordering
-- = 'LT
-- >>> :kind! FoldMapDefault_ Pure [EQ, LT, GT]
-- FoldMapDefault_ Pure [EQ, LT, GT] :: Ordering
-- = LT
type FoldMapDefault_ f xs = Eval (Foldr (Bicomap f Pure (.<>)) MEmpty xs)
-- | Default implementation of 'Foldr'.
@ -104,17 +108,17 @@ type FoldMapDefault_ f xs = Eval (Foldr (Bicomap f Pure (.<>)) MEmpty xs)
--
-- ==== __Example__
--
-- >>> :kind! FoldrDefault_ (.<>) 'EQ '[ 'EQ, 'LT, 'GT ]
-- FoldrDefault_ (.<>) 'EQ '[ 'EQ, 'LT, 'GT ] :: Ordering
-- = 'LT
-- >>> :kind! FoldrDefault_ (.<>) EQ [EQ, LT, GT]
-- FoldrDefault_ (.<>) EQ [EQ, LT, GT] :: Ordering
-- = LT
type FoldrDefault_ f y xs = Eval (UnEndo (Eval (FoldMap (Pure1 'Endo <=< Pure1 f) xs)) y)
-- | Right fold.
--
-- === __Example__
--
-- >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
-- Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
-- >>> :kind! Eval (Foldr (+) 0 [1, 2, 3, 4])
-- Eval (Foldr (+) 0 [1, 2, 3, 4]) :: Natural
-- = 10
data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b
@ -136,13 +140,13 @@ type instance Eval (Foldr f y ('Right x)) = Eval (f x y)
--
-- === __Example__
--
-- >>> :kind! Eval (And '[ 'True, 'True])
-- Eval (And '[ 'True, 'True]) :: Bool
-- = 'True
-- >>> :kind! Eval (And [True, True])
-- Eval (And [True, True]) :: Bool
-- = True
--
-- >>> :kind! Eval (And '[ 'True, 'True, 'False])
-- Eval (And '[ 'True, 'True, 'False]) :: Bool
-- = 'False
-- >>> :kind! Eval (And [True, True, False])
-- Eval (And [True, True, False]) :: Bool
-- = False
data And :: t Bool -> Exp Bool
type instance Eval (And lst) = Eval (Foldr (&&) 'True lst)
@ -152,13 +156,13 @@ type instance Eval (And lst) = Eval (Foldr (&&) 'True lst)
--
-- === __Example__
--
-- >>> :kind! Eval (All (Flip (<) 6) '[0,1,2,3,4,5])
-- Eval (All (Flip (<) 6) '[0,1,2,3,4,5]) :: Bool
-- = 'True
-- >>> :kind! Eval (All (Flip (<) 6) [0,1,2,3,4,5])
-- Eval (All (Flip (<) 6) [0,1,2,3,4,5]) :: Bool
-- = True
--
-- >>> :kind! Eval (All (Flip (<) 5) '[0,1,2,3,4,5])
-- Eval (All (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
-- = 'False
-- >>> :kind! Eval (All (Flip (<) 5) [0,1,2,3,4,5])
-- Eval (All (Flip (<) 5) [0,1,2,3,4,5]) :: Bool
-- = False
data All :: (a -> Exp Bool) -> t a -> Exp Bool
type instance Eval (All p lst) = Eval (Foldr (Bicomap p Pure (&&)) 'True lst)
@ -167,13 +171,13 @@ type instance Eval (All p lst) = Eval (Foldr (Bicomap p Pure (&&)) 'True lst)
--
-- === __Example__
--
-- >>> :kind! Eval (Or '[ 'True, 'True])
-- Eval (Or '[ 'True, 'True]) :: Bool
-- = 'True
-- >>> :kind! Eval (Or [True, True])
-- Eval (Or [True, True]) :: Bool
-- = True
--
-- >>> :kind! Eval (Or '[ 'False, 'False])
-- Eval (Or '[ 'False, 'False]) :: Bool
-- = 'False
-- >>> :kind! Eval (Or [False, False])
-- Eval (Or [False, False]) :: Bool
-- = False
data Or :: t Bool -> Exp Bool
type instance Eval (Or lst) = Eval (Foldr (||) 'False lst)
@ -185,13 +189,13 @@ type instance Eval (Or lst) = Eval (Foldr (||) 'False lst)
--
-- === __Example__
--
-- >>> :kind! Eval (Any (Flip (<) 5) '[0,1,2,3,4,5])
-- Eval (Any (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
-- = 'True
-- >>> :kind! Eval (Any (Flip (<) 5) [0,1,2,3,4,5])
-- Eval (Any (Flip (<) 5) [0,1,2,3,4,5]) :: Bool
-- = True
--
-- >>> :kind! Eval (Any (Flip (<) 0) '[0,1,2,3,4,5])
-- Eval (Any (Flip (<) 0) '[0,1,2,3,4,5]) :: Bool
-- = 'False
-- >>> :kind! Eval (Any (Flip (<) 0) [0,1,2,3,4,5])
-- Eval (Any (Flip (<) 0) [0,1,2,3,4,5]) :: Bool
-- = False
data Any :: (a -> Exp Bool) -> t a -> Exp Bool
type instance Eval (Any p lst) = Eval (Foldr (Bicomap p Pure (||)) 'False lst)
@ -201,7 +205,7 @@ type instance Eval (Any p lst) = Eval (Foldr (Bicomap p Pure (||)) 'False lst)
-- === __Example__
--
-- >>> :kind! Eval (Sum '[1,2,3])
-- Eval (Sum '[1,2,3]) :: Nat
-- Eval (Sum '[1,2,3]) :: Natural
-- = 6
data Sum :: t Nat -> Exp Nat
type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)
@ -215,12 +219,12 @@ type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)
--
-- > Concat :: [[a]] -> Exp [a]
--
-- >>> :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))
-- Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]
-- = '[1, 2, 3, 4, 5, 6]
-- >>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))
-- Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]
-- = '[Int, Maybe Int, Maybe String, Either Double Int]
-- >>> :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
-- Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
-- = [1, 2, 3, 4, 5, 6]
-- >>> :kind! Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]]))
-- Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]])) :: [*]
-- = [Int, Maybe Int, Maybe [Char], Either Double Int]
--
data Concat :: t m -> Exp m
type instance Eval (Concat xs) = Eval (FoldMap Pure xs)

6
src/Fcf/Class/Functor.hs
View File

@ -28,9 +28,9 @@ import Fcf.Core (Exp, Eval)
-- >>> data Example where Ex :: a -> Example -- Hide the type of examples to avoid brittleness in different GHC versions
-- >>> data AddMul :: Nat -> Nat -> Exp Nat
-- >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
-- >>> :kind! 'Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
-- 'Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example
-- = 'Ex '[4, 9, 16, 25, 36]
-- >>> :kind! Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
-- Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example
-- = Ex [4, 9, 16, 25, 36]
data Map :: (a -> Exp b) -> f a -> Exp (f b)
-- | Synonym of 'Map' to avoid name clashes.

19
src/Fcf/Class/Monoid.hs
View File

@ -29,6 +29,7 @@ import GHC.TypeLits (AppendSymbol)
-- $setup
-- >>> import GHC.TypeLits (Nat)
-- >>> import Numeric.Natural (Natural)
-- | Type-level semigroup composition @('Data.Semigroup.<>')@.
--
@ -86,17 +87,17 @@ type instance Eval MEmpty_ = MEmpty
--
-- === __Examples__
--
-- >>> :kind! 'LT <> MEmpty
-- 'LT <> MEmpty :: Ordering
-- = 'LT
-- >>> :kind! LT <> MEmpty
-- LT <> MEmpty :: Ordering
-- = LT
--
-- >>> :kind! MEmpty <> '( 'EQ, '[1, 2])
-- MEmpty <> '( 'EQ, '[1, 2]) :: (Ordering, [Nat])
-- = '( 'EQ, '[1, 2])
-- >>> :kind! MEmpty <> '(EQ, [1, 2])
-- MEmpty <> '(EQ, [1, 2]) :: (Ordering, [Natural])
-- = '(EQ, [1, 2])
--
-- >>> :kind! '( 'GT, 'Just '()) <> MEmpty
-- '( 'GT, 'Just '()) <> MEmpty :: (Ordering, Maybe ())
-- = '( 'GT, 'Just '())
-- >>> :kind! '(GT, Just '()) <> MEmpty
-- '(GT, Just '()) <> MEmpty :: (Ordering, Maybe ())
-- = '(GT, Just '())
type family MEmpty :: a
-- (,)

14
src/Fcf/Class/Ord.hs
View File

@ -37,15 +37,15 @@ import Fcf.Utils (TyEq)
--
-- >>> :kind! Eval (Compare "a" "b")
-- Eval (Compare "a" "b") :: Ordering
-- = 'LT
-- = LT
--
-- >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])
-- Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering
-- = 'EQ
-- = EQ
--
-- >>> :kind! Eval (Compare '[1, 3] '[1, 2])
-- Eval (Compare '[1, 3] '[1, 2]) :: Ordering
-- = 'GT
-- = GT
data Compare :: a -> a -> Exp Ordering
-- (,)
@ -108,7 +108,7 @@ type a ~/= b = Eval (Not (a ~== b))
--
-- >>> :kind! Eval ("b" <= "a")
-- Eval ("b" <= "a") :: Bool
-- = 'False
-- = False
data (<=) :: a -> a -> Exp Bool
type instance Eval ((<=) a b) = Compare a b ~/= 'GT
@ -118,7 +118,7 @@ type instance Eval ((<=) a b) = Compare a b ~/= 'GT
--
-- >>> :kind! Eval ("b" >= "a")
-- Eval ("b" >= "a") :: Bool
-- = 'True
-- = True
data (>=) :: a -> a -> Exp Bool
type instance Eval ((>=) a b) = Compare a b ~/= 'LT
@ -128,7 +128,7 @@ type instance Eval ((>=) a b) = Compare a b ~/= 'LT
--
-- >>> :kind! Eval ("a" < "b")
-- Eval ("a" < "b") :: Bool
-- = 'True
-- = True
data (<) :: a -> a -> Exp Bool
type instance Eval ((<) a b) = Compare a b ~== 'LT
@ -138,6 +138,6 @@ type instance Eval ((<) a b) = Compare a b ~== 'LT
--
-- >>> :kind! Eval ("b" > "a")
-- Eval ("b" > "a") :: Bool
-- = 'True
-- = True
data (>) :: a -> a -> Exp Bool
type instance Eval ((>) a b) = Compare a b ~== 'GT

18
src/Fcf/Data/Function.hs
View File

@ -27,9 +27,9 @@ infixl 1 &
--
-- === __Example__
--
-- >>> :kind! Eval ('( 'True, 'Nothing) & Fst)
-- Eval ('( 'True, 'Nothing) & Fst) :: Bool
-- = 'True
-- >>> :kind! Eval ('(True, Nothing) & Fst)
-- Eval ('(True, Nothing) & Fst) :: Bool
-- = True
data (&) :: a -> (a -> Exp b) -> Exp b
type instance Eval (x & f) = Eval (f x)
@ -37,9 +37,9 @@ type instance Eval (x & f) = Eval (f x)
--
-- === __Example__
--
-- >>> :kind! Eval (((&&) `On` Fst) '( 'True, 'Nothing) '( 'False, 'Just '()))
-- Eval (((&&) `On` Fst) '( 'True, 'Nothing) '( 'False, 'Just '())) :: Bool
-- = 'False
-- >>> :kind! Eval (((&&) `On` Fst) '(True, Nothing) '(False, Just '()))
-- Eval (((&&) `On` Fst) '(True, Nothing) '(False, Just '())) :: Bool
-- = False
data On :: (b -> b -> Exp c) -> (a -> Exp b) -> a -> a -> Exp c
type instance Eval (On r f x y) = Eval (r (Eval (f x)) (Eval (f y)))
@ -47,8 +47,8 @@ type instance Eval (On r f x y) = Eval (r (Eval (f x)) (Eval (f y)))
--
-- === __Example__
--
-- >>> :kind! Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True)
-- Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True) :: Bool
-- = 'True
-- >>> :kind! Eval (Bicomap Fst Pure (||) '(False, Nothing) True)
-- Eval (Bicomap Fst Pure (||) '(False, Nothing) True) :: Bool
-- = True
data Bicomap :: (a -> Exp c) -> (b -> Exp d) -> (c -> d -> Exp e) -> a -> b -> Exp e
type instance Eval (Bicomap f g r x y) = Eval (r (Eval (f x)) (Eval (g y)))

251
src/Fcf/Data/List.hs
View File

@ -81,22 +81,26 @@ import Fcf.Data.Nat
import Fcf.Utils (If, TyEq)
-- $setup
-- >>> :set -XGADTs
-- >>> import Fcf.Core (Eval)
-- >>> :set -XGADTs -XUndecidableInstances
-- >>> import Fcf.Core (Exp, Eval)
-- >>> import Fcf.Combinators
-- >>> import Fcf.Class.Foldable (Concat)
-- >>> import Fcf.Class.Monoid ()
-- >>> import Fcf.Data.Nat
-- >>> import Fcf.Utils (If, TyEq)
-- >>> import Data.Type.Ord ()
-- >>> import qualified GHC.TypeLits as TL
-- >>> import GHC.TypeLits (Nat)
-- >>> import Numeric.Natural (Natural)
-- | List catenation.
--
-- === __Example__
--
-- >>> data Example where Ex :: a -> Example -- Hide the type of examples to avoid brittleness in different GHC versions
-- >>> :kind! 'Ex (Eval ('[1, 2] ++ '[3, 4]) :: [Nat])
-- 'Ex (Eval ('[1, 2] ++ '[3, 4]) :: [Nat]) :: Example
-- = 'Ex '[1, 2, 3, 4]
-- >>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
-- Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
-- = Ex [1, 2, 3, 4]
--
data (++) :: [a] -> [a] -> Exp [a]
type instance Eval ((++) xs ys) = xs <> ys
@ -134,12 +138,12 @@ type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
--
-- === __Example__
--
-- >>> :kind! Eval (Cons 1 '[2, 3])
-- Eval (Cons 1 '[2, 3]) :: [Nat]
-- = '[1, 2, 3]
-- >>> :kind! Eval (Cons Int '[Char, Maybe Double])
-- Eval (Cons Int '[Char, Maybe Double]) :: [*]
-- = '[Int, Char, Maybe Double]
-- >>> :kind! Eval (Cons 1 [2, 3])
-- Eval (Cons 1 [2, 3]) :: [Natural]
-- = [1, 2, 3]
-- >>> :kind! Eval (Cons Int [Char, Maybe Double])
-- Eval (Cons Int [Char, Maybe Double]) :: [*]
-- = [Int, Char, Maybe Double]
--
data Cons :: a -> [a] -> Exp [a]
type instance Eval (Cons a as) = a ': as
@ -152,9 +156,9 @@ type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
--
-- === __Example__
--
-- >>> :kind! Eval (Snoc '[1,2,3] 4)
-- Eval (Snoc '[1,2,3] 4) :: [Nat]
-- = '[1, 2, 3, 4]
-- >>> :kind! Eval (Snoc [1,2,3] 4)
-- Eval (Snoc [1,2,3] 4) :: [Natural]
-- = [1, 2, 3, 4]
data Snoc :: [a] -> a -> Exp [a]
type instance Eval (Snoc lst a) = Eval (lst ++ '[a])
@ -169,9 +173,9 @@ type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys))
--
-- === __Example__
--
-- >>> :kind! Eval (Reverse '[1,2,3,4,5])
-- Eval (Reverse '[1,2,3,4,5]) :: [Nat]
-- = '[5, 4, 3, 2, 1]
-- >>> :kind! Eval (Reverse [1,2,3,4,5])
-- Eval (Reverse [1,2,3,4,5]) :: [Natural]
-- = [5, 4, 3, 2, 1]
data Reverse :: [a] -> Exp [a]
type instance Eval (Reverse l) = Eval (Rev l '[])
@ -179,9 +183,9 @@ type instance Eval (Reverse l) = Eval (Rev l '[])
--
-- === __Example__
--
-- >>> :kind! Eval (Intersperse 0 '[1,2,3,4])
-- Eval (Intersperse 0 '[1,2,3,4]) :: [Nat]
-- = '[1, 0, 2, 0, 3, 0, 4]
-- >>> :kind! Eval (Intersperse 0 [1,2,3,4])
-- Eval (Intersperse 0 [1,2,3,4]) :: [Natural]
-- = [1, 0, 2, 0, 3, 0, 4]
data Intersperse :: a -> [a] -> Exp [a]
type instance Eval (Intersperse _ '[] ) = '[]
type instance Eval (Intersperse sep (x ': xs)) = x ': Eval (PrependToAll sep xs)
@ -195,9 +199,9 @@ type instance Eval (PrependToAll sep (x ': xs)) = sep ': x ': Eval (PrependToAll
--
-- === __Example__
--
-- >>> :kind! Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ])
-- Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
-- = '["Lorem", ", ", "ipsum", ", ", "dolor"]
-- >>> :kind! Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ])
-- Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
-- = ["Lorem", ", ", "ipsum", ", ", "dolor"]
data Intercalate :: [a] -> [[a]] -> Exp [a]
type instance Eval (Intercalate xs xss) = Eval (Concat =<< Intersperse xs xss)
@ -221,13 +225,13 @@ type instance Eval (UnfoldrCase _ 'Nothing) = '[]
-- >>> :{
-- type instance Eval (ToThree b) =
-- If (Eval (b Fcf.>= 4))
-- 'Nothing
-- ('Just '(b, b TL.+ 1))
-- Nothing
-- (Just '(b, b TL.+ 1))
-- :}
--
-- >>> :kind! Eval (Unfoldr ToThree 0)
-- Eval (Unfoldr ToThree 0) :: [Nat]
-- = '[0, 1, 2, 3]
-- Eval (Unfoldr ToThree 0) :: [Natural]
-- = [0, 1, 2, 3]
--
-- See also the definition of `Replicate`.
data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]
@ -246,8 +250,8 @@ type instance Eval (NumIter a s) =
-- === __Example__
--
-- >>> :kind! Eval (Replicate 4 '("ok", 2))
-- Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Nat)]
-- = '[ '("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
-- Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Natural)]
-- = ['("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
data Replicate :: Nat -> a -> Exp [a]
type instance Eval (Replicate n a) = Eval (Unfoldr (NumIter a) n)
@ -256,9 +260,9 @@ type instance Eval (Replicate n a) = Eval (Unfoldr (NumIter a) n)
--
-- === __Example__
--
-- >>> :kind! Eval (Take 2 '[1,2,3,4,5])
-- Eval (Take 2 '[1,2,3,4,5]) :: [Nat]
-- = '[1, 2]
-- >>> :kind! Eval (Take 2 [1,2,3,4,5])
-- Eval (Take 2 [1,2,3,4,5]) :: [Natural]
-- = [1, 2]
data Take :: Nat -> [a] -> Exp [a]
type instance Eval (Take n as) = Take_ n as
@ -271,9 +275,9 @@ type family Take_ (n :: Nat) (xs :: [a]) :: [a] where
--
-- === __Example__
--
-- >>> :kind! Eval (Drop 2 '[1,2,3,4,5])
-- Eval (Drop 2 '[1,2,3,4,5]) :: [Nat]
-- = '[3, 4, 5]
-- >>> :kind! Eval (Drop 2 [1,2,3,4,5])
-- Eval (Drop 2 [1,2,3,4,5]) :: [Natural]
-- = [3, 4, 5]
data Drop :: Nat -> [a] -> Exp [a]
type instance Eval (Drop n as) = Drop_ n as
@ -286,9 +290,9 @@ type family Drop_ (n :: Nat) (xs :: [a]) :: [a] where
--
-- === __Example__
--
-- >>> :kind! Eval (TakeWhile ((>=) 3) '[1, 2, 3, 4, 5])
-- Eval (TakeWhile ((>=) 3) '[1, 2, 3, 4, 5]) :: [Nat]
-- = '[1, 2, 3]
-- >>> :kind! Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5])
-- Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
-- = [1, 2, 3]
data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
type instance Eval (TakeWhile p '[]) = '[]
type instance Eval (TakeWhile p (x ': xs)) =
@ -301,9 +305,9 @@ type instance Eval (TakeWhile p (x ': xs)) =
--
-- === __Example__
--
-- :kind! Eval (DropWhile ((>=) 3) '[1, 2, 3, 4, 5])
-- Eval (DropWhile ((>=) 3) '[1, 2, 3, 4, 5]) :: [Nat]
-- = '[4, 5]
-- :kind! Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5])
-- Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
-- = [4, 5]
data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
type instance Eval (DropWhile p '[]) = '[]
type instance Eval (DropWhile p (x ': xs)) =
@ -321,17 +325,17 @@ type instance Eval (DropWhile p (x ': xs)) =
--
-- === __Example__
--
-- >>> :kind! Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4])
-- Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
-- = '( '[1, 2], '[3, 4, 1, 2, 3, 4])
-- >>> :kind! Eval (Span (Flip (<) 3) [1,2,3,4,1,2])
-- Eval (Span (Flip (<) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
-- = '([1, 2], [3, 4, 1, 2])
--
-- >>> :kind! Eval (Span (Flip (<) 9) '[1,2,3])
-- Eval (Span (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
-- = '( '[1, 2, 3], '[])
-- >>> :kind! Eval (Span (Flip (<) 9) [1,2,3])
-- Eval (Span (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
-- = '([1, 2, 3], '[])
--
-- >>> :kind! Eval (Span (Flip (<) 0) '[1,2,3])
-- Eval (Span (Flip (<) 0) '[1,2,3]) :: ([Nat], [Nat])
-- = '( '[], '[1, 2, 3])
-- >>> :kind! Eval (Span (Flip (<) 0) [1,2,3])
-- Eval (Span (Flip (<) 0) [1,2,3]) :: ([Natural], [Natural])
-- = '( '[], [1, 2, 3])
data Span :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
type instance Eval (Span p lst) = '( Eval (TakeWhile p lst), Eval (DropWhile p lst))
@ -342,17 +346,17 @@ type instance Eval (Span p lst) = '( Eval (TakeWhile p lst), Eval (DropWhile p l
--
-- === __Example__
--
-- >>> :kind! Eval (Break (Flip (>) 3) '[1,2,3,4,1,2,3,4])
-- Eval (Break (Flip (>) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
-- = '( '[1, 2, 3], '[4, 1, 2, 3, 4])
-- >>> :kind! Eval (Break (Flip (>) 3) [1,2,3,4,1,2])
-- Eval (Break (Flip (>) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
-- = '([1, 2, 3], [4, 1, 2])
--
-- >>> :kind! Eval (Break (Flip (<) 9) '[1,2,3])
-- Eval (Break (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
-- = '( '[], '[1, 2, 3])
-- >>> :kind! Eval (Break (Flip (<) 9) [1,2,3])
-- Eval (Break (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
-- = '( '[], [1, 2, 3])
--
-- >>> :kind! Eval (Break (Flip (>) 9) '[1,2,3])
-- Eval (Break (Flip (>) 9) '[1,2,3]) :: ([Nat], [Nat])
-- = '( '[1, 2, 3], '[])
-- >>> :kind! Eval (Break (Flip (>) 9) [1,2,3])
-- Eval (Break (Flip (>) 9) [1,2,3]) :: ([Natural], [Natural])
-- = '([1, 2, 3], '[])
data Break :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
type instance Eval (Break p lst) = Eval (Span (Not <=< p) lst)
@ -361,9 +365,9 @@ type instance Eval (Break p lst) = Eval (Span (Not <=< p) lst)
--
-- === __Example__
--
-- >>> :kind! Eval (Tails '[0,1,2,3])
-- Eval (Tails '[0,1,2,3]) :: [[Nat]]
-- = '[ '[0, 1, 2, 3], '[1, 2, 3], '[2, 3], '[3]]
-- >>> :kind! Eval (Tails [0,1,2,3])
-- Eval (Tails [0,1,2,3]) :: [[Natural]]
-- = [[0, 1, 2, 3], [1, 2, 3], [2, 3], '[3]]
data Tails :: [a] -> Exp [[a]]
type instance Eval (Tails '[]) = '[]
type instance Eval (Tails (a ': as)) = (a ': as) ': Eval (Tails as)
@ -373,21 +377,21 @@ type instance Eval (Tails (a ': as)) = (a ': as) ': Eval (Tails as)
--
-- === __Example__
--
-- >>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5])
-- Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5]) :: Bool
-- = 'True
-- >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5])
-- Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5]) :: Bool
-- = True
--
-- >>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5])
-- Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5]) :: Bool
-- = 'False
-- >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5])
-- Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
-- = False
--
-- >>> :kind! Eval (IsPrefixOf '[] '[0,1,3,2,4,5])
-- Eval (IsPrefixOf '[] '[0,1,3,2,4,5]) :: Bool
-- = 'True
-- >>> :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
-- Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
-- = True
--
-- >>> :kind! Eval (IsPrefixOf '[0,1,3,2,4,5] '[])
-- Eval (IsPrefixOf '[0,1,3,2,4,5] '[]) :: Bool
-- = 'False
-- >>> :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
-- Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
-- = False
data IsPrefixOf :: [a] -> [a] -> Exp Bool
type instance Eval (IsPrefixOf xs ys) = IsPrefixOf_ xs ys
@ -403,21 +407,21 @@ type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where
--
-- === __Example__
--
-- >>> :kind! Eval (IsSuffixOf '[3,4,5] '[0,1,2,3,4,5])
-- Eval (IsSuffixOf '[3,4,5] '[0,1,2,3,4,5]) :: Bool
-- = 'True
-- >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5])
-- Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5]) :: Bool
-- = True
--
-- >>> :kind! Eval (IsSuffixOf '[3,4,5] '[0,1,3,2,4,5])
-- Eval (IsSuffixOf '[3,4,5] '[0,1,3,2,4,5]) :: Bool
-- = 'False
-- >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5])
-- Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5]) :: Bool
-- = False
--
-- >>> :kind! Eval (IsSuffixOf '[] '[0,1,3,2,4,5])
-- Eval (IsSuffixOf '[] '[0,1,3,2,4,5]) :: Bool
-- = 'True
-- >>> :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
-- Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
-- = True
--
-- >>> :kind! Eval (IsSuffixOf '[0,1,3,2,4,5] '[])
-- Eval (IsSuffixOf '[0,1,3,2,4,5] '[]) :: Bool
-- = 'False
-- >>> :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
-- Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
-- = False
data IsSuffixOf :: [a] -> [a] -> Exp Bool
type instance Eval (IsSuffixOf xs ys) =
Eval (IsPrefixOf (Reverse @@ xs) (Reverse @@ ys))
@ -427,13 +431,13 @@ type instance Eval (IsSuffixOf xs ys) =
--
-- === __Example__
--
-- >>> :kind! Eval (IsInfixOf '[2,3,4] '[0,1,2,3,4,5,6])
-- Eval (IsInfixOf '[2,3,4] '[0,1,2,3,4,5,6]) :: Bool
-- = 'True
-- >>> :kind! Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6])
-- Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6]) :: Bool
-- = True
--
-- >>> :kind! Eval (IsInfixOf '[2,4,4] '[0,1,2,3,4,5,6])
-- Eval (IsInfixOf '[2,4,4] '[0,1,2,3,4,5,6]) :: Bool
-- = 'False
-- >>> :kind! Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6])
-- Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6]) :: Bool
-- = False
data IsInfixOf :: [a] -> [a] -> Exp Bool
type instance Eval (IsInfixOf xs ys) = Eval (Any (IsPrefixOf xs) =<< Tails ys)
@ -444,12 +448,12 @@ type instance Eval (IsInfixOf xs ys) = Eval (Any (IsPrefixOf xs) =<< Tails ys)
--
-- === __Example__
--
-- >>> :kind! Eval (Elem 1 '[1,2,3])
-- Eval (Elem 1 '[1,2,3]) :: Bool
-- = 'True
-- >>> :kind! Eval (Elem 1 '[2,3])
-- Eval (Elem 1 '[2,3]) :: Bool
-- = 'False
-- >>> :kind! Eval (Elem 1 [1,2,3])
-- Eval (Elem 1 [1,2,3]) :: Bool
-- = True
-- >>> :kind! Eval (Elem 1 [2,3])
-- Eval (Elem 1 [2,3]) :: Bool
-- = False
--
data Elem :: a -> [a] -> Exp Bool
type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)
@ -465,13 +469,13 @@ type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =
--
-- === __Example__
--
-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3])
-- Eval (Find (TyEq 0) '[1,2,3]) :: Maybe Nat
-- = 'Nothing
-- >>> :kind! Eval (Find (TyEq 0) [1,2,3])
-- Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
-- = Nothing
--
-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3,0])
-- Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
-- = 'Just 0
-- >>> :kind! Eval (Find (TyEq 0) [1,2,3,0])
-- Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
-- = Just 0
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
type instance Eval (Find _p '[]) = 'Nothing
type instance Eval (Find p (a ': as)) =
@ -484,9 +488,9 @@ type instance Eval (Find p (a ': as)) =
--
-- === __Example__
--
-- >>> :kind! Eval (Filter ((>) 3) '[1,2,3,0])
-- Eval (Filter ((>) 3) '[1,2,3,0]) :: [Nat]
-- = '[1, 2, 0]
-- >>> :kind! Eval (Filter ((>) 3) [1,2,3,0])
-- Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural]
-- = [1, 2, 0]
data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
type instance Eval (Filter _p '[]) = '[]
type instance Eval (Filter p (a ': as)) =
@ -500,9 +504,10 @@ type instance Eval (Filter p (a ': as)) =
--
-- === __Example__
--
-- >>> :kind! Eval (Partition ((>=) 35) '[ 20, 30, 40, 50])
-- Eval (Partition ((>=) 35) '[ 20, 30, 40, 50]) :: ([Nat], [Nat])
-- = '( '[20, 30], '[40, 50])
-- >>> :kind! Eval (Partition ((>=) 35) [20, 30, 40, 50])
-- Eval (Partition ((>=) 35) [20, 30, 40, 50]) :: ([Natural],
-- [Natural])
-- = '([20, 30], [40, 50])
data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
type instance Eval (Partition p lst) = Eval (Foldr (PartHelp p) '( '[], '[]) lst)
@ -518,13 +523,13 @@ type instance Eval (PartHelp p a '(xs,ys)) =
--
-- === __Example__
--
-- >>> :kind! Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3])
-- Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3]) :: Maybe Nat
-- = 'Just 2
-- >>> :kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
-- Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural
-- = Just 2
--
-- >>> :kind! Eval (FindIndex ((>) 0) '[1,2,3,1,2,3])
-- Eval (FindIndex ((>) 0) '[1,2,3,1,2,3]) :: Maybe Nat
-- = 'Nothing
-- >>> :kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
-- Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural
-- = Nothing
data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
type instance Eval (FindIndex _p '[]) = 'Nothing
type instance Eval (FindIndex p (a ': as)) =
@ -539,9 +544,9 @@ type instance Eval (FindIndex p (a ': as)) =
--
-- === __Example__
--
-- >>> :kind! Eval (SetIndex 2 7 '[1,2,3])
-- Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
-- = '[1, 2, 7]
-- >>> :kind! Eval (SetIndex 2 7 [1,2,3])
-- Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
-- = [1, 2, 7]
data SetIndex :: Nat -> a -> [a] -> Exp [a]
type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
@ -554,9 +559,9 @@ type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
--
-- === __Example__
--
-- >>> :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
-- Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
-- = '[2, 3, 4]
-- >>> :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
-- Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
-- = [2, 3, 4]
data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
type instance Eval (ZipWith _f '[] _bs) = '[]
type instance Eval (ZipWith _f _as '[]) = '[]