first-class-families 0.8.0.1 → 0.8.1.0

raw patch · 19 files changed

+232/−220 lines, 19 filesdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−1
• LICENSE +1/−1
• first-class-families.cabal +9/−5
• src/Fcf.hs +0/−1
• src/Fcf/Class/Bifunctor.hs +10/−6
• src/Fcf/Class/Foldable.hs +44/−41
• src/Fcf/Class/Functor.hs +5/−5
• src/Fcf/Class/Monoid.hs +10/−10
• src/Fcf/Class/Monoid/Types.hs +0/−1
• src/Fcf/Class/Ord.hs +7/−8
• src/Fcf/Combinators.hs +1/−1
• src/Fcf/Core.hs +0/−1
• src/Fcf/Data/Bool.hs +0/−1
• src/Fcf/Data/Common.hs +0/−1
• src/Fcf/Data/Function.hs +9/−10
• src/Fcf/Data/List.hs +130/−124
• src/Fcf/Data/Nat.hs +0/−1
• src/Fcf/Data/Symbol.hs +0/−1
• src/Fcf/Utils.hs +0/−1

@@ -1,3 +1,8 @@+# 0.8.1.0++- Add `(Fcf.Combinators.>>=)`+- Resolve warnings about deprecated `TypeInType`+ # 0.8.0.1  - Bump upper bounds for GHC 9.0@@ -33,7 +38,7 @@  # 0.6.0.0 -- Add `Fcf.Utils.Case` and `(Fcf.Combinators.>>=)` (thanks to TheMatten)+- Add `Fcf.Utils.Case` (thanks to TheMatten) - Deprecate `Fcf.Bool.Guarded` - GHC 8.8 compatibility 

@@ -1,4 +1,4 @@-Copyright Li-yao Xia (c) 2018+Copyright Li-yao Xia (c) 2018-2024  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in

@@ -1,5 +1,5 @@ name:                first-class-families-version:             0.8.0.1+version:             0.8.1.0 synopsis:   First-class type families description:@@ -11,13 +11,16 @@ license-file:        LICENSE author:              Li-yao Xia maintainer:          lysxia@gmail.com-copyright:           2018 Li-yao Xia+copyright:           2018-2024 Li-yao Xia category:            Other build-type:          Simple extra-source-files:  README.md, CHANGELOG.md cabal-version:       >=1.10 tested-with:-  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.1, GHC == 8.10.1, GHC == 9.0.1+  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,+  GHC == 8.8.1, GHC == 8.10.1, GHC == 9.0.1, GHC == 9.2.1,+  GHC == 9.2.8, GHC == 9.4.8, GHC == 9.6.4, GHC == 9.8.2,+  GHC == 9.10.1  library   hs-source-dirs:      src@@ -40,10 +43,11 @@     Fcf.Class.Ord     Fcf.Utils   build-depends:-    -- This upper bound is conservative.-    base >= 4.9 && < 4.16+    base >= 4.9 && < 5   ghc-options:         -Wall   default-language:    Haskell2010+  if impl(ghc < 8.6)+    default-extensions: TypeInType  test-suite fcf-test   type:                exitcode-stdio-1.0

