first-class-families 0.7.0.0 → 0.8.0.0

raw patch · 20 files changed

+1359/−309 lines, 20 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +26/−5
• README.md +57/−1
• first-class-families.cabal +9/−1
• src/Fcf.hs +2/−7
• src/Fcf/Class/Bifunctor.hs +65/−0
• src/Fcf/Class/Foldable.hs +233/−0
• src/Fcf/Class/Functor.hs +55/−0
• src/Fcf/Class/Monoid.hs +128/−0
• src/Fcf/Class/Monoid/Types.hs +38/−0
• src/Fcf/Class/Ord.hs +141/−0
• src/Fcf/Classes.hs +3/−56
• src/Fcf/Combinators.hs +2/−0
• src/Fcf/Data/Bool.hs +0/−37
• src/Fcf/Data/Common.hs +4/−4
• src/Fcf/Data/Function.hs +53/−0
• src/Fcf/Data/List.hs +406/−168
• src/Fcf/Data/Nat.hs +3/−0
• src/Fcf/Data/Symbol.hs +31/−0
• src/Fcf/Utils.hs +27/−13
• test/test.hs +76/−17

@@ -1,13 +1,34 @@+# 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`. (gspia)+  `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` and `(Fcf.Combinators.>>=)` (TheMatten)+- Add `Fcf.Utils.Case` and `(Fcf.Combinators.>>=)` (thanks to TheMatten) - Deprecate `Fcf.Bool.Guarded` - GHC 8.8 compatibility @@ -24,7 +45,7 @@  # 0.4.0.0 -- New functions (blmage)+- New functions (thanks to blmage)      + `LiftM`, `LiftM2`, `LiftM3`     + `(<=)`, `(>=)`, `(<)`, `(>)`@@ -36,11 +57,11 @@  # 0.3.0.0 -- More new functions, (isovector)+- More new functions, (thanks to isovector)  # 0.2.0.0 -- A whole bunch of basic functions (isovector)+- A whole bunch of basic functions (thanks to isovector) - Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`)  # 0.1.0.0

@@ -1,5 +1,21 @@ # First-class type families [![Hackage](https://img.shields.io/hackage/v/first-class-families.svg)](https://hackage.haskell.org/package/first-class-families) [![Build Status](https://travis-ci.org/Lysxia/first-class-families.svg)](https://travis-ci.org/Lysxia/first-class-families) +First-class type families are type-level functions that can be+composed using higher-order functions.++The core of the idea is an extensible kind of "type-level expressions"+and an open type family for evaluating such expressions.++```haskell+type Exp (k :: Type) :: Type+type family Eval (e :: Exp k) :: k+```++This library provides that core foundation,+and also exports basic first-class type families.++## Example+ For example, consider this simple type family:  ```haskell@@ -38,9 +54,49 @@     UndecidableInstances #-} ``` +## Overview++- `Fcf.Core`: definition of `Exp` and `Eval`.+- `Fcf.Combinators`: general combinators to compose first-class families.+- `Fcf.Data.*`: first-class families on common data types.+- `Fcf.Class.*`: overloaded first-class families.+- `Fcf.Utils`: miscellaneous.++The top-level module `Fcf` is a prelude to get acquainted with the library.+For regular use, import what you need from the specialized modules+above, preferably with explicit import lists.++```haskell+import Fcf                       -- Simple but fragile++import Fcf.Class.Functor (FMap)  -- Explicit and robust+```++## Features++### Overloaded type families++Value-level functions can be overloaded using type classes.+Type families---type-level functions---are open by design,+so overloading is as easy as just declaring them with more general types.++```haskell+data Map :: (a -> Exp b) -> f a -> Exp (f b)++-- Instances for f = []+type instance Eval (Map f '[]) = '[]+type instance Eval (Map f (x ': xs)) = Eval (f x) ': Eval (Map f xs)++-- Instances for f = Maybe+type instance Eval (Map f 'Nothing) = 'Nothing+type instance Eval (Map f ('Just x)) = 'Just (Eval (f x))+```+ ## See also -[Haskell with only one type family](http://blog.poisson.chat/posts/2018-08-06-one-type-family.html) (blogpost)+- [Haskell with only one type family](http://blog.poisson.chat/posts/2018-08-06-one-type-family.html)+- [Overloaded type families](https://blog.poisson.chat/posts/2018-09-29-overloaded-families.html)+- [The *singletons* library](https://hackage.haskell.org/package/singletons)  --- 

@@ -1,5 +1,5 @@ name:                first-class-families-version:             0.7.0.0+version:             0.8.0.0 synopsis:   First class type families description:@@ -28,9 +28,17 @@     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:     -- This upper bound is conservative.

