first-class-families 0.8.1.0 → 0.8.2.0
raw patch · 8 files changed
+1255/−1104 lines, 8 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Fcf: type f @@ x = Eval (f x)
- Fcf.Core: type f @@ x = Eval (f x)
+ Fcf: data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
+ Fcf: data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
+ Fcf: data Break (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
+ Fcf: data Concat (a :: t m) (b :: m)
+ Fcf: data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])
+ Fcf: data Cons (b :: a) (c :: [a]) (d :: [a])
+ Fcf: data Drop (b :: Nat) (c :: [a]) (d :: [a])
+ Fcf: data DropWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
+ Fcf: data Elem (b :: a) (c :: [a]) (d :: Bool)
+ Fcf: data Init (b :: [a]) (c :: Maybe [a])
+ Fcf: data Intercalate (b :: [a]) (c :: [[a]]) (d :: [a])
+ Fcf: data Intersperse (b :: a) (c :: [a]) (d :: [a])
+ Fcf: data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)
+ Fcf: data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)
+ Fcf: data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)
+ Fcf: data Last (b :: [a]) (c :: Maybe a)
+ Fcf: data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
+ Fcf: data Pure4 (f :: a -> b -> c -> d -> e) (g :: a) (h :: b) (i :: c) (j :: d) (k :: e)
+ Fcf: data Pure5 (g :: a -> b -> c -> d -> e -> f) (h :: a) (i :: b) (j :: c) (k :: d) (l :: e) (m :: f)
+ Fcf: data Pure6 (h :: a -> b -> c -> d -> e -> f -> g) (i :: a) (j :: b) (k :: c) (l :: d) (m :: e) (n :: f) (o :: g)
+ Fcf: data Pure7 (i :: a -> b -> c -> d -> e -> f -> g -> h) (j :: a) (k :: b) (l :: c) (m :: d) (n :: e) (o :: f) (p :: g) (q :: h)
+ Fcf: data Pure8 (j :: a -> b -> c -> d -> e -> f -> g -> h -> i) (k :: a) (l :: b) (m :: c) (n :: d) (o :: e) (p :: f) (q :: g) (r :: h) (s :: i)
+ Fcf: data Pure9 (k :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j) (l :: a) (m :: b) (n :: c) (o :: d) (p :: e) (q :: f) (r :: g) (s :: h) (t :: i) (u :: j)
+ Fcf: data Replicate (b :: Nat) (c :: a) (d :: [a])
+ Fcf: data Reverse (b :: [a]) (c :: [a])
+ Fcf: data Singleton (b :: a) (c :: [a])
+ Fcf: data Snoc (b :: [a]) (c :: a) (d :: [a])
+ Fcf: data Span (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
+ Fcf: data SplitAt (b :: Nat) (c :: [a]) (d :: ([a], [a]))
+ Fcf: data Tails (b :: [a]) (c :: [[a]])
+ Fcf: data Take (b :: Nat) (c :: [a]) (d :: [a])
+ Fcf: data TakeWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
+ Fcf: data Uncons (b :: [a]) (c :: Maybe (a, [a]))
+ Fcf: data Unfoldr (c :: b -> Exp Maybe (a, b)) (d :: b) (e :: [a])
+ Fcf: data Unsnoc (b :: [a]) (c :: Maybe ([a], a))
+ Fcf: infixl 1 >>=
+ Fcf.Combinators: data Pure4 (f :: a -> b -> c -> d -> e) (g :: a) (h :: b) (i :: c) (j :: d) (k :: e)
+ Fcf.Combinators: data Pure5 (g :: a -> b -> c -> d -> e -> f) (h :: a) (i :: b) (j :: c) (k :: d) (l :: e) (m :: f)
+ Fcf.Combinators: data Pure6 (h :: a -> b -> c -> d -> e -> f -> g) (i :: a) (j :: b) (k :: c) (l :: d) (m :: e) (n :: f) (o :: g)
+ Fcf.Combinators: data Pure7 (i :: a -> b -> c -> d -> e -> f -> g -> h) (j :: a) (k :: b) (l :: c) (m :: d) (n :: e) (o :: f) (p :: g) (q :: h)
+ Fcf.Combinators: data Pure8 (j :: a -> b -> c -> d -> e -> f -> g -> h -> i) (k :: a) (l :: b) (m :: c) (n :: d) (o :: e) (p :: f) (q :: g) (r :: h) (s :: i)
+ Fcf.Combinators: data Pure9 (k :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j) (l :: a) (m :: b) (n :: c) (o :: d) (p :: e) (q :: f) (r :: g) (s :: h) (t :: i) (u :: j)
+ Fcf.Core: type (f :: k1 -> Exp k) @@ (x :: k1) = Eval f x
+ Fcf.Data.List: data Singleton (b :: a) (c :: [a])
+ Fcf.Data.List: data SplitAt (b :: Nat) (c :: [a]) (d :: ([a], [a]))
+ Fcf.Data.List: data Uncons (b :: [a]) (c :: Maybe (a, [a]))
+ Fcf.Data.List: data Unsnoc (b :: [a]) (c :: Maybe ([a], a))
+ Fcf.Utils: (:$$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
+ Fcf.Utils: (:<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
+ Fcf.Utils: ShowType :: t -> ErrorMessage
+ Fcf.Utils: Text :: Symbol -> ErrorMessage
+ Fcf.Utils: data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
+ Fcf.Utils: data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
+ Fcf.Utils: data ErrorMessage
+ Fcf.Utils: infixl 5 :$$:
+ Fcf.Utils: infixl 6 :<>:
- Fcf: data (>) :: Nat -> Nat -> Exp Bool
+ Fcf: data ( (a :: Nat) > (b :: Nat) ) (c :: Bool)
- Fcf: data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
+ Fcf: data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')
- Fcf: data Case :: [Match j k] -> j -> Exp k
+ Fcf: data Case (a :: [Match j k]) (b :: j) (c :: k)
- Fcf: data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
+ Fcf: data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b]))
- Fcf: data ConstFn :: a -> b -> Exp a
+ Fcf: data ConstFn (c :: a) (d :: b) (e :: a)
- Fcf: data Constraints :: [Constraint] -> Exp Constraint
+ Fcf: data Constraints (a :: [Constraint]) b
- Fcf: data Error :: Symbol -> Exp a
+ Fcf: data Error (b :: Symbol) (c :: a)
- Fcf: data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
+ Fcf: data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
- Fcf: data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
+ Fcf: data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)
- Fcf: data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
+ Fcf: data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat)
- Fcf: data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
+ Fcf: data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c)
- Fcf: data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b
+ Fcf: data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)
- Fcf: data FromMaybe :: k -> Maybe k -> Exp k
+ Fcf: data FromMaybe (a :: k) (b :: Maybe k) (c :: k)
- Fcf: data Fst :: (a, b) -> Exp a
+ Fcf: data Fst (c :: (a, b)) (d :: a)
- Fcf: data Head :: [a] -> Exp (Maybe a)
+ Fcf: data Head (b :: [a]) (c :: Maybe a)
- Fcf: data IsJust :: Maybe a -> Exp Bool
+ Fcf: data IsJust (b :: Maybe a) (c :: Bool)
- Fcf: data IsLeft :: Either a b -> Exp Bool
+ Fcf: data IsLeft (c :: Either a b) (d :: Bool)
- Fcf: data IsNothing :: Maybe a -> Exp Bool
+ Fcf: data IsNothing (b :: Maybe a) (c :: Bool)
- Fcf: data IsRight :: Either a b -> Exp Bool
+ Fcf: data IsRight (c :: Either a b) (d :: Bool)
- Fcf: data Join :: Exp (Exp a) -> Exp a
+ Fcf: data Join (b :: Exp Exp a) (c :: a)
- Fcf: data Length :: [a] -> Exp Nat
+ Fcf: data Length (b :: [a]) (c :: Nat)
- Fcf: data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c
+ Fcf: data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c)
- Fcf: data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d
+ Fcf: data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d)
- Fcf: data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
+ Fcf: data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b)
- Fcf: data Map :: (a -> Exp b) -> f a -> Exp (f b)
+ Fcf: data Map (c :: a -> Exp b) (d :: f a) (e :: f b)
- Fcf: data Not :: Bool -> Exp Bool
+ Fcf: data Not (a :: Bool) (b :: Bool)
- Fcf: data Null :: [a] -> Exp Bool
+ Fcf: data Null (b :: [a]) (c :: Bool)
- Fcf: data Pure :: a -> Exp a
+ Fcf: data Pure (b :: a) (c :: a)
- Fcf: data Pure1 :: (a -> b) -> a -> Exp b
+ Fcf: data Pure1 (c :: a -> b) (d :: a) (e :: b)
- Fcf: data Pure2 :: (a -> b -> c) -> a -> b -> Exp c
+ Fcf: data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c)
- Fcf: data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d
+ Fcf: data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d)
- Fcf: data SetIndex :: Nat -> a -> [a] -> Exp [a]
+ Fcf: data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])
- Fcf: data Snd :: (a, b) -> Exp b
+ Fcf: data Snd (c :: (a, b)) (d :: b)
- Fcf: data Tail :: [a] -> Exp (Maybe [a])
+ Fcf: data Tail (b :: [a]) (c :: Maybe [a])
- Fcf: data TyEq :: a -> b -> Exp Bool
+ Fcf: data TyEq (c :: a) (d :: b) (e :: Bool)
- Fcf: data UnBool :: Exp a -> Exp a -> Bool -> Exp a
+ Fcf: data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a)
- Fcf: data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
+ Fcf: data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c)
- Fcf: data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
+ Fcf: data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b)
- Fcf: data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
+ Fcf: data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b)
- Fcf: data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
+ Fcf: data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c)
- Fcf: data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
+ Fcf: data Unzip (c :: Exp [(a, b)]) (d :: ([a], [b]))
- Fcf: data Zip :: [a] -> [b] -> Exp [(a, b)]
+ Fcf: data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)])
- Fcf: data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
+ Fcf: data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c])
- Fcf: type (-->) = ('Match_ :: j -> k -> Match j k)
+ Fcf: type (-->) = 'Match_ :: j -> k -> Match j k
- Fcf: type Any = ('Any_ :: k -> Match j k)
+ Fcf: type Any = 'Any_ :: k -> Match j k
- Fcf: type Else = ('Else_ :: (j -> Exp k) -> Match j k)
+ Fcf: type Else = 'Else_ :: j -> Exp k -> Match j k
- Fcf: type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)
+ Fcf: type Is = 'Is_ :: j -> Exp Bool -> k -> Match j k
- Fcf: type LiftM = (=<<)
+ Fcf: type LiftM = (=<<) :: a -> Exp b -> Exp a -> b -> Type
- Fcf.Class.Bifunctor: data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
+ Fcf.Class.Bifunctor: data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')
- Fcf.Class.Bifunctor: data First :: (a -> Exp b) -> f a c -> Exp (f b c)
+ Fcf.Class.Bifunctor: data First (d :: a -> Exp b) (e :: f a c) (g :: f b c)
- Fcf.Class.Bifunctor: data Second :: (c -> Exp d) -> f a c -> Exp (f a d)
+ Fcf.Class.Bifunctor: data Second (b :: c -> Exp d) (e :: f a c) (g :: f a d)
- Fcf.Class.Foldable: data All :: (a -> Exp Bool) -> t a -> Exp Bool
+ Fcf.Class.Foldable: data All (b :: a -> Exp Bool) (c :: t a) (d :: Bool)
- Fcf.Class.Foldable: data And :: t Bool -> Exp Bool
+ Fcf.Class.Foldable: data And (a :: t Bool) (b :: Bool)
- Fcf.Class.Foldable: data Any :: (a -> Exp Bool) -> t a -> Exp Bool
+ Fcf.Class.Foldable: data Any (b :: a -> Exp Bool) (c :: t a) (d :: Bool)
- Fcf.Class.Foldable: data Concat :: t m -> Exp m
+ Fcf.Class.Foldable: data Concat (a :: t m) (b :: m)
- Fcf.Class.Foldable: data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]
+ Fcf.Class.Foldable: data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])
- Fcf.Class.Foldable: data FoldMap :: (a -> Exp m) -> t a -> Exp m
+ Fcf.Class.Foldable: data FoldMap (b :: a -> Exp m) (c :: t a) (d :: m)
- Fcf.Class.Foldable: data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b
+ Fcf.Class.Foldable: data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)
- Fcf.Class.Foldable: data Or :: t Bool -> Exp Bool
+ Fcf.Class.Foldable: data Or (a :: t Bool) (b :: Bool)
- Fcf.Class.Foldable: data Sum :: t Nat -> Exp Nat
+ Fcf.Class.Foldable: data Sum (a :: t Nat) (b :: Nat)
- Fcf.Class.Foldable: type FoldMapDefault_ f xs = Eval (Foldr (Bicomap f Pure (.<>)) MEmpty xs)
+ Fcf.Class.Foldable: type FoldMapDefault_ (f :: a -> Exp k) (xs :: t a) = Eval Foldr Bicomap f Pure :: k -> k -> Type (.<>) :: k -> k -> k -> Type MEmpty :: k xs
- Fcf.Class.Foldable: type FoldrDefault_ f y xs = Eval (UnEndo (Eval (FoldMap (Pure1 'Endo <=< Pure1 f) xs)) y)
+ Fcf.Class.Foldable: type FoldrDefault_ (f :: a -> k -> Exp k) (y :: k) (xs :: t a) = Eval UnEndo Eval FoldMap Pure1 'Endo :: k -> Exp k -> Endo k <=< Pure1 f xs y
- Fcf.Class.Functor: data Map :: (a -> Exp b) -> f a -> Exp (f b)
+ Fcf.Class.Functor: data Map (c :: a -> Exp b) (d :: f a) (e :: f b)
- Fcf.Class.Functor: type FMap = Map
+ Fcf.Class.Functor: type FMap = Map :: a -> Exp b -> f a -> f b -> Type
- Fcf.Class.Monoid: data (.<>) :: a -> a -> Exp a
+ Fcf.Class.Monoid: data ( (b :: a) .<> (c :: a) ) (d :: a)
- Fcf.Class.Monoid: data MEmpty_ :: Exp a
+ Fcf.Class.Monoid: data MEmpty_ (b :: a)
- Fcf.Class.Ord: data (>) :: a -> a -> Exp Bool
+ Fcf.Class.Ord: data ( (b :: a) > (c :: a) ) (d :: Bool)
- Fcf.Class.Ord: data Compare :: a -> a -> Exp Ordering
+ Fcf.Class.Ord: data Compare (b :: a) (c :: a) (d :: Ordering)
- Fcf.Class.Ord: data TyEq :: a -> b -> Exp Bool
+ Fcf.Class.Ord: data TyEq (c :: a) (d :: b) (e :: Bool)
- Fcf.Classes: data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
+ Fcf.Classes: data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')
- Fcf.Classes: data Map :: (a -> Exp b) -> f a -> Exp (f b)
+ Fcf.Classes: data Map (c :: a -> Exp b) (d :: f a) (e :: f b)
- Fcf.Combinators: data ($) :: (a -> Exp b) -> a -> Exp b
+ Fcf.Combinators: data ( (c :: a -> Exp b) $ (d :: a) ) (e :: b)
- Fcf.Combinators: data ConstFn :: a -> b -> Exp a
+ Fcf.Combinators: data ConstFn (c :: a) (d :: b) (e :: a)
- Fcf.Combinators: data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
+ Fcf.Combinators: data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c)
- Fcf.Combinators: data Join :: Exp (Exp a) -> Exp a
+ Fcf.Combinators: data Join (b :: Exp Exp a) (c :: a)
- Fcf.Combinators: data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c
+ Fcf.Combinators: data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c)
- Fcf.Combinators: data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d
+ Fcf.Combinators: data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d)
- Fcf.Combinators: data Pure :: a -> Exp a
+ Fcf.Combinators: data Pure (b :: a) (c :: a)
- Fcf.Combinators: data Pure1 :: (a -> b) -> a -> Exp b
+ Fcf.Combinators: data Pure1 (c :: a -> b) (d :: a) (e :: b)
- Fcf.Combinators: data Pure2 :: (a -> b -> c) -> a -> b -> Exp c
+ Fcf.Combinators: data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c)
- Fcf.Combinators: data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d
+ Fcf.Combinators: data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d)
- Fcf.Combinators: type LiftM = (=<<)
+ Fcf.Combinators: type LiftM = (=<<) :: a -> Exp b -> Exp a -> b -> Type
- Fcf.Data.Bool: data (&&) :: Bool -> Bool -> Exp Bool
+ Fcf.Data.Bool: data ( (a :: Bool) && (b :: Bool) ) (c :: Bool)
- Fcf.Data.Bool: data Not :: Bool -> Exp Bool
+ Fcf.Data.Bool: data Not (a :: Bool) (b :: Bool)
- Fcf.Data.Bool: data UnBool :: Exp a -> Exp a -> Bool -> Exp a
+ Fcf.Data.Bool: data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a)
- Fcf.Data.Common: data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
+ Fcf.Data.Common: data ( (a :: b -> Exp c) *** (d :: b' -> Exp c') ) (e :: (b, b')) (f :: (c, c'))
- Fcf.Data.Common: data FromMaybe :: k -> Maybe k -> Exp k
+ Fcf.Data.Common: data FromMaybe (a :: k) (b :: Maybe k) (c :: k)
- Fcf.Data.Common: data Fst :: (a, b) -> Exp a
+ Fcf.Data.Common: data Fst (c :: (a, b)) (d :: a)
- Fcf.Data.Common: data IsJust :: Maybe a -> Exp Bool
+ Fcf.Data.Common: data IsJust (b :: Maybe a) (c :: Bool)
- Fcf.Data.Common: data IsLeft :: Either a b -> Exp Bool
+ Fcf.Data.Common: data IsLeft (c :: Either a b) (d :: Bool)
- Fcf.Data.Common: data IsNothing :: Maybe a -> Exp Bool
+ Fcf.Data.Common: data IsNothing (b :: Maybe a) (c :: Bool)
- Fcf.Data.Common: data IsRight :: Either a b -> Exp Bool
+ Fcf.Data.Common: data IsRight (c :: Either a b) (d :: Bool)
- Fcf.Data.Common: data Snd :: (a, b) -> Exp b
+ Fcf.Data.Common: data Snd (c :: (a, b)) (d :: b)
- Fcf.Data.Common: data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
+ Fcf.Data.Common: data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c)
- Fcf.Data.Common: data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
+ Fcf.Data.Common: data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b)
- Fcf.Data.Common: data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
+ Fcf.Data.Common: data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c)
- Fcf.Data.Function: data (&) :: a -> (a -> Exp b) -> Exp b
+ Fcf.Data.Function: data ( (c :: a) & (d :: a -> Exp b) ) (e :: b)
- Fcf.Data.Function: data Bicomap :: (a -> Exp c) -> (b -> Exp d) -> (c -> d -> Exp e) -> a -> b -> Exp e
+ Fcf.Data.Function: data Bicomap (f :: a -> Exp c) (g :: b -> Exp d) (h :: c -> d -> Exp e) (i :: a) (j :: b) (k :: e)
- Fcf.Data.Function: data On :: (b -> b -> Exp c) -> (a -> Exp b) -> a -> a -> Exp c
+ Fcf.Data.Function: data On (d :: b -> b -> Exp c) (e :: a -> Exp b) (f :: a) (g :: a) (h :: c)
- Fcf.Data.List: data (++) :: [a] -> [a] -> Exp [a]
+ Fcf.Data.List: data ( (b :: [a]) ++ (c :: [a]) ) (d :: [a])
- Fcf.Data.List: data Break :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
+ Fcf.Data.List: data Break (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
- Fcf.Data.List: data Concat :: t m -> Exp m
+ Fcf.Data.List: data Concat (a :: t m) (b :: m)
- Fcf.Data.List: data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]
+ Fcf.Data.List: data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])
- Fcf.Data.List: data Cons :: a -> [a] -> Exp [a]
+ Fcf.Data.List: data Cons (b :: a) (c :: [a]) (d :: [a])
- Fcf.Data.List: data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
+ Fcf.Data.List: data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b]))
- Fcf.Data.List: data Drop :: Nat -> [a] -> Exp [a]
+ Fcf.Data.List: data Drop (b :: Nat) (c :: [a]) (d :: [a])
- Fcf.Data.List: data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
+ Fcf.Data.List: data DropWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
- Fcf.Data.List: data Elem :: a -> [a] -> Exp Bool
+ Fcf.Data.List: data Elem (b :: a) (c :: [a]) (d :: Bool)
- Fcf.Data.List: data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
+ Fcf.Data.List: data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
- Fcf.Data.List: data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
+ Fcf.Data.List: data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)
- Fcf.Data.List: data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
+ Fcf.Data.List: data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat)
- Fcf.Data.List: data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b
+ Fcf.Data.List: data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)
- Fcf.Data.List: data Head :: [a] -> Exp (Maybe a)
+ Fcf.Data.List: data Head (b :: [a]) (c :: Maybe a)
- Fcf.Data.List: data Init :: [a] -> Exp (Maybe [a])
+ Fcf.Data.List: data Init (b :: [a]) (c :: Maybe [a])
- Fcf.Data.List: data Intercalate :: [a] -> [[a]] -> Exp [a]
+ Fcf.Data.List: data Intercalate (b :: [a]) (c :: [[a]]) (d :: [a])
- Fcf.Data.List: data Intersperse :: a -> [a] -> Exp [a]
+ Fcf.Data.List: data Intersperse (b :: a) (c :: [a]) (d :: [a])
- Fcf.Data.List: data IsInfixOf :: [a] -> [a] -> Exp Bool
+ Fcf.Data.List: data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)
- Fcf.Data.List: data IsPrefixOf :: [a] -> [a] -> Exp Bool
+ Fcf.Data.List: data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)
- Fcf.Data.List: data IsSuffixOf :: [a] -> [a] -> Exp Bool
+ Fcf.Data.List: data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)
- Fcf.Data.List: data Last :: [a] -> Exp (Maybe a)
+ Fcf.Data.List: data Last (b :: [a]) (c :: Maybe a)
- Fcf.Data.List: data Length :: [a] -> Exp Nat
+ Fcf.Data.List: data Length (b :: [a]) (c :: Nat)
- Fcf.Data.List: data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
+ Fcf.Data.List: data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b)
- Fcf.Data.List: data Null :: [a] -> Exp Bool
+ Fcf.Data.List: data Null (b :: [a]) (c :: Bool)
- Fcf.Data.List: data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
+ Fcf.Data.List: data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
- Fcf.Data.List: data Replicate :: Nat -> a -> Exp [a]
+ Fcf.Data.List: data Replicate (b :: Nat) (c :: a) (d :: [a])
- Fcf.Data.List: data Reverse :: [a] -> Exp [a]
+ Fcf.Data.List: data Reverse (b :: [a]) (c :: [a])
- Fcf.Data.List: data SetIndex :: Nat -> a -> [a] -> Exp [a]
+ Fcf.Data.List: data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])
- Fcf.Data.List: data Snoc :: [a] -> a -> Exp [a]
+ Fcf.Data.List: data Snoc (b :: [a]) (c :: a) (d :: [a])
- Fcf.Data.List: data Span :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
+ Fcf.Data.List: data Span (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))
- Fcf.Data.List: data Tail :: [a] -> Exp (Maybe [a])
+ Fcf.Data.List: data Tail (b :: [a]) (c :: Maybe [a])
- Fcf.Data.List: data Tails :: [a] -> Exp [[a]]
+ Fcf.Data.List: data Tails (b :: [a]) (c :: [[a]])
- Fcf.Data.List: data Take :: Nat -> [a] -> Exp [a]
+ Fcf.Data.List: data Take (b :: Nat) (c :: [a]) (d :: [a])
- Fcf.Data.List: data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
+ Fcf.Data.List: data TakeWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])
- Fcf.Data.List: data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
+ Fcf.Data.List: data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b)
- Fcf.Data.List: data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]
+ Fcf.Data.List: data Unfoldr (c :: b -> Exp Maybe (a, b)) (d :: b) (e :: [a])
- Fcf.Data.List: data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
+ Fcf.Data.List: data Unzip (c :: Exp [(a, b)]) (d :: ([a], [b]))
- Fcf.Data.List: data Zip :: [a] -> [b] -> Exp [(a, b)]
+ Fcf.Data.List: data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)])
- Fcf.Data.List: data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
+ Fcf.Data.List: data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c])
- Fcf.Data.Nat: data (>) :: Nat -> Nat -> Exp Bool
+ Fcf.Data.Nat: data ( (a :: Nat) > (b :: Nat) ) (c :: Bool)
- Fcf.Data.Symbol: data () => Symbol
+ Fcf.Data.Symbol: data Symbol
- Fcf.Utils: data Case :: [Match j k] -> j -> Exp k
+ Fcf.Utils: data Case (a :: [Match j k]) (b :: j) (c :: k)
- Fcf.Utils: data Constraints :: [Constraint] -> Exp Constraint
+ Fcf.Utils: data Constraints (a :: [Constraint]) b
- Fcf.Utils: data Error :: Symbol -> Exp a
+ Fcf.Utils: data Error (b :: Symbol) (c :: a)
- Fcf.Utils: data TError :: ErrorMessage -> Exp a
+ Fcf.Utils: data TError (b :: ErrorMessage) (c :: a)
- Fcf.Utils: data TyEq :: a -> b -> Exp Bool
+ Fcf.Utils: data TyEq (c :: a) (d :: b) (e :: Bool)
- Fcf.Utils: type (-->) = ('Match_ :: j -> k -> Match j k)
+ Fcf.Utils: type (-->) = 'Match_ :: j -> k -> Match j k
- Fcf.Utils: type Any = ('Any_ :: k -> Match j k)
+ Fcf.Utils: type Any = 'Any_ :: k -> Match j k
- Fcf.Utils: type Else = ('Else_ :: (j -> Exp k) -> Match j k)
+ Fcf.Utils: type Else = 'Else_ :: j -> Exp k -> Match j k
- Fcf.Utils: type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)
+ Fcf.Utils: type Is = 'Is_ :: j -> Exp Bool -> k -> Match j k
- Fcf.Utils: type family If (cond :: Bool) (tru :: k) (fls :: k) :: k
+ Fcf.Utils: type family TypeError (a :: ErrorMessage) :: b
Files
- CHANGELOG.md +84/−79
- LICENSE +1/−1
- first-class-families.cabal +63/−63
- src/Fcf.hs +186/−150
- src/Fcf/Combinators.hs +24/−0
- src/Fcf/Data/List.hs +621/−575
- src/Fcf/Utils.hs +170/−136
- test/test.hs +106/−100
CHANGELOG.md view
@@ -1,79 +1,84 @@-# 0.8.1.0--- Add `(Fcf.Combinators.>>=)`-- Resolve warnings about deprecated `TypeInType`--# 0.8.0.1--- Bump upper bounds for GHC 9.0-- Update doctests for cabal-docspec--# 0.8.0.0--- Add modules- + `Fcf.Data.Symbol` (currently just reexports `Symbol`) (thanks to gspia)- + `Fcf.Data.Function`- + "Overloaded type families" ("type-level type classes")- * `Fcf.Class.Ord`- * `Fcf.Class.Monoid`- * `Fcf.Class.Monoid.Types` (which exports just an `Endo a` to wrap `a -> Exp a`)- * `Fcf.Class.Functor`- * `Fcf.Class.Bifunctor`- * `Fcf.Class.Foldable`--- Add functions in `Fcf.Data.List`:- `Intersperse`, `Intercalate`, `Span`, `Break`, `Tails`, `IsPrefixOf`,- `IsSuffixOf`, `IsInfixOf`, `Partition`.-- Generalize `Foldr`, `Concat` and `ConcatMap` to foldable types.--- Remove deprecated `Guarded`, `Guard((:=))`, `Otherwise`.-- Deprecate `Fcf.Classes`--# 0.7.0.0--- Add `Unfoldr`, `Concat`, `ConcatMap`, `Replicate`, `Take`, `Drop`,- `TakeWhile`, `DropWhile`, `Reverse` to `Data.List`. (thanks to gspia)-- Change `Elem`, `Lookup`, `Zip` to be `data` instead of `type` synonyms.-- Fix performance of `Filter` and `Find`.--# 0.6.0.0--- Add `Fcf.Utils.Case` (thanks to TheMatten)-- Deprecate `Fcf.Bool.Guarded`-- GHC 8.8 compatibility--# 0.5.0.0--- Modularized library--- `Fcf.Utils`:-- + Add `TError`- + Rename `Collapse` to `Constraints`--- `Fcf.Data.List`: Added `Cons`, `Last`, `Init`, `Elem`--# 0.4.0.0--- New functions (thanks to blmage)-- + `LiftM`, `LiftM2`, `LiftM3`- + `(<=)`, `(>=)`, `(<)`, `(>)`- + `Guarded`, `Guard((:=))`, `Otherwise`--# 0.3.0.1--- GHC 8.6 compatibility--# 0.3.0.0--- More new functions, (thanks to isovector)--# 0.2.0.0--- A whole bunch of basic functions (thanks to isovector)-- Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`)--# 0.1.0.0--Initial version+# 0.8.2.0 - 2025-10-12 + +- Add `Fcf.Utils.Assert` and `Fcf.Utils.AssertNot`. +- Export everything in `Fcf` + +# 0.8.1.0 + +- Add `(Fcf.Combinators.>>=)` +- Resolve warnings about deprecated `TypeInType` + +# 0.8.0.1 + +- Bump upper bounds for GHC 9.0 +- Update doctests for cabal-docspec + +# 0.8.0.0 + +- Add modules + + `Fcf.Data.Symbol` (currently just reexports `Symbol`) (thanks to gspia) + + `Fcf.Data.Function` + + "Overloaded type families" ("type-level type classes") + * `Fcf.Class.Ord` + * `Fcf.Class.Monoid` + * `Fcf.Class.Monoid.Types` (which exports just an `Endo a` to wrap `a -> Exp a`) + * `Fcf.Class.Functor` + * `Fcf.Class.Bifunctor` + * `Fcf.Class.Foldable` + +- Add functions in `Fcf.Data.List`: + `Intersperse`, `Intercalate`, `Span`, `Break`, `Tails`, `IsPrefixOf`, + `IsSuffixOf`, `IsInfixOf`, `Partition`. +- Generalize `Foldr`, `Concat` and `ConcatMap` to foldable types. + +- Remove deprecated `Guarded`, `Guard((:=))`, `Otherwise`. +- Deprecate `Fcf.Classes` + +# 0.7.0.0 + +- Add `Unfoldr`, `Concat`, `ConcatMap`, `Replicate`, `Take`, `Drop`, + `TakeWhile`, `DropWhile`, `Reverse` to `Data.List`. (thanks to gspia) +- Change `Elem`, `Lookup`, `Zip` to be `data` instead of `type` synonyms. +- Fix performance of `Filter` and `Find`. + +# 0.6.0.0 + +- Add `Fcf.Utils.Case` (thanks to TheMatten) +- Deprecate `Fcf.Bool.Guarded` +- GHC 8.8 compatibility + +# 0.5.0.0 + +- Modularized library + +- `Fcf.Utils`: + + + Add `TError` + + Rename `Collapse` to `Constraints` + +- `Fcf.Data.List`: Added `Cons`, `Last`, `Init`, `Elem` + +# 0.4.0.0 + +- New functions (thanks to blmage) + + + `LiftM`, `LiftM2`, `LiftM3` + + `(<=)`, `(>=)`, `(<)`, `(>)` + + `Guarded`, `Guard((:=))`, `Otherwise` + +# 0.3.0.1 + +- GHC 8.6 compatibility + +# 0.3.0.0 + +- More new functions, (thanks to isovector) + +# 0.2.0.0 + +- A whole bunch of basic functions (thanks to isovector) +- Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`) + +# 0.1.0.0 + +Initial version
LICENSE view
@@ -1,4 +1,4 @@-Copyright Li-yao Xia (c) 2018-2024+Copyright Li-yao Xia (c) 2018-2025 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
first-class-families.cabal view
@@ -1,63 +1,63 @@-name: first-class-families-version: 0.8.1.0-synopsis:- First-class type families-description:- A library for type-level programming.- .- See README.-homepage: https://github.com/Lysxia/first-class-families#readme-license: MIT-license-file: LICENSE-author: Li-yao Xia-maintainer: lysxia@gmail.com-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 == 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- exposed-modules:- Fcf- Fcf.Core- Fcf.Combinators- Fcf.Data.Bool- Fcf.Data.Common- Fcf.Data.Function- Fcf.Data.List- Fcf.Data.Nat- Fcf.Data.Symbol- Fcf.Classes- Fcf.Class.Bifunctor- Fcf.Class.Foldable- Fcf.Class.Functor- Fcf.Class.Monoid- Fcf.Class.Monoid.Types- Fcf.Class.Ord- Fcf.Utils- build-depends:- 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- hs-source-dirs: test- main-is: test.hs- default-language: Haskell2010- build-depends:- base,- first-class-families--source-repository head- type: git- location: https://github.com/Lysxia/first-class-families+name: first-class-families +version: 0.8.2.0 +synopsis: + First-class type families +description: + A library for type-level programming. + . + See README. +homepage: https://github.com/Lysxia/first-class-families#readme +license: MIT +license-file: LICENSE +author: Li-yao Xia +maintainer: lysxia@gmail.com +copyright: 2018-2025 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.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.1, + GHC == 9.2.8, GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4, + GHC == 9.10.1, GHC == 9.12.2 + +library + hs-source-dirs: src + exposed-modules: + Fcf + Fcf.Core + Fcf.Combinators + Fcf.Data.Bool + Fcf.Data.Common + Fcf.Data.Function + Fcf.Data.List + Fcf.Data.Nat + Fcf.Data.Symbol + Fcf.Classes + Fcf.Class.Bifunctor + Fcf.Class.Foldable + Fcf.Class.Functor + Fcf.Class.Monoid + Fcf.Class.Monoid.Types + Fcf.Class.Ord + Fcf.Utils + build-depends: + 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 + hs-source-dirs: test + main-is: test.hs + default-language: Haskell2010 + build-depends: + base, + first-class-families + +source-repository head + type: git + location: https://github.com/Lysxia/first-class-families
src/Fcf.hs view
@@ -1,150 +1,186 @@-{-# LANGUAGE TypeOperators #-}---- | First-class type families------ For example, here is a regular type family:------ @--- type family FromMaybe (a :: k) (m :: Maybe k) :: k--- type instance FromMaybe a 'Nothing = a--- type instance FromMaybe a ('Just b) = b--- @------ With @Fcf@, it translates to a @data@ declaration:------ @--- data FromMaybe :: k -> Maybe k -> 'Exp' k--- type instance 'Eval' (FromMaybe a 'Nothing) = a--- type instance 'Eval' (FromMaybe a ('Just b)) = b--- @------ - Fcfs can be higher-order.--- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.------ Essential language extensions for "Fcf":------ > {-# LANGUAGE--- > DataKinds,--- > PolyKinds,--- > TypeFamilies,--- > TypeOperators,--- > UndecidableInstances #-}--module Fcf- ( -- * First-class type families-- Exp- , Eval- , type (@@)-- -- ** Functional combinators-- , Pure- , Pure1- , Pure2- , Pure3- , type (=<<)- , type (<=<)- , LiftM- , LiftM2- , LiftM3- , Join- , type (<$>)- , type (<*>)- , Flip- , ConstFn- , type ($)-- -- * Operations on common types-- -- ** Pairs-- , Uncurry- , Fst- , Snd- , type (***)-- -- ** Either-- , UnEither- , IsLeft- , IsRight-- -- ** Maybe-- , UnMaybe- , FromMaybe- , IsNothing- , IsJust-- -- ** Lists-- , Foldr- , UnList- , type (++)- , Filter- , Head- , Tail- , Null- , Length- , Find- , FindIndex- , Lookup- , SetIndex- , ZipWith- , Zip- , Unzip- , Cons2-- -- ** Bool-- , UnBool- , type (||)- , type (&&)- , Not-- -- ** Case splitting-- , Case- , Match()- , type (-->)- , Is- , Any- , Else-- -- ** Nat-- , type (+)- , type (-)- , type (Fcf.Data.Nat.*)- , type (^)- , type (<=)- , type (>=)- , type (<)- , type (>)-- -- * Overloaded operations-- , Map- , Bimap-- -- * Miscellaneous-- , Error- , Constraints- , TyEq- , Stuck- , IsBool(_If)- , If-- ) where--import Fcf.Core-import Fcf.Combinators-import Fcf.Data.Bool-import Fcf.Data.Common-import Fcf.Data.List-import Fcf.Data.Nat-import Fcf.Class.Functor-import Fcf.Class.Bifunctor-import Fcf.Utils+{-# LANGUAGE TypeOperators #-} + +-- | First-class type families +-- +-- For example, here is a regular type family: +-- +-- @ +-- type family FromMaybe (a :: k) (m :: Maybe k) :: k +-- type instance FromMaybe a 'Nothing = a +-- type instance FromMaybe a ('Just b) = b +-- @ +-- +-- With @Fcf@, it translates to a @data@ declaration: +-- +-- @ +-- data FromMaybe :: k -> Maybe k -> 'Exp' k +-- type instance 'Eval' (FromMaybe a 'Nothing) = a +-- type instance 'Eval' (FromMaybe a ('Just b)) = b +-- @ +-- +-- - Fcfs can be higher-order. +-- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'. +-- +-- Essential language extensions for "Fcf": +-- +-- > {-# LANGUAGE +-- > DataKinds, +-- > PolyKinds, +-- > TypeFamilies, +-- > TypeOperators, +-- > UndecidableInstances #-} + +module Fcf + ( -- * First-class type families + + Exp + , Eval + , type (@@) + + -- ** Functional combinators + + , Pure + , Pure1 + , Pure2 + , Pure3 + , Pure4 + , Pure5 + , Pure6 + , Pure7 + , Pure8 + , Pure9 + , type (=<<) + , type (>>=) + , type (<=<) + , LiftM + , LiftM2 + , LiftM3 + , Join + , type (<$>) + , type (<*>) + , Flip + , ConstFn + , type ($) + + -- * Operations on common types + + -- ** Pairs + + , Uncurry + , Fst + , Snd + , type (***) + + -- ** Either + + , UnEither + , IsLeft + , IsRight + + -- ** Maybe + + , UnMaybe + , FromMaybe + , IsNothing + , IsJust + + -- ** Lists + + , type (++) + , Head + , Last + , Tail + , Cons + , Snoc + , Cons2 + , Init + , Uncons + , Unsnoc + , Singleton + , Null + , Length + , Reverse + , Intersperse + , Intercalate + , Foldr + , UnList + , Concat + , ConcatMap + , Unfoldr + , Replicate + , Take + , Drop + , SplitAt + , TakeWhile + , DropWhile + , Span + , Break + , Tails + , IsPrefixOf + , IsSuffixOf + , IsInfixOf + , Elem + , Lookup + , Find + , Filter + , Partition + , FindIndex + , SetIndex + , ZipWith + , Zip + , Unzip + + -- ** Bool + + , UnBool + , type (||) + , type (&&) + , Not + + -- ** Case splitting + + , Case + , Match() + , type (-->) + , Is + , Any + , Else + + -- ** Nat + + , type (+) + , type (-) + , type (Fcf.Data.Nat.*) + , type (^) + , type (<=) + , type (>=) + , type (<) + , type (>) + + -- * Overloaded operations + + , Map + , Bimap + + -- * Miscellaneous + + , Error + , Constraints + , TyEq + , Stuck + , IsBool(_If) + , If + , Assert + , AssertNot + + ) where + +import Fcf.Core +import Fcf.Combinators +import Fcf.Data.Bool +import Fcf.Data.Common +import Fcf.Data.List +import Fcf.Data.Nat +import Fcf.Class.Functor +import Fcf.Class.Bifunctor +import Fcf.Utils
src/Fcf/Combinators.hs view
@@ -13,6 +13,12 @@ , Pure1 , Pure2 , Pure3+ , Pure4+ , Pure5+ , Pure6+ , Pure7+ , Pure8+ , Pure9 , type (=<<) , type (>>=) , type (<=<)@@ -46,6 +52,24 @@ data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d type instance Eval (Pure3 f x y z) = f x y z++data Pure4 :: (a -> b -> c -> d -> e) -> a -> b -> c -> d -> Exp e+type instance Eval (Pure4 f w x y z) = f w x y z++data Pure5 :: (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> Exp f+type instance Eval (Pure5 f v w x y z) = f v w x y z++data Pure6 :: (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> Exp g+type instance Eval (Pure6 f u v w x y z) = f u v w x y z++data Pure7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> Exp h+type instance Eval (Pure7 f t u v w x y z) = f t u v w x y z++data Pure8 :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> Exp i+type instance Eval (Pure8 f s t u v w x y z) = f s t u v w x y z++data Pure9 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> Exp j+type instance Eval (Pure9 f r s t u v w x y z) = f r s t u v w x y z data (=<<) :: (a -> Exp b) -> Exp a -> Exp b type instance Eval (k =<< e) = Eval (k (Eval e))
src/Fcf/Data/List.hs view
@@ -1,575 +1,621 @@-{-# LANGUAGE- DataKinds,- PolyKinds,- TypeFamilies,- TypeOperators,- UndecidableInstances #-}---- | Lists.------ See also "Fcf.Class.Foldable" for additional functions.-module Fcf.Data.List- ( -- * Basic functions- type (++)- , Head- , Last- , Tail- , Cons- , Snoc- , Cons2- , Init- , Null- , Length-- -- * List transformations- , Reverse- , Intersperse- , Intercalate-- -- * Reducing lists- -- | See also "Fcf.Class.Foldable".- , Foldr- , UnList- , Concat- , ConcatMap-- -- * Unfolding and building- , Unfoldr- , Replicate-- -- * Sublists- , Take- , Drop- , TakeWhile- , DropWhile- , Span- , Break- , Tails-- -- ** Predicates- , IsPrefixOf- , IsSuffixOf- , IsInfixOf-- -- * Searching- , Elem- , Lookup- , Find- , Filter- , Partition-- -- * Indexing lists- , FindIndex- , SetIndex-- -- * Zipping and unzipping- , ZipWith- , Zip- , Unzip- ) where--import qualified GHC.TypeLits as TL--import Fcf.Core-import Fcf.Combinators-import Fcf.Class.Functor (Map)-import Fcf.Class.Monoid (type (<>))-import Fcf.Class.Foldable-import Fcf.Data.Bool-import Fcf.Data.Common-import Fcf.Data.Nat-import Fcf.Utils (If, TyEq)---- $setup--- >>> :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]) :: [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---data Head :: [a] -> Exp (Maybe a)-type instance Eval (Head '[]) = 'Nothing-type instance Eval (Head (a ': _as)) = 'Just a--data Last :: [a] -> Exp (Maybe a)-type instance Eval (Last '[]) = 'Nothing-type instance Eval (Last (a ': '[])) = 'Just a-type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))--data Init :: [a] -> Exp (Maybe [a])-type instance Eval (Init '[]) = 'Nothing-type instance Eval (Init (a ': '[])) = 'Just '[]-type instance Eval (Init (a ': b ': as)) =- Eval (Map (Cons a) =<< (Init (b ': as)))--data Tail :: [a] -> Exp (Maybe [a])-type instance Eval (Tail '[]) = 'Nothing-type instance Eval (Tail (_a ': as)) = 'Just as--data Null :: [a] -> Exp Bool-type instance Eval (Null '[]) = 'True-type instance Eval (Null (a ': as)) = 'False--data Length :: [a] -> Exp Nat-type instance Eval (Length '[]) = 0-type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)----- | Append an element to a list.------ === __Example__------ >>> :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---- | Append elements to two lists. Used in the definition of 'Unzip'.-data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])-type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)---- | Append an element to the end of a list.------ === __Example__------ >>> :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])----- Helper for Reverse. This corresponds to rev in the data list lib.-data Rev :: [a] -> [a] -> Exp [a]-type instance Eval (Rev '[] ys) = ys-type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys))----- | Reverse a list.------ === __Example__------ >>> :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 '[])---- | Intersperse a separator between elements of a list.------ === __Example__------ >>> :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)---- | Helper for Intersperse-data PrependToAll :: a -> [a] -> Exp [a]-type instance Eval (PrependToAll _ '[] ) = '[]-type instance Eval (PrependToAll sep (x ': xs)) = sep ': x ': Eval (PrependToAll sep xs)---- | Join a list of words separated by some word.------ === __Example__------ >>> :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)----- | This is 'Foldr' with its argument flipped.-data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b-type instance Eval (UnList y f xs) = Eval (Foldr f y xs)----- Helper for the Unfoldr.-data UnfoldrCase :: (b -> Exp (Maybe (a, b))) -> Maybe (a, b) -> Exp [a]-type instance Eval (UnfoldrCase f ('Just ab)) =- Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))-type instance Eval (UnfoldrCase _ 'Nothing) = '[]---- | Unfold a generator into a list.------ === __Example__------ >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))--- >>> :{--- type instance Eval (ToThree b) =--- If (4 TL.<=? b)--- Nothing--- (Just '(b, b TL.+ 1))--- :}------ >>> :kind! Eval (Unfoldr ToThree 0)--- 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]-type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c))----- Helper for the Replicate.-data NumIter :: a -> Nat -> Exp (Maybe (a, Nat))-type instance Eval (NumIter a s) =- If (Eval (s > 0))- ('Just '(a, s TL.- 1))- 'Nothing---- | Repeat the same element in a list.------ === __Example__------ >>> :kind! Eval (Replicate 4 '("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)----- | Take a prefix of fixed length.------ === __Example__------ >>> :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--type family Take_ (n :: Nat) (xs :: [a]) :: [a] where- Take_ 0 _ = '[]- Take_ _ '[] = '[]- Take_ n (x ': xs) = x ': Take_ (n TL.- 1) xs---- | Drop a prefix of fixed length, evaluate to the remaining suffix.------ === __Example__------ >>> :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--type family Drop_ (n :: Nat) (xs :: [a]) :: [a] where- Drop_ 0 xs = xs- Drop_ _ '[] = '[]- Drop_ n (x ': xs) = Drop_ (n TL.- 1) xs---- | Take the longest prefix of elements satisfying a predicate.------ === __Example__------ >>> :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)) =- Eval (If (Eval (p x))- ('(:) x <$> TakeWhile p xs)- (Pure '[]))---- | Drop the longest prefix of elements satisfying a predicate,--- evaluate to the remaining suffix.------ === __Example__------ :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)) =- Eval (If (Eval (p x))- (DropWhile p xs)- (Pure (x ': xs)))----- | 'Span', applied to a predicate @p@ and a list @xs@, returns a tuple:--- the first component is the longest prefix (possibly empty) of @xs@ whose elements--- satisfy @p@;--- the second component is the remainder of the list.------ See also 'TakeWhile', 'DropWhile', and 'Break'.------ === __Example__------ >>> :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]) :: ([Natural], [Natural])--- = '([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))----- | 'Break', applied to a predicate @p@ and a list @xs@, returns a tuple:--- the first component is the longest prefix (possibly empty) of @xs@ whose elements--- /do not satisfy/ @p@; the second component is the remainder of the list.------ === __Example__------ >>> :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]) :: ([Natural], [Natural])--- = '( '[], [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)----- | List of suffixes of a list.------ === __Example__------ >>> :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)----- | Return @True@ when the first list is a prefix of the second.------ === __Example__------ >>> :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 ([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 ([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---- helper for IsPrefixOf-type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where- IsPrefixOf_ '[] _ = 'True- IsPrefixOf_ _ '[] = 'False- IsPrefixOf_ (x ': xs) (y ': ys) =- Eval ((Eval (TyEq x y)) && IsPrefixOf_ xs ys)----- | Return @True@ when the first list is a suffix of the second.------ === __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,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--- = False-data IsSuffixOf :: [a] -> [a] -> Exp Bool-type instance Eval (IsSuffixOf xs ys) =- Eval (IsPrefixOf (Reverse @@ xs) (Reverse @@ ys))----- | Return @True@ when the first list is contained within the second.------ === __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,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)----- | Return @True@ if an element is in a list.------ See also 'FindIndex'.------ === __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----data Elem :: a -> [a] -> Exp Bool-type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)---- | Find an element associated with a key in an association list.-data Lookup :: k -> [(k, b)] -> Exp (Maybe b)-type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =- Eval (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))----- | Find @Just@ the first element satisfying a predicate, or evaluate to--- @Nothing@ if no element satisfies the predicate.------ === __Example__------ >>> :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 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)) =- Eval (If (Eval (p a))- (Pure ('Just a))- (Find p as))----- | Keep all elements that satisfy a predicate, remove all that don't.------ === __Example__------ >>> :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)) =- Eval (If (Eval (p a))- ('(:) a <$> Filter p as)- (Filter p as))----- | Split a list into one where all elements satisfy a predicate,--- and a second where no elements satisfy it.------ === __Example__------ >>> :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)---- | Helper for 'Partition'.-data PartHelp :: (a -> Exp Bool) -> a -> ([a],[a]) -> Exp ([a],[a])-type instance Eval (PartHelp p a '(xs,ys)) =- If (Eval (p a))- '(a ': xs, ys)- '(xs, a ': ys)----- | Find the index of an element satisfying the predicate.------ === __Example__------ >>> :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 Natural--- = Nothing-data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)-type instance Eval (FindIndex _p '[]) = 'Nothing-type instance Eval (FindIndex p (a ': as)) =- Eval (If (Eval (p a))- (Pure ('Just 0))- (Map ((+) 1) =<< FindIndex p as))----- | Modify an element at a given index.------ The list is unchanged if the index is out of bounds.------ === __Example__------ >>> :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--type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where- SetIndexImpl _n _a' '[] = '[]- SetIndexImpl 0 a' (_a ': as) = a' ': as- SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as---- | Combine elements of two lists pairwise.------ === __Example__------ >>> :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 '[]) = '[]-type instance Eval (ZipWith f (a ': as) (b ': bs)) =- Eval (f a b) ': Eval (ZipWith f as bs)--data Zip :: [a] -> [b] -> Exp [(a, b)]-type instance Eval (Zip as bs) = Eval (ZipWith (Pure2 '(,)) as bs)--data Unzip :: Exp [(a, b)] -> Exp ([a], [b])-type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))+{-# LANGUAGE + DataKinds, + PolyKinds, + TypeFamilies, + TypeOperators, + UndecidableInstances #-} + +-- | Lists. +-- +-- See also "Fcf.Class.Foldable" for additional functions. +module Fcf.Data.List + ( -- * Basic functions + type (++) + , Head + , Last + , Tail + , Cons + , Snoc + , Cons2 + , Init + , Uncons + , Unsnoc + , Singleton + , Null + , Length + + -- * List transformations + , Reverse + , Intersperse + , Intercalate + + -- * Reducing lists + -- | See also "Fcf.Class.Foldable". + , Foldr + , UnList + , Concat + , ConcatMap + + -- * Unfolding and building + , Unfoldr + , Replicate + + -- * Sublists + , Take + , Drop + , SplitAt + , TakeWhile + , DropWhile + , Span + , Break + , Tails + + -- ** Predicates + , IsPrefixOf + , IsSuffixOf + , IsInfixOf + + -- * Searching + , Elem + , Lookup + , Find + , Filter + , Partition + + -- * Indexing lists + , FindIndex + , SetIndex + + -- * Zipping and unzipping + , ZipWith + , Zip + , Unzip + ) where + +import qualified GHC.TypeLits as TL + +import Fcf.Core +import Fcf.Combinators +import Fcf.Class.Functor (Map) +import Fcf.Class.Monoid (type (<>)) +import Fcf.Class.Foldable +import Fcf.Data.Bool +import Fcf.Data.Common +import Fcf.Data.Nat +import Fcf.Utils (If, TyEq) + +-- $setup +-- >>> :set -XGADTs -XUndecidableInstances -XDataKinds +-- >>> import Fcf.Core (Exp, Eval) +-- >>> import Fcf.Combinators +-- >>> import Fcf.Class.Foldable (Concat) +-- >>> import Fcf.Class.Functor () +-- >>> 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]) :: [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 + + +data Head :: [a] -> Exp (Maybe a) +type instance Eval (Head '[]) = 'Nothing +type instance Eval (Head (a ': _as)) = 'Just a + +data Last :: [a] -> Exp (Maybe a) +type instance Eval (Last '[]) = 'Nothing +type instance Eval (Last (a ': '[])) = 'Just a +type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as)) + +data Init :: [a] -> Exp (Maybe [a]) +type instance Eval (Init '[]) = 'Nothing +type instance Eval (Init (a ': '[])) = 'Just '[] +type instance Eval (Init (a ': b ': as)) = + Eval (Map (Cons a) =<< (Init (b ': as))) + +data Uncons :: [a] -> Exp (Maybe (a, [a])) +type instance Eval (Uncons '[]) = 'Nothing +type instance Eval (Uncons (a ': xs)) = 'Just '(a, xs) + +-- | Decompose a list into 'init' and 'last' +-- +-- === __Example__ +-- +-- >>> :kind! Eval (Unsnoc '[]) +-- Eval (Unsnoc '[]) :: Maybe ([a], a) +-- = Nothing +-- +-- >>> :kind! Eval (Unsnoc '[1]) +-- Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural) +-- = Just '( '[], 1) +-- +-- >>> :kind! Eval (Unsnoc '[1,2,3]) +-- Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural) +-- = Just '([1, 2], 3) +data Unsnoc :: [a] -> Exp (Maybe ([a], a)) +type instance Eval (Unsnoc '[]) = 'Nothing +type instance Eval (Unsnoc (x ': '[])) = 'Just '( '[], x) +type instance Eval (Unsnoc (x ': y ': ys)) = Eval (Map (PrependF x) =<< Unsnoc (y ': ys)) + +data PrependF :: a -> ([a], a) -> Exp ([a], a) +type instance Eval (PrependF x '(xs, y)) = '(x ': xs, y) + +data Singleton :: a -> Exp [a] +type instance Eval (Singleton x) = '[x] + +data Tail :: [a] -> Exp (Maybe [a]) +type instance Eval (Tail '[]) = 'Nothing +type instance Eval (Tail (_a ': as)) = 'Just as + +data Null :: [a] -> Exp Bool +type instance Eval (Null '[]) = 'True +type instance Eval (Null (a ': as)) = 'False + +data Length :: [a] -> Exp Nat +type instance Eval (Length '[]) = 0 +type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as) + + +-- | Append an element to a list. +-- +-- === __Example__ +-- +-- >>> :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 + +-- | Append elements to two lists. Used in the definition of 'Unzip'. +data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b]) +type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs) + +-- | Append an element to the end of a list. +-- +-- === __Example__ +-- +-- >>> :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]) + + +-- Helper for Reverse. This corresponds to rev in the data list lib. +data Rev :: [a] -> [a] -> Exp [a] +type instance Eval (Rev '[] ys) = ys +type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys)) + + +-- | Reverse a list. +-- +-- === __Example__ +-- +-- >>> :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 '[]) + +-- | Intersperse a separator between elements of a list. +-- +-- === __Example__ +-- +-- >>> :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) + +-- | Helper for Intersperse +data PrependToAll :: a -> [a] -> Exp [a] +type instance Eval (PrependToAll _ '[] ) = '[] +type instance Eval (PrependToAll sep (x ': xs)) = sep ': x ': Eval (PrependToAll sep xs) + +-- | Join a list of words separated by some word. +-- +-- === __Example__ +-- +-- >>> :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) + + +-- | This is 'Foldr' with its argument flipped. +data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b +type instance Eval (UnList y f xs) = Eval (Foldr f y xs) + + +-- Helper for the Unfoldr. +data UnfoldrCase :: (b -> Exp (Maybe (a, b))) -> Maybe (a, b) -> Exp [a] +type instance Eval (UnfoldrCase f ('Just ab)) = + Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab))) +type instance Eval (UnfoldrCase _ 'Nothing) = '[] + +-- | Unfold a generator into a list. +-- +-- === __Example__ +-- +-- >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat)) +-- >>> :{ +-- type instance Eval (ToThree b) = +-- If (4 TL.<=? b) +-- Nothing +-- (Just '(b, b TL.+ 1)) +-- :} +-- +-- >>> :kind! Eval (Unfoldr ToThree 0) +-- 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] +type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c)) + + +-- Helper for the Replicate. +data NumIter :: a -> Nat -> Exp (Maybe (a, Nat)) +type instance Eval (NumIter a s) = + If (Eval (s > 0)) + ('Just '(a, s TL.- 1)) + 'Nothing + +-- | Repeat the same element in a list. +-- +-- === __Example__ +-- +-- >>> :kind! Eval (Replicate 4 '("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) + + +-- | Take a prefix of fixed length. +-- +-- === __Example__ +-- +-- >>> :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 + +type family Take_ (n :: Nat) (xs :: [a]) :: [a] where + Take_ 0 _ = '[] + Take_ _ '[] = '[] + Take_ n (x ': xs) = x ': Take_ (n TL.- 1) xs + +-- | Drop a prefix of fixed length, evaluate to the remaining suffix. +-- +-- === __Example__ +-- +-- >>> :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 + +type family Drop_ (n :: Nat) (xs :: [a]) :: [a] where + Drop_ 0 xs = xs + Drop_ _ '[] = '[] + Drop_ n (x ': xs) = Drop_ (n TL.- 1) xs + +-- | Return a tuple where first element is @xs@ prefix of length @n@ +-- and second element is the remainder of the list. +-- +-- === __Example__ +-- +-- >>> :kind! Eval (SplitAt 3 '[1,2,3,4,5]) +-- Eval (SplitAt 3 '[1,2,3,4,5]) :: ([Natural], [Natural]) +-- = '([1, 2, 3], [4, 5]) +data SplitAt :: Nat -> [a] -> Exp ([a], [a]) +type instance Eval (SplitAt n xs) = '(Eval (Take n xs), Eval (Drop n xs)) + +-- | Take the longest prefix of elements satisfying a predicate. +-- +-- === __Example__ +-- +-- >>> :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)) = + Eval (If (Eval (p x)) + ('(:) x <$> TakeWhile p xs) + (Pure '[])) + +-- | Drop the longest prefix of elements satisfying a predicate, +-- evaluate to the remaining suffix. +-- +-- === __Example__ +-- +-- :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)) = + Eval (If (Eval (p x)) + (DropWhile p xs) + (Pure (x ': xs))) + + +-- | 'Span', applied to a predicate @p@ and a list @xs@, returns a tuple: +-- the first component is the longest prefix (possibly empty) of @xs@ whose elements +-- satisfy @p@; +-- the second component is the remainder of the list. +-- +-- See also 'TakeWhile', 'DropWhile', and 'Break'. +-- +-- === __Example__ +-- +-- >>> :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]) :: ([Natural], [Natural]) +-- = '([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)) + + +-- | 'Break', applied to a predicate @p@ and a list @xs@, returns a tuple: +-- the first component is the longest prefix (possibly empty) of @xs@ whose elements +-- /do not satisfy/ @p@; the second component is the remainder of the list. +-- +-- === __Example__ +-- +-- >>> :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]) :: ([Natural], [Natural]) +-- = '( '[], [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) + + +-- | List of suffixes of a list. +-- +-- === __Example__ +-- +-- >>> :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) + + +-- | Return @True@ when the first list is a prefix of the second. +-- +-- === __Example__ +-- +-- >>> :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 ([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 ([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 + +-- helper for IsPrefixOf +type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where + IsPrefixOf_ '[] _ = 'True + IsPrefixOf_ _ '[] = 'False + IsPrefixOf_ (x ': xs) (y ': ys) = + Eval ((Eval (TyEq x y)) && IsPrefixOf_ xs ys) + + +-- | Return @True@ when the first list is a suffix of the second. +-- +-- === __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,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 +-- = False +data IsSuffixOf :: [a] -> [a] -> Exp Bool +type instance Eval (IsSuffixOf xs ys) = + Eval (IsPrefixOf (Reverse @@ xs) (Reverse @@ ys)) + + +-- | Return @True@ when the first list is contained within the second. +-- +-- === __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,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) + + +-- | Return @True@ if an element is in a list. +-- +-- See also 'FindIndex'. +-- +-- === __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 +-- +data Elem :: a -> [a] -> Exp Bool +type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as) + +-- | Find an element associated with a key in an association list. +data Lookup :: k -> [(k, b)] -> Exp (Maybe b) +type instance Eval (Lookup (a :: k) (as :: [(k, b)])) = + Eval (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b)) + + +-- | Find @Just@ the first element satisfying a predicate, or evaluate to +-- @Nothing@ if no element satisfies the predicate. +-- +-- === __Example__ +-- +-- >>> :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 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)) = + Eval (If (Eval (p a)) + (Pure ('Just a)) + (Find p as)) + + +-- | Keep all elements that satisfy a predicate, remove all that don't. +-- +-- === __Example__ +-- +-- >>> :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)) = + Eval (If (Eval (p a)) + ('(:) a <$> Filter p as) + (Filter p as)) + + +-- | Split a list into one where all elements satisfy a predicate, +-- and a second where no elements satisfy it. +-- +-- === __Example__ +-- +-- >>> :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) + +-- | Helper for 'Partition'. +data PartHelp :: (a -> Exp Bool) -> a -> ([a],[a]) -> Exp ([a],[a]) +type instance Eval (PartHelp p a '(xs,ys)) = + If (Eval (p a)) + '(a ': xs, ys) + '(xs, a ': ys) + + +-- | Find the index of an element satisfying the predicate. +-- +-- === __Example__ +-- +-- >>> :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 Natural +-- = Nothing +data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat) +type instance Eval (FindIndex _p '[]) = 'Nothing +type instance Eval (FindIndex p (a ': as)) = + Eval (If (Eval (p a)) + (Pure ('Just 0)) + (Map ((+) 1) =<< FindIndex p as)) + + +-- | Modify an element at a given index. +-- +-- The list is unchanged if the index is out of bounds. +-- +-- === __Example__ +-- +-- >>> :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 + +type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where + SetIndexImpl _n _a' '[] = '[] + SetIndexImpl 0 a' (_a ': as) = a' ': as + SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as + +-- | Combine elements of two lists pairwise. +-- +-- === __Example__ +-- +-- >>> :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 '[]) = '[] +type instance Eval (ZipWith f (a ': as) (b ': bs)) = + Eval (f a b) ': Eval (ZipWith f as bs) + +data Zip :: [a] -> [b] -> Exp [(a, b)] +type instance Eval (Zip as bs) = Eval (ZipWith (Pure2 '(,)) as bs) + +data Unzip :: Exp [(a, b)] -> Exp ([a], [b]) +type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
src/Fcf/Utils.hs view
@@ -1,136 +1,170 @@-{-# LANGUAGE- AllowAmbiguousTypes,- ConstraintKinds,- DataKinds,- PolyKinds,- RankNTypes,- TypeFamilies,- TypeOperators,- UndecidableInstances #-}---- | Miscellaneous families.-module Fcf.Utils- ( Error- , TError- , Constraints- , TyEq- , Stuck- , IsBool(_If)- , Case- , Match()- , type (-->)- , Is- , Any- , Else-- -- * From "Data.Type.Bool"- , If- ) where--import Data.Kind (Constraint)-import Data.Type.Bool (If)-import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))--import Fcf.Core-import Fcf.Combinators (Pure)---- | Type-level 'error'.-data Error :: Symbol -> Exp a-type instance Eval (Error msg) = TypeError ('Text msg)---- | 'TypeError' as a fcf.-data TError :: ErrorMessage -> Exp a-type instance Eval (TError msg) = TypeError msg---- | Conjunction of a list of constraints.-data Constraints :: [Constraint] -> Exp Constraint-type instance Eval (Constraints '[]) = (() :: Constraint)-type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))---- | Type equality.------ === __Details__------ The base library also defines a similar @('Type.Equality.==')@;--- it differs from 'TyEq' in the following ways:------ * 'TyEq' is heterogeneous: its arguments may have different kinds;--- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is--- a variable.-data TyEq :: a -> b -> Exp Bool-type instance Eval (TyEq a b) = TyEqImpl a b--type family TyEqImpl (a :: k) (b :: l) :: Bool where- TyEqImpl a a = 'True- TyEqImpl a b = 'False---- | A stuck type that can be used like a type-level 'undefined'.-type family Stuck :: a---- * Reification--class IsBool (b :: Bool) where- _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r--instance IsBool 'True where _If a _ = a-instance IsBool 'False where _If _ b = b---- * Case splitting--infix 0 -->--data Match j k- = Match_ j k- | Is_ (j -> Exp Bool) k- | Any_ k- | Else_ (j -> Exp k)---- | (Limited) equivalent of @\\case { .. }@ syntax. Supports matching of exact--- values ('-->') and final matches for any value ('Any') or for passing value--- to subcomputation ('Else'). Examples:------ @--- type BoolToNat = 'Case'--- [ 'True '-->' 0--- , 'False '-->' 1--- ]------ type NatToBool = 'Case'--- [ 0 '-->' 'False--- , 'Any' 'True--- ]------ type ZeroOneOrSucc = 'Case'--- [ 0 '-->' 0--- , 1 '-->' 1--- , 'Else' (('+') 1)--- ]--- @-data Case :: [Match j k] -> j -> Exp k-type instance Eval (Case ms a) = Case_ ms a--type family Case_ (ms :: [Match j k]) (a :: j) :: k where- Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a))- Case_ ('Is_ p b : ms) a = Case_ [ 'True --> b- , 'False --> Case_ ms a- ] (p @@ a)- Case_ ('Any_ b : _ ) _ = b- Case_ ('Else_ f : _ ) a = f @@ a---- | Match concrete type in 'Case'.-type (-->) = ('Match_ :: j -> k -> Match j k)---- | Match on predicate being successful with type in 'Case'.-type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)---- | Match any type in 'Case'. Should be used as a final branch.------ Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable")--- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").------ We recommend importing this one qualified.-type Any = ('Any_ :: k -> Match j k)---- | Pass type being matched in 'Case' to subcomputation. Should be used as a--- final branch.-type Else = ('Else_ :: (j -> Exp k) -> Match j k)+{-# LANGUAGE + AllowAmbiguousTypes, + ConstraintKinds, + DataKinds, + PolyKinds, + RankNTypes, + TypeFamilies, + TypeOperators, + UndecidableInstances #-} + +-- | Miscellaneous families. +module Fcf.Utils + ( Error + , TError + , Constraints + , TyEq + , Stuck + , IsBool(_If) + , Case + , Match() + , type (-->) + , Is + , Any + , Else + + -- * From "Data.Type.Bool" + , If + + -- * Compile-time asserts + , Assert + , AssertNot + + -- * Reexports + , GHC.TypeLits.ErrorMessage(Text, ShowType, type (:<>:), type (:$$:)) + , GHC.TypeLits.TypeError + ) where + +import Data.Kind (Constraint) +import Data.Type.Bool (If) +import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..)) + +import Fcf.Core +import Fcf.Combinators (Pure, type (=<<)) +import Fcf.Data.Bool (Not) + +-- | Type-level 'error'. +data Error :: Symbol -> Exp a +type instance Eval (Error msg) = TypeError ('Text msg) + +-- | 'TypeError' as a fcf. +data TError :: ErrorMessage -> Exp a +type instance Eval (TError msg) = TypeError msg + +-- | Conjunction of a list of constraints. +data Constraints :: [Constraint] -> Exp Constraint +type instance Eval (Constraints '[]) = (() :: Constraint) +type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as)) + +-- | Type equality. +-- +-- === __Details__ +-- +-- The base library also defines a similar @('Type.Equality.==')@; +-- it differs from 'TyEq' in the following ways: +-- +-- * 'TyEq' is heterogeneous: its arguments may have different kinds; +-- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is +-- a variable. +data TyEq :: a -> b -> Exp Bool +type instance Eval (TyEq a b) = TyEqImpl a b + +type family TyEqImpl (a :: k) (b :: l) :: Bool where + TyEqImpl a a = 'True + TyEqImpl a b = 'False + +-- | A stuck type that can be used like a type-level 'undefined'. +type family Stuck :: a + +-- * Reification + +class IsBool (b :: Bool) where + _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r + +instance IsBool 'True where _If a _ = a +instance IsBool 'False where _If _ b = b + +-- * Case splitting + +infix 0 --> + +data Match j k + = Match_ j k + | Is_ (j -> Exp Bool) k + | Any_ k + | Else_ (j -> Exp k) + +-- | (Limited) equivalent of @\\case { .. }@ syntax. Supports matching of exact +-- values ('-->') and final matches for any value ('Any') or for passing value +-- to subcomputation ('Else'). Examples: +-- +-- @ +-- type BoolToNat = 'Case' +-- [ 'True '-->' 0 +-- , 'False '-->' 1 +-- ] +-- +-- type NatToBool = 'Case' +-- [ 0 '-->' 'False +-- , 'Any' 'True +-- ] +-- +-- type ZeroOneOrSucc = 'Case' +-- [ 0 '-->' 0 +-- , 1 '-->' 1 +-- , 'Else' (('+') 1) +-- ] +-- @ +data Case :: [Match j k] -> j -> Exp k +type instance Eval (Case ms a) = Case_ ms a + +type family Case_ (ms :: [Match j k]) (a :: j) :: k where + Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a)) + Case_ ('Is_ p b : ms) a = Case_ [ 'True --> b + , 'False --> Case_ ms a + ] (p @@ a) + Case_ ('Any_ b : _ ) _ = b + Case_ ('Else_ f : _ ) a = f @@ a + +-- | Match concrete type in 'Case'. +type (-->) = ('Match_ :: j -> k -> Match j k) + +-- | Match on predicate being successful with type in 'Case'. +type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k) + +-- | Match any type in 'Case'. Should be used as a final branch. +-- +-- Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable") +-- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts"). +-- +-- We recommend importing this one qualified. +type Any = ('Any_ :: k -> Match j k) + +-- | Pass type being matched in 'Case' to subcomputation. Should be used as a +-- final branch. +type Else = ('Else_ :: (j -> Exp k) -> Match j k) + +-- | A compile-time assert. +-- +-- Raises the provided `TypeError`, whenever the condition evaluates to `False`. +-- +-- Usage example: +-- @ +-- type ExampleAssertionFailure = Eval ( +-- Pure '["foo", "bar"] +-- >>= Length +-- >>= Assert ('Text "Assertion") (TyEq Int Void) +-- ) +-- @ +data Assert :: ErrorMessage -> Exp Bool -> r -> Exp r +type instance Eval (Assert msg mcond k) + = Eval (If (Eval mcond) (Pure k) (TError msg)) + +-- | Compile-time assert, with condition negated. +-- +-- Raises the provided `TypeError`, whenever the condition evaluates to `True`. +-- +-- Also see 'Assert'. +data AssertNot :: forall r. ErrorMessage -> Exp Bool -> r -> Exp r +type instance Eval (AssertNot err mcond k) + = Eval (Assert err (Not =<< mcond) k)
test/test.hs view
@@ -1,100 +1,106 @@-{-# LANGUAGE- CPP,- DataKinds,- KindSignatures,- TypeOperators #-}--import Data.Type.Equality ((:~:)(Refl))-import qualified Data.Monoid as Monoid--import Fcf.Core (Eval, type (@@))-import Fcf.Combinators-import Fcf.Utils (Case, type (-->), Error)-import qualified Fcf.Utils as Case--import Fcf.Class.Bifunctor-import Fcf.Class.Foldable-import Fcf.Class.Monoid-import Fcf.Class.Ord--import Fcf.Data.Function-import Fcf.Data.List-import Fcf.Data.Nat (type (+))--type UnitPrefix = Case- [ 0 --> ""- , 1 --> "deci"- , 2 --> "hecto"- , 3 --> "kilo"- , 6 --> "mega"- , 9 --> "giga"- , Case.Any (Error @@ "Something Else")- ]---- Compile-time tests--_ = Refl :: Eval (UnitPrefix 0) :~: ""-_ = Refl :: Eval (UnitPrefix 3) :~: "kilo"---- * Class---- ** Ord--_ = Refl :: Eval (Compare '( '(), 0 ) '( '(), 1 )) :~: 'LT-_ = Refl :: Eval (Compare '( 1, 3 ) '( 1, 2 )) :~: 'GT-_ = Refl :: Eval (Compare ('Left '()) ('Right 'LT)) :~: 'LT-_ = Refl :: Eval (Compare ('Right 'EQ) ('Right 'EQ)) :~: 'EQ-_ = Refl :: Eval (Compare '[ 'LT, 'EQ, 'GT ] '[ 'LT, 'EQ, 'GT ]) :~: 'EQ-_ = Refl :: Eval (Compare 'True 'True) :~: 'EQ-_ = Refl :: Eval (Compare "A" "B") :~: 'LT--_ = Refl :: Eval (1 <= 1) :~: 'True-_ = Refl :: Eval (2 <= 1) :~: 'False-_ = Refl :: Eval (1 < 1) :~: 'False-_ = Refl :: Eval (1 < 2) :~: 'True-_ = Refl :: Eval (1 >= 1) :~: 'True-_ = Refl :: Eval (1 >= 2) :~: 'False-_ = Refl :: Eval (1 > 1) :~: 'False-_ = Refl :: Eval (2 > 1) :~: 'True---- ** Monoid--_ = Refl :: Eval ('( '(), '[ 'LT, 'EQ ]) .<> '( '(), '[ 'GT ])) :~: '( '(), '[ 'LT, 'EQ, 'GT ])-_ = Refl :: Eval ('Nothing .<> 'Just '[]) :~: 'Just '[]-_ = Refl :: Eval ('LT .<> 'GT) :~: 'LT-_ = Refl :: Eval ('EQ .<> 'GT) :~: 'GT-_ = Refl :: Eval ('Monoid.All 'True .<> 'Monoid.All 'False) :~: 'Monoid.All 'False-_ = Refl :: Eval ('Monoid.Any 'True .<> 'Monoid.Any 'False) :~: 'Monoid.Any 'True-#if __GLASGOW_HASKELL__ >= 802-_ = Refl :: Eval ("a" .<> MEmpty) :~: "a"-#endif---- ** Foldable--_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) '[ 'True, 'False ]) :~: 'Monoid.All 'False-_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) 'Nothing) :~: 'Monoid.All 'True-_ = Refl :: Eval (Foldr (.<>) 'LT '[ 'EQ, 'EQ ]) :~: 'LT-_ = Refl :: Eval (And '[ 'False, 'False ]) :~: 'False-_ = Refl :: Eval (Or '[ 'False, 'False ]) :~: 'False-_ = Refl :: Eval (Concat ('Right 'LT)) :~: 'LT--_ = Refl :: FoldMapDefault_ (Pure1 'Monoid.All) 'Nothing :~: 'Monoid.All 'True-_ = Refl :: FoldrDefault_ (.<>) 'LT '[ 'EQ, 'EQ ] :~: 'LT---- ** Functor--_ = Refl :: Eval (Bimap ((+) 1) (Pure2 '(:) '()) '(8, '[])) :~: '(9, '[ '()])-_ = Refl :: Eval (First ((+) 1) ('Left 8)) :~: 'Left 9-_ = Refl :: Eval (First ((+) 1) ('Right 0)) :~: 'Right 0-_ = Refl :: Eval (Second ((+) 1) ('Left 0)) :~: 'Left 0-_ = Refl :: Eval (Second ((+) 1) ('Right 8)) :~: 'Right 9---- ** Function--_ = Refl :: Eval (3 & Pure) :~: 3-_ = Refl :: Eval (((+) `On` Length) '[1,2,3] '[1,2]) :~: 5---- Dummy--main :: IO ()-main = pure ()+{-# LANGUAGE + CPP, + DataKinds, + KindSignatures, + TypeOperators #-} + +import Data.Type.Equality ((:~:)(Refl)) +import qualified Data.Monoid as Monoid + +import Fcf.Core (Eval, type (@@)) +import Fcf.Combinators +import Fcf.Utils (Assert, AssertNot, Case, type (-->), Error, ErrorMessage (Text), TypeError) +import qualified Fcf.Utils as Utils + +import Fcf.Class.Bifunctor +import Fcf.Class.Foldable +import Fcf.Class.Monoid +import Fcf.Class.Ord + +import Fcf.Data.Function +import Fcf.Data.List +import Fcf.Data.Nat (type (+)) + +type UnitPrefix = Case + [ 0 --> "" + , 1 --> "deci" + , 2 --> "hecto" + , 3 --> "kilo" + , 6 --> "mega" + , 9 --> "giga" + , Utils.Any (Error @@ "Something Else") + ] + +-- Compile-time tests + +_ = Refl :: Eval (UnitPrefix 0) :~: "" +_ = Refl :: Eval (UnitPrefix 3) :~: "kilo" + +-- * Class + +-- ** Ord + +_ = Refl :: Eval (Compare '( '(), 0 ) '( '(), 1 )) :~: 'LT +_ = Refl :: Eval (Compare '( 1, 3 ) '( 1, 2 )) :~: 'GT +_ = Refl :: Eval (Compare ('Left '()) ('Right 'LT)) :~: 'LT +_ = Refl :: Eval (Compare ('Right 'EQ) ('Right 'EQ)) :~: 'EQ +_ = Refl :: Eval (Compare '[ 'LT, 'EQ, 'GT ] '[ 'LT, 'EQ, 'GT ]) :~: 'EQ +_ = Refl :: Eval (Compare 'True 'True) :~: 'EQ +_ = Refl :: Eval (Compare "A" "B") :~: 'LT + +_ = Refl :: Eval (1 <= 1) :~: 'True +_ = Refl :: Eval (2 <= 1) :~: 'False +_ = Refl :: Eval (1 < 1) :~: 'False +_ = Refl :: Eval (1 < 2) :~: 'True +_ = Refl :: Eval (1 >= 1) :~: 'True +_ = Refl :: Eval (1 >= 2) :~: 'False +_ = Refl :: Eval (1 > 1) :~: 'False +_ = Refl :: Eval (2 > 1) :~: 'True + +-- ** Monoid + +_ = Refl :: Eval ('( '(), '[ 'LT, 'EQ ]) .<> '( '(), '[ 'GT ])) :~: '( '(), '[ 'LT, 'EQ, 'GT ]) +_ = Refl :: Eval ('Nothing .<> 'Just '[]) :~: 'Just '[] +_ = Refl :: Eval ('LT .<> 'GT) :~: 'LT +_ = Refl :: Eval ('EQ .<> 'GT) :~: 'GT +_ = Refl :: Eval ('Monoid.All 'True .<> 'Monoid.All 'False) :~: 'Monoid.All 'False +_ = Refl :: Eval ('Monoid.Any 'True .<> 'Monoid.Any 'False) :~: 'Monoid.Any 'True +#if __GLASGOW_HASKELL__ >= 802 +_ = Refl :: Eval ("a" .<> MEmpty) :~: "a" +#endif + +-- ** Foldable + +_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) '[ 'True, 'False ]) :~: 'Monoid.All 'False +_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) 'Nothing) :~: 'Monoid.All 'True +_ = Refl :: Eval (Foldr (.<>) 'LT '[ 'EQ, 'EQ ]) :~: 'LT +_ = Refl :: Eval (And '[ 'False, 'False ]) :~: 'False +_ = Refl :: Eval (Or '[ 'False, 'False ]) :~: 'False +_ = Refl :: Eval (Concat ('Right 'LT)) :~: 'LT + +_ = Refl :: FoldMapDefault_ (Pure1 'Monoid.All) 'Nothing :~: 'Monoid.All 'True +_ = Refl :: FoldrDefault_ (.<>) 'LT '[ 'EQ, 'EQ ] :~: 'LT + +-- ** Functor + +_ = Refl :: Eval (Bimap ((+) 1) (Pure2 '(:) '()) '(8, '[])) :~: '(9, '[ '()]) +_ = Refl :: Eval (First ((+) 1) ('Left 8)) :~: 'Left 9 +_ = Refl :: Eval (First ((+) 1) ('Right 0)) :~: 'Right 0 +_ = Refl :: Eval (Second ((+) 1) ('Left 0)) :~: 'Left 0 +_ = Refl :: Eval (Second ((+) 1) ('Right 8)) :~: 'Right 9 + +-- ** Function + +_ = Refl :: Eval (3 & Pure) :~: 3 +_ = Refl :: Eval (((+) `On` Length) '[1,2,3] '[1,2]) :~: 5 + +-- ** Asserts + +_ = Refl :: Eval (Pure Monoid.First >>= Assert ('Text "no error") (Pure True)) :~: Monoid.First +_ = Refl :: Eval (Pure Int >>= AssertNot ('Text "no error") (Pure False)) :~: Int +-- negative tests (asserts firing at compile time) are a challenge to test. tried, but omitted + +-- Dummy + +main :: IO () +main = pure ()