@@ -27,7 +27,6 @@ -- >     DataKinds, -- >     PolyKinds, -- >     TypeFamilies,--- >     TypeInType, -- >     TypeOperators, -- >     UndecidableInstances #-} 

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -21,16 +20,21 @@ import Fcf.Combinators (Pure)  -- $setup+-- >>> :set -XGADTs -- >>> import Fcf.Core (Eval) -- >>> 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'. ----- >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))--- Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)--- = '(3, 3)+-- === __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)) :: (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')  -- (,)@@ -47,7 +51,7 @@ -- === __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)@@ -60,7 +64,7 @@ -- === __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)

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -56,8 +55,12 @@ 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@@ -87,9 +90,9 @@ -- -- ==== __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'.@@ -105,17 +108,17 @@ -- -- ==== __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 @@ -137,13 +140,13 @@ -- -- === __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) @@ -153,13 +156,13 @@ -- -- === __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) @@ -168,13 +171,13 @@ -- -- === __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) @@ -186,13 +189,13 @@ -- -- === __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) @@ -202,7 +205,7 @@ -- === __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)@@ -216,12 +219,12 @@ -- -- > 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)

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -14,7 +13,7 @@ import Fcf.Core (Exp, Eval)  -- $setup--- >>> :set -XUndecidableInstances -XTypeInType+-- >>> :set -XUndecidableInstances -XDataKinds -XPolyKinds -XGADTs -- >>> import Fcf.Core (Eval, Exp) -- >>> import Fcf.Data.Nat -- >>> import qualified GHC.TypeLits as TL@@ -26,11 +25,12 @@ -- -- === __Example__ --+-- >>> 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! Eval (Map (AddMul 2) '[0, 1, 2, 3, 4])--- Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]--- = '[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.

@@ -3,7 +3,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -30,6 +29,7 @@  -- $setup -- >>> import GHC.TypeLits (Nat)+-- >>> import Numeric.Natural (Natural)  -- | Type-level semigroup composition @('Data.Semigroup.<>')@. --@@ -87,17 +87,17 @@ -- -- === __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  -- (,)

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} 

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -38,15 +37,15 @@ -- -- >>> :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  -- (,)@@ -109,7 +108,7 @@ -- -- >>> :kind! Eval ("b" <= "a") -- Eval ("b" <= "a") :: Bool--- = 'False+-- = False data (<=) :: a -> a -> Exp Bool type instance Eval ((<=) a b) = Compare a b ~/= 'GT @@ -119,7 +118,7 @@ -- -- >>> :kind! Eval ("b" >= "a") -- Eval ("b" >= "a") :: Bool--- = 'True+-- = True data (>=) :: a -> a -> Exp Bool type instance Eval ((>=) a b) = Compare a b ~/= 'LT @@ -129,7 +128,7 @@ -- -- >>> :kind! Eval ("a" < "b") -- Eval ("a" < "b") :: Bool--- = 'True+-- = True data (<) :: a -> a -> Exp Bool type instance Eval ((<) a b) = Compare a b ~== 'LT @@ -139,6 +138,6 @@ -- -- >>> :kind! Eval ("b" > "a") -- Eval ("b" > "a") :: Bool--- = 'True+-- = True data (>) :: a -> a -> Exp Bool type instance Eval ((>) a b) = Compare a b ~== 'GT

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -15,6 +14,7 @@   , Pure2   , Pure3   , type (=<<)+  , type (>>=)   , type (<=<)   , LiftM   , LiftM2

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators #-}  -- | The 'Eval' family.

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} 

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators #-}  -- | Common data types: tuples, 'Either', 'Maybe'.

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -28,9 +27,9 @@ -- -- === __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) @@ -38,9 +37,9 @@ -- -- === __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))) @@ -48,8 +47,8 @@ -- -- === __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)))

@@ -2,7 +2,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} @@ -82,20 +81,26 @@ import Fcf.Utils (If, TyEq)  -- $setup--- >>> 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__ ----- >>> :kind! Eval ('[1, 2] ++ '[3, 4])--- Eval ('[1, 2] ++ '[3, 4]) :: [Nat]--- = '[1, 2, 3, 4]+-- >>> 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]) :: [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@@ -133,12 +138,12 @@ -- -- === __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@@ -151,9 +156,9 @@ -- -- === __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]) @@ -168,9 +173,9 @@ -- -- === __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 '[]) @@ -178,9 +183,9 @@ -- -- === __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)@@ -194,9 +199,9 @@ -- -- === __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) @@ -219,14 +224,14 @@ -- >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat)) -- >>> :{ -- type instance Eval (ToThree b) =---   If (Eval (b Fcf.>= 4))---     'Nothing---     ('Just '(b, b TL.+ 1))+--   If (4 TL.<=? b)+--     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]@@ -245,8 +250,8 @@ -- === __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) @@ -255,9 +260,9 @@ -- -- === __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 @@ -270,9 +275,9 @@ -- -- === __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 @@ -285,9 +290,9 @@ -- -- === __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)) =@@ -300,9 +305,9 @@ -- -- === __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)) =@@ -320,17 +325,17 @@ -- -- === __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)) @@ -341,17 +346,17 @@ -- -- === __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) @@ -360,9 +365,9 @@ -- -- === __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)@@ -372,21 +377,21 @@ -- -- === __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 @@ -402,21 +407,21 @@ -- -- === __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))@@ -426,13 +431,13 @@ -- -- === __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) @@ -443,12 +448,12 @@ -- -- === __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)@@ -464,13 +469,13 @@ -- -- === __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)) =@@ -483,9 +488,9 @@ -- -- === __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)) =@@ -499,9 +504,10 @@ -- -- === __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) @@ -517,13 +523,13 @@ -- -- === __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)) =@@ -538,9 +544,9 @@ -- -- === __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 @@ -553,9 +559,9 @@ -- -- === __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 '[]) = '[]

@@ -3,7 +3,6 @@     DataKinds,     PolyKinds,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-} 

@@ -1,7 +1,6 @@ {-# LANGUAGE DataKinds              #-} {-# LANGUAGE PolyKinds              #-} {-# LANGUAGE TypeFamilies           #-}-{-# LANGUAGE TypeInType             #-} {-# LANGUAGE TypeOperators          #-} {-# LANGUAGE UndecidableInstances   #-} {-# OPTIONS_GHC -Wall                       #-}

@@ -5,7 +5,6 @@     PolyKinds,     RankNTypes,     TypeFamilies,-    TypeInType,     TypeOperators,     UndecidableInstances #-}