@@ -104,12 +104,6 @@   , type (&&)   , Not -    -- *** Multi-way if--  , Guarded-  , Guard((:=))-  , Otherwise-     -- ** Case splitting    , Case@@ -152,5 +146,6 @@ import Fcf.Data.Common import Fcf.Data.List import Fcf.Data.Nat-import Fcf.Classes+import Fcf.Class.Functor+import Fcf.Class.Bifunctor import Fcf.Utils

@@ -0,0 +1,65 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Bifunctors.+--+-- Bifunctors are "two-argument functors".+--+-- This module is the type-level equivalent of "Data.Bifunctor".+module Fcf.Class.Bifunctor+  ( Bimap+  , First+  , Second+  ) where++import Fcf.Core (Exp, Eval)+import Fcf.Combinators (Pure)++-- $setup+-- >>> import Fcf.Combinators (Flip)+-- >>> import Fcf.Data.Nat (Nat, type (+), type (-))+-- >>> import Fcf.Data.Symbol (Symbol)++-- | Type-level 'Data.Bifunctor.bimap'.+--+-- >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))+-- Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)+-- = '(3, 3)+data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')++-- (,)+type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))++-- Either+type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))+type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))+++-- | Type-level 'Data.Bifunctor.first'.+-- Apply a function along the first parameter of a bifunctor.+--+-- === __Example__+--+-- >>> :kind! Eval (First ((+) 1) '(3,"a"))+-- Eval (First ((+) 1) '(3,"a")) :: (Nat, 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)++-- | Type-level 'Data.Bifunctor.second'.+-- Apply a function along the second parameter of a bifunctor.+--+-- This is generally equivalent to 'Data.Functor.Map'.+--+-- === __Example__+--+-- >>> :kind! Eval (Second ((+) 1) '("a",3))+-- Eval (Second ((+) 1) '("a",3)) :: (Symbol, Nat)+-- = '("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)

@@ -0,0 +1,233 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Foldable types.+--+-- A minimal implementation of this interface is given by either 'FoldMap' or+-- 'Foldr', but a default still needs to be given explicitly for the other.+--+-- @+-- data MyType a = ... {- Some custom Foldable type -}+--+-- -- Method 1: Implement Foldr, default FoldMap.+-- type instance 'Eval' ('Foldr' f y xs) = ... {- Explicit implementation -}+-- type instance 'Eval' ('FoldMap' f xs) = 'FoldMapDefault_' f xs {- Default -}+--+-- -- Method 2: Implement FoldMap, default Foldr.+-- type instance 'Eval' ('FoldMap' f xs) = ... {- Explicit implementation -}+-- type instance 'Eval' ('Foldr' f y xs) = 'FoldrDefault_' f y xs {- Default -}+-- @+module Fcf.Class.Foldable+  ( -- * Core interface+    Foldr+  , FoldMap++    -- ** Default implementations+  , FoldMapDefault_+  , FoldrDefault_++    -- * Derived operations++    -- ** Predicates+  , And+  , Or+  , All+  , Any++    -- ** Numbers+  , Sum++    -- ** Lists+  , Concat+  , ConcatMap+  ) where++import Fcf.Core (Exp, Eval)+import Fcf.Combinators (Pure, Pure1, type (<=<))+import Fcf.Data.Function (Bicomap)+import Fcf.Class.Monoid+import Fcf.Class.Monoid.Types (Endo(..), UnEndo)+import Fcf.Data.Bool (type (&&), type (||))+import Fcf.Data.Nat (Nat, type (+))++-- $setup+-- >>> import Fcf.Combinators (Flip)+-- >>> import Fcf.Class.Ord (type (<))++-- | Type-level 'Data.Foldable.foldMap'.+data FoldMap :: (a -> Exp m) -> t a -> Exp m++-- List+type instance Eval (FoldMap f '[]) = MEmpty+type instance Eval (FoldMap f (x ': xs)) = Eval (f x) <> Eval (FoldMap f xs)++-- Maybe+type instance Eval (FoldMap f 'Nothing) = MEmpty+type instance Eval (FoldMap f ('Just x)) = Eval (f x)++-- Either+type instance Eval (FoldMap f ('Left _a)) = MEmpty+type instance Eval (FoldMap f ('Right x)) = Eval (f x)++-- | Default implementation of 'FoldMap'.+--+-- === __Usage__+--+-- To define an instance of 'FoldMap' for a custom @MyType@ for which you already have+-- an instance of 'Foldr':+--+-- @+-- type instance 'Eval' ('FoldMap' f (xs :: MyType a)) = 'FoldMapDefault_' f xs+-- @+--+-- ==== __Example__+--+-- >>> :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'.+--+-- === __Usage__+--+-- To define an instance of 'Foldr' for a custom @MyType@ for which you already+-- have an instance of 'FoldMap':+--+-- @+-- type instance 'Eval' ('Foldr' f y (xs :: MyType a)) = 'FoldrDefault_' f y xs+-- @+--+-- ==== __Example__+--+-- >>> :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+-- = 10+data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b++-- List+type instance Eval (Foldr f y '[]) = y+type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))++-- Maybe+type instance Eval (Foldr f y 'Nothing) = y+type instance Eval (Foldr f y ('Just x)) = Eval (f x y)++-- Either+type instance Eval (Foldr f y ('Left _a)) = y+type instance Eval (Foldr f y ('Right x)) = Eval (f x y)++-- * Derived operations++-- | Give @True@ if all of the booleans in the list are @True@.+--+-- === __Example__+--+-- >>> :kind! Eval (And '[ 'True, 'True])+-- Eval (And '[ 'True, 'True]) :: Bool+-- = 'True+--+-- >>> :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)++-- | Whether all elements of the list satisfy a predicate.+--+-- Note: this identifier conflicts with 'Data.Monoid.All' (from "Data.Monoid").+--+-- === __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 (<) 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)+++-- | Give @True@ if any of the booleans in the list are @True@.+--+-- === __Example__+--+-- >>> :kind! Eval (Or '[ 'True, 'True])+-- Eval (Or '[ 'True, 'True]) :: Bool+-- = 'True+--+-- >>> :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)+++-- | Whether any element of the list satisfies a predicate.+--+-- Note: this identifier conflicts with 'Fcf.Utils.Any' (from "Fcf.Utils"),+-- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").+--+-- === __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 (<) 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)+++-- | Sum a @Nat@-list.+--+-- === __Example__+--+-- >>> :kind! Eval (Sum '[1,2,3])+-- Eval (Sum '[1,2,3]) :: Nat+-- = 6+data Sum :: t Nat -> Exp Nat+type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)+++-- | Concatenate a collection of elements from a monoid.+--+-- === __Example__+--+-- For example, fold a list of lists.+--+-- > 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]+--+data Concat :: t m -> Exp m+type instance Eval (Concat xs) = Eval (FoldMap Pure xs)++-- | Map a function and concatenate the results.+--+-- This is 'FoldMap' specialized to the list monoid.+data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]+type instance Eval (ConcatMap f xs) = Eval (FoldMap f xs)

@@ -0,0 +1,55 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++module Fcf.Class.Functor+  ( Map+  , FMap+  ) where++import Fcf.Core (Exp, Eval)++-- | Type-level 'fmap' for type-level functors.+--+-- Note: this name clashes with 'Data.Map.Lazy.Map' from /containers/.+-- 'FMap' is provided as a synonym to avoid this.+--+-- === __Example__+--+-- >>> import Fcf.Data.Nat+-- >>> import qualified GHC.TypeLits as TL+-- >>> 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]+data Map :: (a -> Exp b) -> f a -> Exp (f b)++-- | Synonym of 'Map' to avoid name clashes.+type FMap = Map++-- []+type instance Eval (Map f '[]) = '[]+type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)++-- Maybe+type instance Eval (Map f 'Nothing) = 'Nothing+type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))++-- Either+type instance Eval (Map f ('Left x)) = 'Left x+type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))++-- Tuples+type instance Eval (Map f '(x, a)) =+  '(x, Eval (f a))+type instance Eval (Map f '(x, y, a)) =+  '(x, y, Eval (f a))+type instance Eval (Map f '(x, y, z, a)) =+  '(x, y, z, Eval (f a))+type instance Eval (Map f '(x, y, z, w, a)) =+  '(x, y, z, w, Eval (f a))

@@ -0,0 +1,128 @@+{-# LANGUAGE+    CPP,+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Semigroups and monoids.+module Fcf.Class.Monoid+  ( -- * Pure type families+    -- | Nicer to use when applied explicitly.+    type (<>)+  , MEmpty++    -- * First-class families+    -- | Can be composed and passed to higher-order functions.+  , type (.<>)+  , MEmpty_+  ) where++import Fcf.Core (Exp, Eval)+import Data.Monoid (All(..), Any(..))+import Data.Type.Bool (type (&&), type (||))++#if __GLASGOW_HASKELL__ >= 802+import GHC.TypeLits (AppendSymbol)+#endif++-- $setup+-- >>> import GHC.TypeLits (Nat)++-- | Type-level semigroup composition @('Data.Semigroup.<>')@.+--+-- This is the fcf-encoding of @('<>')@.+-- To define a new semigroup, add type instances to @('<>')@.+data (.<>) :: a -> a -> Exp a+type instance Eval (x .<> y) = x <> y++-- | Type-level semigroup composition @('Data.Semigroup.<>')@.+type family (<>) (x :: a) (y :: a) :: a++-- (,)+type instance (<>) '(a1, a2) '(b1, b2) = '(a1 <> b1, a2 <> b2)++-- (,,)+type instance (<>) '(a1, a2, a3) '(b1, b2, b3) = '(a1 <> b1, a2 <> b2, a3 <> b3)++-- List+type instance (<>) '[] ys = ys+type instance (<>) (x ': xs) ys = x ': (<>) xs ys++-- Maybe+type instance (<>) 'Nothing b = b+type instance (<>) a 'Nothing = a+type instance (<>) ('Just a) ('Just b) = 'Just (a <> b)++-- Ordering+type instance (<>) 'EQ b = b+type instance (<>) a 'EQ = a+type instance (<>) 'LT _b = 'LT+type instance (<>) 'GT _b = 'GT++-- ()+type instance (<>) _a _b = '()++-- All+type instance (<>) ('All a) ('All b) = 'All (a && b)++-- Any+type instance (<>) ('Any a) ('Any b) = 'Any (a || b)++#if __GLASGOW_HASKELL__ >= 802+-- Symbol+-- | With /base >= 4.10.0.0/.+type instance (<>) x y = AppendSymbol x y+#endif++-- | Type-level monoid identity 'Data.Monoid.mempty'.+--+-- This is the fcf-encoding of 'MEmpty'.+data MEmpty_ :: Exp a+type instance Eval MEmpty_ = MEmpty++-- | Type-level monoid identity 'Data.Monoid.mempty'.+--+-- === __Examples__+--+-- >>> :kind! 'LT <> MEmpty+-- 'LT <> MEmpty :: Ordering+-- = 'LT+--+-- >>> :kind! MEmpty <> '( 'EQ, '[1, 2])+-- MEmpty <> '( 'EQ, '[1, 2]) :: (Ordering, [Nat])+-- = '( 'EQ, '[1, 2])+--+-- >>> :kind! '( 'GT, 'Just '()) <> MEmpty+-- '( 'GT, 'Just '()) <> MEmpty :: (Ordering, Maybe ())+-- = '( 'GT, 'Just '())+type family MEmpty :: a++-- (,)+type instance MEmpty = '(MEmpty, MEmpty)++-- (,,)+type instance MEmpty = '(MEmpty, MEmpty, MEmpty)++-- List+type instance MEmpty = '[]++-- Maybe+type instance MEmpty = 'Nothing++-- Ordering+type instance MEmpty = 'EQ++-- ()+type instance MEmpty = '()++-- All+type instance MEmpty = 'All 'True++-- Any+type instance MEmpty = 'Any 'False++-- Symbol+type instance MEmpty = ""

@@ -0,0 +1,38 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Carriers of useful monoid instances.+module Fcf.Class.Monoid.Types+  ( -- * Endo+    Endo(..)+  , UnEndo+  ) where++import Fcf.Core (Exp)+import Fcf.Combinators (Pure, type (<=<))+import Fcf.Class.Monoid++-- | Endofunctions.+--+-- === __Details__+--+-- This is is used in the default implementation of+-- 'Fcf.Class.Foldable.Foldr' in terms of+-- 'Fcf.Class.Foldable.FoldMap'.+newtype Endo a = Endo (a -> Exp a)++-- | Inverse of the 'Endo' constructor.+type family UnEndo (e :: Endo a) :: a -> Exp a where+  UnEndo ('Endo f) = f++-- * Endo as a monoid+--+-- Note it is only a monoid up to 'Eval'.++type instance 'Endo f <> 'Endo g = 'Endo (f <=< g)+type instance MEmpty = 'Endo Pure

@@ -0,0 +1,141 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Equality and ordering.+--+-- Note that equality doesn't really require a class,+-- it can be defined uniformly as 'TyEq'.+module Fcf.Class.Ord+  ( -- * Order+    Compare+  , type (<=)+  , type (>=)+  , type (<)+  , type (>)++    -- * Equality+  , TyEq+  ) where++import qualified GHC.TypeLits as TL++import Fcf.Core+import Fcf.Class.Monoid (type (<>))  -- Semigroup Ordering+import Fcf.Data.Bool (Not)+import Fcf.Utils (TyEq)++-- | Type-level 'compare' for totally ordered data types.+--+-- === __Example__+--+-- >>> :kind! Eval (Compare "a" "b")+-- Eval (Compare "a" "b") :: Ordering+-- = 'LT+--+-- >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])+-- Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering+-- = 'EQ+--+-- >>> :kind! Eval (Compare '[1, 3] '[1, 2])+-- Eval (Compare '[1, 3] '[1, 2]) :: Ordering+-- = 'GT+data Compare :: a -> a -> Exp Ordering++-- (,)+type instance Eval (Compare '(a1, a2) '(b1, b2)) = Eval (Compare a1 b1) <> Eval (Compare a2 b2)++-- (,,)+type instance Eval (Compare '(a1, a2, a3) '(b1, b2, b3))+  = Eval (Compare a1 b1) <> Eval (Compare a2 b2) <> Eval (Compare a3 b3)++-- Either+type instance Eval (Compare ('Left a) ('Left b)) = Eval (Compare a b)+type instance Eval (Compare ('Right a) ('Right b)) = Eval (Compare a b)+type instance Eval (Compare ('Left _a) ('Right _b)) = 'LT+type instance Eval (Compare ('Right _a) ('Left _b)) = 'GT++-- Maybe+type instance Eval (Compare 'Nothing 'Nothing) = 'EQ+type instance Eval (Compare ('Just a) ('Just b)) = Eval (Compare a b)+type instance Eval (Compare 'Nothing ('Just _b)) = 'LT+type instance Eval (Compare ('Just _a) 'Nothing) = 'GT++-- List+type instance Eval (Compare '[] '[]) = 'EQ+type instance Eval (Compare (x ': xs) (y ': ys)) = Eval (Compare x y) <> Eval (Compare xs ys)+type instance Eval (Compare '[] (_y ': _ys)) = 'LT+type instance Eval (Compare (_x ': _xs) '[]) = 'GT++-- Bool+type instance Eval (Compare (a :: Bool) a) = 'EQ+type instance Eval (Compare 'False 'True) = 'GT+type instance Eval (Compare 'True 'False) = 'GT++-- Ordering+type instance Eval (Compare (a :: Ordering) a) = 'EQ+type instance Eval (Compare 'LT 'EQ) = 'LT+type instance Eval (Compare 'LT 'GT) = 'LT+type instance Eval (Compare 'EQ 'GT) = 'LT+type instance Eval (Compare 'EQ 'LT) = 'GT+type instance Eval (Compare 'GT 'LT) = 'GT+type instance Eval (Compare 'GT 'EQ) = 'GT++-- Symbol+type instance Eval (Compare a b) = TL.CmpSymbol a b++-- Nat+type instance Eval (Compare a b) = TL.CmpNat a b++-- ()+type instance Eval (Compare (a :: ()) b) = 'EQ++-- * Derived operations++-- Asymmetric comparison operators @Exp a -> a -> Bool@.+type a ~== b = Eval (TyEq (Eval a) b)+type a ~/= b = Eval (Not (a ~== b))++-- | "Smaller than or equal to". Type-level version of @('<=')@.+--+-- === __Example__+--+-- >>> :kind! Eval ("b" <= "a")+-- Eval ("b" <= "a") :: Bool+-- = 'False+data (<=) :: a -> a -> Exp Bool+type instance Eval ((<=) a b) = Compare a b ~/= 'GT++-- | "Greater than or equal to". Type-level version of @('>=')@.+--+-- === __Example__+--+-- >>> :kind! Eval ("b" >= "a")+-- Eval ("b" >= "a") :: Bool+-- = 'True+data (>=) :: a -> a -> Exp Bool+type instance Eval ((>=) a b) = Compare a b ~/= 'LT++-- | "Smaller than". Type-level version of @('<')@.+--+-- === __Example__+--+-- >>> :kind! Eval ("a" < "b")+-- Eval ("a" < "b") :: Bool+-- = 'True+data (<) :: a -> a -> Exp Bool+type instance Eval ((<) a b) = Compare a b ~== 'LT++-- | "Greater than". Type-level version of @('>')@.+--+-- === __Example__+--+-- >>> :kind! Eval ("b" > "a")+-- Eval ("b" > "a") :: Bool+-- = 'True+data (>) :: a -> a -> Exp Bool+type instance Eval ((>) a b) = Compare a b ~== 'GT

@@ -1,65 +1,12 @@ {-# LANGUAGE-    DataKinds,-    PolyKinds,-    TypeFamilies,-    TypeInType,     TypeOperators #-}  -- | Overloaded functions. module Fcf.Classes+  {-# DEPRECATED "Use Fcf.Class.Functor or Fcf.Class.Bifunctor instead." #-}   ( Map   , Bimap   ) where --import Fcf.Core----- $--- >>> import Fcf.Core----- | Type-level 'fmap' for type-level functors.------ === __Example__------ >>> import Fcf.Data.Nat--- >>> import qualified GHC.TypeLits as TL--- >>> 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]-data Map :: (a -> Exp b) -> f a -> Exp (f b)---- []-type instance Eval (Map f '[]) = '[]-type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)---- Maybe-type instance Eval (Map f 'Nothing) = 'Nothing-type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))---- Either-type instance Eval (Map f ('Left x)) = 'Left x-type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))---- Tuples-type instance Eval (Map f '(x, a)) =-  '(x, Eval (f a))-type instance Eval (Map f '(x, y, a)) =-  '(x, y, Eval (f a))-type instance Eval (Map f '(x, y, z, a)) =-  '(x, y, z, Eval (f a))-type instance Eval (Map f '(x, y, z, w, a)) =-  '(x, y, z, w, Eval (f a))---- | Type-level 'Data.Bifunctor.bimap'.-data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')---- (,)-type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))---- Either-type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))-type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))+import Fcf.Class.Functor+import Fcf.Class.Bifunctor

@@ -7,6 +7,8 @@     UndecidableInstances #-}  -- | General fcf combinators.+--+-- See also "Fcf.Data.Function" for more. module Fcf.Combinators   ( Pure   , Pure1

@@ -15,17 +15,9 @@   , type (||)   , type (&&)   , Not--    -- *** Multi-way if--  , Guarded-  , Guard((:=))-  , Otherwise   ) where  import Fcf.Core-import Fcf.Combinators (ConstFn)-import Fcf.Utils  -- | N.B.: The order of the two branches is the opposite of "if": -- @UnBool ifFalse ifTrue bool@.@@ -58,32 +50,3 @@ data Not :: Bool -> Exp Bool type instance Eval (Not 'True)  = 'False type instance Eval (Not 'False) = 'True---- | A conditional choosing the first branch whose guard @a -> 'Exp' 'Bool'@--- accepts a given value @a@.------ === Example------ @--- type UnitPrefix n = 'Eval' ('Guarded' n---   '[ 'TyEq' 0 \'':=' 'Pure' \"\"---    , 'TyEq' 1 \'':=' 'Pure' \"deci\"---    , 'TyEq' 2 \'':=' 'Pure' \"hecto\"---    , 'TyEq' 3 \'':=' 'Pure' \"kilo\"---    , 'TyEq' 6 \'':=' 'Pure' \"mega\"---    , 'TyEq' 9 \'':=' 'Pure' \"giga\"---    , 'Otherwise' \'':=' 'Error' "Something else"---    ])--- @-data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b-type instance Eval (Guarded x ((p ':= y) ': ys)) =-    Eval (If (Eval (p x)) y (Guarded x ys))-{-# DEPRECATED Guarded "Use 'Case' instead" #-}---- | A fancy-looking pair type to use with 'Guarded'.-data Guard a b = a := b-infixr 0 :=---- | A catch-all guard for 'Guarded'.-type Otherwise = ConstFn 'True-

@@ -8,20 +8,17 @@ -- | Common data types: tuples, 'Either', 'Maybe'. module Fcf.Data.Common   ( -- ** Pairs-     Uncurry   , Fst   , Snd   , type (***)      -- ** Either-   , UnEither   , IsLeft   , IsRight      -- ** Maybe-   , UnMaybe   , FromMaybe   , IsNothing@@ -41,12 +38,14 @@ data Snd :: (a, b) -> Exp b type instance Eval (Snd '(_a, b)) = b + infixr 3 *** --- | Equivalent to 'Bimap' for pairs.+-- | Specialization of 'Fcf.Class.Bifunctor.Bimap' for pairs. data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c') type instance Eval ((***) f f' '(b, b')) = '(Eval (f b), Eval (f' b')) + -- ** Either  data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c@@ -60,6 +59,7 @@ data IsRight :: Either a b -> Exp Bool type instance Eval (IsRight ('Left _a)) = 'False type instance Eval (IsRight ('Right _a)) = 'True+  -- ** Maybe 

@@ -0,0 +1,53 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Simple combinators for functions.+module Fcf.Data.Function+  ( type (&)+  , On+  , Bicomap+  ) where++import Fcf.Core++infixl 1 &++-- $setup+-- >>> import Fcf.Combinators (Pure)+-- >>> import Fcf.Data.Common (Fst)+-- >>> import Fcf.Data.Bool (type (&&), type (||))++-- | Reverse function application, argument first.+--+-- === __Example__+--+-- >>> :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)++-- | Lift a binary function to the domain of a projection.+--+-- === __Example__+--+-- >>> :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)))++-- | Pre-compose a binary function with a function for each argument.+--+-- === __Example__+--+-- >>> :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)))

@@ -7,57 +7,130 @@     UndecidableInstances #-}  -- | Lists.+--+-- See also "Fcf.Class.Foldable" for additional functions. module Fcf.Data.List-  ( Foldr-  , Unfoldr-  , UnList-  , Cons-  , type (++)-  , Concat-  , ConcatMap-  , Filter+  ( -- * 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-  , Find-  , FindIndex++  -- * 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-  , Cons2-  , Take-  , Drop-  , TakeWhile-  , DropWhile-  , Reverse   ) where  import qualified GHC.TypeLits as TL  import Fcf.Core import Fcf.Combinators-import Fcf.Classes+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+import Fcf.Utils (If, TyEq) --- $+-- $setup -- >>> import Fcf.Core -- >>> import Fcf.Combinators -- >>> import qualified GHC.TypeLits as TL  --- | Append an element for type-level lists.+-- | List catenation. -- -- === __Example__ --+-- >>> :kind! Eval ('[1, 2] ++ '[3, 4])+-- Eval ('[1, 2] ++ '[3, 4]) :: [Nat]+-- = '[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]) :: [Nat] -- = '[1, 2, 3]@@ -68,28 +141,76 @@ data Cons :: a -> [a] -> Exp [a] type instance Eval (Cons a as) = a ': as --- | Foldr for type-level lists.+-- | 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 (Foldr (+) 0 '[1, 2, 3, 4])--- Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat--- = 10-data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b-type instance Eval (Foldr f y '[]) = y-type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))+-- >>> :kind! Eval (Snoc '[1,2,3] 4)+-- Eval (Snoc '[1,2,3] 4) :: [Nat]+-- = '[1, 2, 3, 4]+data Snoc :: [a] -> a -> Exp [a]+type instance Eval (Snoc lst a) = Eval (lst ++ '[a]) --- | N.B.: This is equivalent to a 'Foldr' flipped.++-- 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]) :: [Nat]+-- = '[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]) :: [Nat]+-- = '[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) = '[] --- | Type-level Unfoldr.+-- | Unfold a generator into a list. -- -- === __Example__ --@@ -109,70 +230,7 @@ data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a] type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c)) --- | Type-level list catenation.------ === __Example__------ >>> :kind! Eval ('[1, 2] ++ '[3, 4])--- Eval ('[1, 2] ++ '[3, 4]) :: [Nat]--- = '[1, 2, 3, 4]----data (++) :: [a] -> [a] -> Exp [a]-type instance Eval ((++) '[] ys) = ys-type instance Eval ((++) (x ': xs) ys) = x ': Eval ((++) xs ys) --- | Concat for lists.------ === __Example__------ >>> :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]----data Concat :: [[a]] -> Exp [a]-type instance Eval (Concat lsts) = Eval (Foldr (++) '[] lsts)---- | ConcatMap for lists.-data ConcatMap :: (a -> Exp [b]) -> [a] -> Exp [b]-type instance Eval (ConcatMap f lst) = Eval (Concat (Eval (Map f lst)))--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))--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)- -- Helper for the Replicate. data NumIter :: a -> Nat -> Exp (Maybe (a, Nat)) type instance Eval (NumIter a s) =@@ -180,8 +238,7 @@     ('Just '(a, s TL.- 1))     'Nothing ---- | Type-level `Replicate` for lists.+-- | Repeat the same element in a list. -- -- === __Example__ --@@ -191,68 +248,8 @@ data Replicate :: Nat -> a -> Exp [a] type instance Eval (Replicate n a) = Eval (Unfoldr (NumIter a) n) -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)) --- | Find the index of an element satisfying the predicate.-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))---- | Type-level `Elem` for lists.------ === __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.-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))---- | Modify an element at a given index.------ The list is unchanged if the index is out of bounds.-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--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))--data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])-type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)----- | Type-level list take.+-- | Take a prefix of fixed length. -- -- === __Example__ --@@ -267,7 +264,7 @@   Take_ _ '[]       = '[]   Take_ n (x ': xs) = x ': Take_ (n TL.- 1) xs --- | Type-level list drop.+-- | Drop a prefix of fixed length, evaluate to the remaining suffix. -- -- === __Example__ --@@ -282,7 +279,7 @@   Drop_ _ '[]       = '[]   Drop_ n (x ': xs) = Drop_ (n TL.- 1) xs --- | Type-level list takeWhile.+-- | Take the longest prefix of elements satisfying a predicate. -- -- === __Example__ --@@ -296,7 +293,8 @@       ('(:) x <$> TakeWhile p xs)       (Pure '[])) --- | Type-level list dropWhile.+-- | Drop the longest prefix of elements satisfying a predicate,+-- evaluate to the remaining suffix. -- -- === __Example__ --@@ -311,19 +309,259 @@       (Pure (x ': xs)))  --- 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))+-- | '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,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 (<) 9) '[1,2,3])+-- Eval (Span (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])+-- = '( '[1, 2, 3], '[])+--+-- >>> :kind! Eval (Span (Flip (<) 0) '[1,2,3])+-- Eval (Span (Flip (<) 0) '[1,2,3]) :: ([Nat], [Nat])+-- = '( '[], '[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))  --- | Type-level list reverse.+-- | '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 (Reverse '[1,2,3,4,5])--- Eval (Reverse '[1,2,3,4,5]) :: [Nat]--- = '[5, 4, 3, 2, 1]-data Reverse :: [a] -> Exp [a]-type instance Eval (Reverse l) = Eval (Rev l '[])+-- >>> :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 (<) 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]) :: ([Nat], [Nat])+-- = '( '[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]) :: [[Nat]]+-- = '[ '[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 (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 (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 (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+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 Nat+-- = 'Nothing+--+-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3,0])+-- Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat+-- = '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]) :: [Nat]+-- = '[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]) :: ([Nat], [Nat])+-- = '( '[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 Nat+-- = 'Just 2+--+-- >>> :kind! Eval (FindIndex ((>) 0) '[1,2,3,1,2,3])+-- Eval (FindIndex ((>) 0) '[1,2,3,1,2,3]) :: Maybe Nat+-- = '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]) :: [Nat]+-- = '[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]) :: [Nat]+-- = '[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))

@@ -27,6 +27,9 @@   , type (-)   , type (Fcf.Data.Nat.*)   , type (^)++    -- * Comparisons+    -- | Note that these conflict with "Fcf.Class.Ord".   , type (<=)   , type (>=)   , type (<)

@@ -0,0 +1,31 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# OPTIONS_GHC -Wall                       #-}+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}++{-|+Module      : Fcf.Data.Symbol+Description : Type-level strings++= Symbols++Type-level strings.++Note that the operators from this module conflict with "GHC.TypeLits".++'Symbol' also has instances of @('Fcf.Class.Monoid.<>')@ and 'Fcf.Class.Monoid.MEmpty'.++-}+module Fcf.Data.Symbol+    ( -- * Type of symbols+      -- | From "GHC.TypeLits".++      Symbol+    )+  where++import           GHC.TypeLits (Symbol)

@@ -33,6 +33,7 @@ import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))  import Fcf.Core+import Fcf.Combinators (Pure)  -- | Type-level 'error'. data Error :: Symbol -> Exp a@@ -48,10 +49,19 @@ 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 :: k) :: Bool where+type family TyEqImpl (a :: k) (b :: l) :: Bool where   TyEqImpl a a = 'True   TyEqImpl a b = 'False @@ -81,28 +91,27 @@ -- to subcomputation ('Else'). Examples: -- -- @--- type BoolToNat = Case---   [ 'True  --> 0---   , 'False --> 1+-- type BoolToNat = 'Case'+--   [ 'True  '-->' 0+--   , 'False '-->' 1 --   ] ----- type NatToBool = Case---   [ 0 --> 'False---   , Any   'True+-- type NatToBool = 'Case'+--   [ 0 '-->' 'False+--   , 'Any'   'True --   ] ----- type ZeroOneOrSucc = Case---   [ 0  --> 0---   , 1  --> 1---   , Else   ((+) 1)+-- 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 : _ ) a = b-  Case_ ('Match_ _ _ : ms) a = Case_ ms a+  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)@@ -116,6 +125,11 @@ 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

@@ -1,39 +1,98 @@ {-# LANGUAGE+    CPP,     DataKinds,     KindSignatures,     TypeOperators #-}  import Data.Type.Equality ((:~:)(Refl))-import GHC.TypeLits (Nat)-import Fcf+import qualified Data.Monoid as Monoid -type UnitPrefix (n :: Nat) = Eval (Guarded n-  [ TyEq 0 ':= Pure ""-  , TyEq 1 ':= Pure "deci"-  , TyEq 2 ':= Pure "hecto"-  , TyEq 3 ':= Pure "kilo"-  , TyEq 6 ':= Pure "mega"-  , TyEq 9 ':= Pure "giga"-  , Otherwise ':= Error "Something else"-  ])+import Fcf.Core (Eval, type (@@))+import Fcf.Combinators+import Fcf.Utils (Case, type (-->), Error)+import qualified Fcf.Utils as Case -type UnitPrefix' = 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"-  , Any   (Error @@ "Something Else")+  , Case.Any   (Error @@ "Something Else")   ]  -- Compile-time tests -_ = Refl :: UnitPrefix 0 :~: ""-_ = Refl :: UnitPrefix 9 :~: "giga"+_ = Refl :: Eval (UnitPrefix 0) :~: ""+_ = Refl :: Eval (UnitPrefix 3) :~: "kilo" -_ = 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