packages feed

defun-core (empty) → 0.1

raw patch · 7 files changed

+859/−0 lines, 7 filesdep +base

Dependencies added: base

Files

+ CHANGELOG.md view
@@ -0,0 +1,3 @@+## 0.1++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2023, Oleg Grenrus++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Oleg Grenrus nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ defun-core.cabal view
@@ -0,0 +1,65 @@+cabal-version:   2.4+name:            defun-core+version:         0.1+license:         BSD-3-Clause+license-file:    LICENSE+author:          Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:      Oleg Grenrus <oleg.grenrus@iki.fi>+category:        Data+build-type:      Simple+extra-doc-files: CHANGELOG.md+tested-with:     GHC ==9.2.8 || ==9.4.8 || ==9.6.3 || ==9.8.1+synopsis:        Defunctionalization helpers: core definitions+description:+  The package @defun@ provides defunctionalization helpers, most importantly+  type family 'DeFun.Core.App' allowing to write higher-order type families.+  The @singletons@ package also has its own type family @Apply@,+  but the machinery is tied to the @Sing@ / singletons.+  .+  In particular, the @Lam@ counterpart @SLambda@ is specialized to @Sing@ arguments.+  The @defun@'s @Lam@ is however fully general, so you can use your own singletons+  or (importantly) singleton-like arguments.+  .+  The package provides few defunctionalized functions, and their term-level+  variants can be found in @defun-bool@ and @defun-sop@ packages,+  which use @SBool@ and @NP@ data types from @singletons-bool@ and @sop-core@+  packages respectively.++source-repository head+  type:     git+  location: https://github.com/phadej/defun.git+  subdir:   defun-core++common language+  default-language:   Haskell2010+  default-extensions:+    DataKinds+    EmptyCase+    GADTs+    KindSignatures+    NoImplicitPrelude+    PatternSynonyms+    PolyKinds+    RankNTypes+    ScopedTypeVariables+    StandaloneKindSignatures+    TypeApplications+    TypeFamilies+    TypeOperators+    UndecidableInstances+    ViewPatterns++library+  import:                   language+  hs-source-dirs:           src+  exposed-modules:+    DeFun.Bool+    DeFun.Core+    DeFun.Function+    DeFun.List++  build-depends:+    , base            ^>=4.16.3.0 || ^>=4.17.2.0 || ^>=4.18.0.0 || ^>=4.19.0.0++  x-docspec-extra-packages: defun singleton-bool sop-core+  x-docspec-options:        -XDataKinds -XGADTs -XStandaloneDeriving
+ src/DeFun/Bool.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE Trustworthy #-}+-- | Boolean functions.+--+-- Type families are defined in "Data.Type.Bool" module in @base@ package.+-- For term-level reflections see [defun-bool package](https://hackage.haskell.org/package/defun-bool).+--+module DeFun.Bool (+    -- * Logical and+    LAnd, LAndSym, LAndSym1,+    -- * Logical or+    LOr, LOrSym, LOrSym1,+    -- * Logical not+    Not, NotSym,+) where++import Data.Type.Bool (Not, type (&&), type (||))+import Prelude        (Bool)++import DeFun.Core++-------------------------------------------------------------------------------+-- LAnd+-------------------------------------------------------------------------------++-- | Logical and. A synonym of 'Data.Type.Bool.&&'+type LAnd :: Bool -> Bool -> Bool+type LAnd x y = x && y++type LAndSym :: Bool ~> Bool ~> Bool+data LAndSym x+type instance App LAndSym x = LAndSym1 x++type LAndSym1 :: Bool -> Bool ~> Bool+data LAndSym1 x y+type instance App (LAndSym1 x) y = LAnd x y++-------------------------------------------------------------------------------+-- LOr+-------------------------------------------------------------------------------++-- | Logical or. A synonym of 'Data.Type.Bool.||'+type LOr :: Bool -> Bool -> Bool+type LOr x y = x || y++type LOrSym :: Bool ~> Bool ~> Bool+data LOrSym x+type instance App LOrSym x = LOrSym1 x++type LOrSym1 :: Bool -> Bool ~> Bool+data LOrSym1 x y+type instance App (LOrSym1 x) y = LOr x y++-------------------------------------------------------------------------------+-- Not+-------------------------------------------------------------------------------++-- | Logical not.+type NotSym :: Bool ~> Bool+data NotSym x+type instance App NotSym x = Not x
+ src/DeFun/Core.hs view
@@ -0,0 +1,178 @@+{-# LANGUAGE Trustworthy #-}+-- | Defunctorization core primitives.+module DeFun.Core where++import Data.Kind (Type)++-- $setup+-- >>> import Prelude (Show)+-- >>> import Data.SOP.NP (NP (..))+-- >>> import DeFun++-------------------------------------------------------------------------------+-- * FunKind+-------------------------------------------------------------------------------++-- | A kind for type-level functions. +type FunKind :: Type -> Type -> Type+data FunKind :: Type -> Type -> Type++-------------------------------------------------------------------------------+-- * Fun+-------------------------------------------------------------------------------++-- | Something of kind @'Fun' a b@ (or @a '~>' b@) is a defunctionalized type function.+--+-- Normal type arrows @(->)@ can be converted into defunctionalized arrows @('~>')@ by use of 'Con1', 'Con2' ... family of types.+--+type Fun a b = FunKind a b -> Type++-- implementation note: defunctionalized symbols would be nicer+-- if defined as constructors of open data kind.+-- But GHC doesn't have such functionality yet:+-- https://gitlab.haskell.org/ghc/ghc/-/issues/11080++-- | An infix synonmy for 'Fun'.+type (~>) a b = Fun a b+infixr 0 ~>++-------------------------------------------------------------------------------+-- * App+-------------------------------------------------------------------------------++-- | Type level function application.+type family App (f :: a ~> b) (x :: a) :: b++-- | An infix synonym for 'App'.+--+-- Note: there is a term version which is a synonym to 'appLam'.+type (@@) a b = App a b+infixl 9 @@++-------------------------------------------------------------------------------+-- * Lam+-------------------------------------------------------------------------------++-- | A term-level representation of defunctionalized type function.+--+-- If the @a@ and @b@ type arguments are singletons,+-- then @'Lam' a b@ itself will be a singleton of the defunctionalized type function,+-- but in general it may not be.+-- (c.f @'Data.SOP.NP.NP' Sing@ is a list singleton, but @NP@ is more general).+--+type Lam :: (a -> Type) -> (b -> Type) -> (a ~> b) -> Type+newtype Lam a b f = Lam { appLam :: LamRep a b f }++-- | An infix synonym for 'Lam'+type a :~> b = Lam a b+infixr 0 :~>++-- | A constructor of 'Lam'+mkLam :: LamRep a b f -> Lam a b f+mkLam = Lam++-- | Unwrapped representation of defunctionalized type function.+type LamRep :: (a -> Type) -> (b -> Type) -> (a ~> b) -> Type+type LamRep a b fun = forall x. a x -> b (fun @@ x)++-- | An infix synonym for 'appLam'.+--+-- Note: there is a type version which is a synonym to 'App'.+(@@) :: Lam a b f -> a x -> b (f @@ x)+f @@ x = appLam f x++-- | A term-level representation of binary defunctionalized type function.+type Lam2 a b c fun = Lam a (b :~> c) fun++-- | A term-level representation of ternary defunctionalized type function.+type Lam3 a b c d fun = Lam a (b :~> c :~> d) fun++-- | Unwrapped representation of binary defunctionalized type function.+type LamRep2  :: (a -> Type) -> (b -> Type) -> (c -> Type) -> (a ~> b ~> c) -> Type+type LamRep2 a b c fun = forall x y. a x -> b y -> c (fun @@ x @@ y)++-- | Unwrapped representation of ternary defunctionalized type function.+type LamRep3  :: (a -> Type) -> (b -> Type) -> (c -> Type) -> (d -> Type) -> (a ~> b ~> c ~> d) -> Type+type LamRep3 a b c d fun = forall x y z. a x -> b y -> c z -> d (fun @@ x @@ y @@ z)++-- | 'Lam2' explicitly bidirectional pattern synonyms for binary defunctionalized type function.+pattern Lam2 :: LamRep2 a b c fun -> Lam2 a b c fun+pattern Lam2 f <- (appLam2 -> f)+  where Lam2 f = mkLam2 f++-- | 'Lam3' explicitly bidirectional pattern synonyms for ternary defunctionalized type function.+pattern Lam3 :: LamRep3 a b c d fun -> Lam3 a b c d fun+pattern Lam3 f <- (appLam3 -> f)+  where Lam3 f = mkLam3 f++-- | Constructor of 'Lam2'+mkLam2 :: LamRep2 a b c fun -> Lam2 a b c fun+mkLam2 f = Lam (\x -> Lam (f x))++-- | Destructor of 'Lam2'+appLam2 :: Lam2 a b c fun -> LamRep2 a b c fun+appLam2 f x y = f @@ x @@ y++-- | Constructor of 'Lam3'+mkLam3 :: LamRep3 a b c d fun -> Lam3 a b c d fun+mkLam3 f = Lam (\x -> mkLam2 (f x))++-- | Destructor of 'Lam3'+appLam3 :: Lam3 a b c d fun -> LamRep3 a b c d fun+appLam3 f x y z = f @@ x @@ y @@ z++-------------------------------------------------------------------------------+-- * Con+-------------------------------------------------------------------------------++-- | Wrapper for converting the normal type-level arrow into a '~>'. For example, given+--+-- >>> data Nat = Z | S Nat+--+-- we can write+--+-- >>> :kind! Map (Con1 S) '[Z, S Z]+-- Map (Con1 S) '[Z, S Z] :: [Nat]+-- = [S Z, S (S Z)]+--+type Con1 :: (a -> b) -> a ~> b+data Con1 con arg+type instance App (Con1 f) x = f x++-- | Similar to 'Con1', but for two-parameter type constructors.+type Con2 :: (a -> b -> c) -> a ~> b ~> c+data Con2 con arg+type instance App (Con2 f) arg = Con1 (f arg)++-- | Similar to 'Con2', but for three-parameter type constructors.+type Con3 :: (a -> b -> c -> d) -> a ~> b ~> c ~> d+data Con3 con arg+type instance App (Con3 f) arg = Con2 (f arg)++-- | A term-level constructor for 'Lam' of 'Con1'. For example, given+--+-- >>> data Nat = Z | S Nat+-- >>> data SNat (n :: Nat) where { SZ :: SNat Z; SS :: SNat n -> SNat (S n) }+-- >>> deriving instance Show (SNat n) +-- +-- we can define +--+-- >>> let conS = con1 SS -- taking a singleton(-like) constructor.+-- >>> :type conS+-- conS :: Lam SNat SNat (Con1 S)+--+-- and use it with term level functions+--+-- >>> map conS (SZ :* SS SZ :* SS (SS SZ) :* Nil)+-- SS SZ :* SS (SS SZ) :* SS (SS (SS SZ)) :* Nil+--+con1 :: LamRep a b (Con1 con) -> Lam a b (Con1 con)+con1 = mkLam++-- | A term-level constructor for 'Lam' of 'Con2'+con2 :: LamRep2 a b c (Con2 con) -> Lam2 a b c (Con2 con)+con2 = mkLam2++-- | A term-level constructor for 'Lam' of 'Con2'+con3 :: LamRep3 a b c d (Con3 con) -> Lam3 a b c d (Con3 con)+con3 = mkLam3
+ src/DeFun/Function.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE Trustworthy #-}+-- | Defunctionalized function combinators,+-- from [SKI](https://en.wikipedia.org/wiki/SKI_combinator_calculus)+-- and [BCKW](https://en.wikipedia.org/wiki/B,_C,_K,_W_system) combinator calculi.+--+-- These may be useful for writing anonymous functions in point-free style,+-- as pointful style would require extra defunctionalization symbols+-- (see e.g. t'DeFun.List.Map2' for an example).+--+module DeFun.Function (+    -- * Id, I+    Id, IdSym,+    id, idSym,+    -- * Const, K+    Const, ConstSym, ConstSym1,+    const, constSym, constSym1,+    -- * Flip, C+    Flip, FlipSym, FlipSym1, FlipSym2,+    flip, flipSym, flipSym1, flipSym2,+    -- * Comp, B+    Comp, CompSym, CompSym1, CompSym2,+    comp, compSym, compSym1, compSym2,+    -- * Ap, S+    Ap, ApSym, ApSym1, ApSym2,+    ap, apSym, apSym1, apSym2,+    -- * Join, W+    Join, JoinSym, JoinSym1,+    join, joinSym, joinSym1,+) where++import DeFun.Core++-- $setup+-- >>> import Prelude (Bool (..))+-- >>> import Data.Singletons.Bool (SBool (..))+-- >>> import DeFun++-- | Identity function. Combinator @I@ in https://en.wikipedia.org/wiki/SKI_combinator_calculus.+type Id :: a -> a+type family Id x where+    Id x = x++type IdSym :: a ~> a+data IdSym x+type instance App IdSym x = Id x++id :: a x -> a (Id x)+id x = x++idSym :: Lam a a IdSym+idSym = Lam id++--++-- | Constant function. Combinator @K@ in https://en.wikipedia.org/wiki/SKI_combinator_calculus and https://en.wikipedia.org/wiki/B,_C,_K,_W_system.++type Const :: a -> b -> a+type family Const x y where+    Const x y = x++type ConstSym :: a ~> b ~> a+data ConstSym x+type instance App ConstSym x = ConstSym1 x++type ConstSym1 :: a -> b ~> a+data ConstSym1 x y+type instance App (ConstSym1 x) y = Const x y++const :: a x -> b y -> a x+const x _ = x++constSym :: Lam2 a b a ConstSym+constSym = Lam constSym1++constSym1 :: a x -> Lam b a (ConstSym1 x)+constSym1 x = Lam (const x)++-- | Function flip. Combinator @C@ in https://en.wikipedia.org/wiki/B,_C,_K,_W_system.+type Flip :: (a ~> b ~> c) -> b -> a -> c+type family Flip f b a where+    Flip f b a = f @@ a @@ b++type FlipSym :: (a ~> b ~> c) ~> b ~> a ~> c+data FlipSym f+type instance App FlipSym f = FlipSym1 f++type FlipSym1 :: (a ~> b ~> c) -> b ~> a ~> c+data FlipSym1 f x+type instance App (FlipSym1 f) x = FlipSym2 f x++type FlipSym2 :: (a ~> b ~> c) -> b -> a ~> c+data FlipSym2 f b a+type instance App (FlipSym2 f b) a = Flip f b a++flip :: Lam2 a b c f -> b x -> a y -> c (Flip f x y)+flip f b a = f @@ a @@ b++flipSym :: Lam (a :~> b :~> c) (b :~> a :~> c) FlipSym+flipSym = Lam flipSym1++flipSym1 :: Lam2 a b c f -> Lam2 b a c (FlipSym1 f)+flipSym1 f = Lam (flipSym2 f)++flipSym2 :: Lam2 a b c f -> b x -> Lam a c (FlipSym2 f x)+flipSym2 f b = Lam (flip f b)+++--++-- | Function composition. Combinator @B@ in https://en.wikipedia.org/wiki/B,_C,_K,_W_system.+type Comp :: (b ~> c) -> (a ~> b) -> a -> c+type family Comp f g x where+    Comp f g x = f @@ (g @@ x)++type CompSym :: (b ~> c) ~> (a ~> b) ~> a ~> c+data CompSym f+type instance App CompSym f = CompSym1 f++type CompSym1 :: (b ~> c) -> (a ~> b) ~> a ~> c+data CompSym1 f g+type instance App (CompSym1 f) g = CompSym2 f g++type CompSym2 :: (b ~> c) -> (a ~> b) -> a ~> c+data CompSym2 f g x+type instance App (CompSym2 f g) x = Comp f g x++comp :: Lam b c f -> Lam a b g -> a x -> c (Comp f g x)+comp f g x = f @@ (g @@ x)++compSym :: Lam (b :~> c) (Lam a b :~> Lam a c) CompSym+compSym = Lam compSym1++compSym1 :: Lam b c f -> Lam (a :~> b) (a :~> c) (CompSym1 f)+compSym1 f = Lam (compSym2 f)++compSym2 :: Lam b c f -> Lam a b g -> Lam a c (CompSym2 f g)+compSym2 f g = Lam (comp f g)++-- | Combinator 'S' in https://en.wikipedia.org/wiki/SKI_combinator_calculus.+type Ap :: (a ~> b ~> c) -> (a ~> b) -> a -> c+type family Ap f g x where+    Ap f g x = f @@ x @@ (g @@ x)++type ApSym :: (a ~> b ~> c) ~> (a ~> b) ~> a ~> c+data ApSym f+type instance App ApSym f = ApSym1 f++type ApSym1 :: (a ~> b ~> c) -> (a ~> b) ~> a ~> c+data ApSym1 f g+type instance App (ApSym1 f) g = ApSym2 f g++type ApSym2 :: (a ~> b ~> c) -> (a ~> b) -> a ~> c+data ApSym2 f g x+type instance App (ApSym2 f g) x = Ap f g x++ap :: Lam2 a b c f -> Lam a b g -> a x -> c (Ap f g x)+ap f g x = f @@ x @@ (g @@ x)++apSym :: Lam3 (a :~> b :~> c) (a :~> b) a c ApSym+apSym = Lam apSym1++apSym1 :: Lam2 a b c f -> Lam2 (a :~> b) a c (ApSym1 f)+apSym1 f = Lam (apSym2 f)++apSym2 :: Lam2 a b c f -> Lam a b g -> Lam a c (ApSym2 f g)+apSym2 f g = Lam (ap f g) ++-- | Combinator 'W' in https://en.wikipedia.org/wiki/B,_C,_K,_W_system+type Join :: (a ~> a ~> b) -> a -> b+type family Join f x where+    Join f x = f @@ x @@ x++type JoinSym :: (a ~> a ~> b) ~> a ~> b+data JoinSym f+type instance App JoinSym f = JoinSym1 f++type JoinSym1 :: (a ~> a ~> b) -> a ~> b+data JoinSym1 f x+type instance App (JoinSym1 f) x = Join f x++join :: Lam2 a a b f -> a x -> b (Join f x)+join f x = f @@ x @@ x++joinSym :: Lam2 (a :~> a :~> b) a b JoinSym+joinSym = Lam joinSym1++joinSym1 :: Lam2 a a b fun -> Lam a b (JoinSym1 fun)+joinSym1 f = Lam (join f)
+ src/DeFun/List.hs view
@@ -0,0 +1,335 @@+{-# LANGUAGE Trustworthy #-}+-- | List type-families.+--+-- For term-level reflections see [defun-sop package](https://hackage.haskell.org/package/defun-sop).+--+-- Implementation note: It would be great if first-order type families,+-- like 'Append' and 'Concat', were defined already in @base@,+-- e.g. in @Data.Type.List@ module.+-- Higher-order type families, like @Map@, obviously cannot be there+-- as they rely on the defunctorization machinery.+-- Yet, some first-order type families like 'Sequence' and 'Reverse'+-- may also be defined directly, but it's more convenient to define+-- them as special case of an higher-order type family ('Map2' and 'Foldl'+-- respectively), as that makes working with them more convenient.+--+module DeFun.List (+    -- * Append+    Append, AppendSym, AppendSym1,+    -- * Map+    Map, MapSym, MapSym1,+    -- * Concat+    Concat, ConcatSym,+    -- * ConcatMap+    ConcatMap, ConcatMapSym, ConcatMapSym1,+    -- * Map2+    Map2, Map2Sym, Map2Sym1, Map2Sym2,+    -- * Sequence+    Sequence, SequenceSym,+    -- * Foldr+    Foldr, FoldrSym, FoldrSym1, FoldrSym2,+    -- * Foldl+    Foldl, FoldlSym, FoldlSym1, FoldlSym2,+    -- * ZipWith+    ZipWith, ZipWithSym, ZipWithSym1, ZipWithSym2,+    -- * Filter+    Filter, FilterSym, FilterSym1,+    -- * Reverse+    Reverse, ReverseSym,+) where++import Prelude              (Bool (..))++import DeFun.Core+import DeFun.Function++-- $setup+-- >>> import Prelude (Bool (..), Char, Maybe (..), Int, String)+-- >>> import Data.Singletons.Bool (SBool (..))+-- >>> import Numeric.Natural (Natural)+-- >>> import DeFun+-- >>> :set -dppr-cols9999++-------------------------------------------------------------------------------+-- Append+-------------------------------------------------------------------------------++-- | List append.+--+-- >>> :kind! Append [1, 2, 3] [4, 5, 6]+-- Append [1, 2, 3] [4, 5, 6] :: [Natural]+-- = [1, 2, 3, 4, 5, 6]+--+type Append :: [a] -> [a] -> [a]+type family Append xs ys where+    Append '[]       ys = ys+    Append (x ': xs) ys = x ': Append xs ys++type AppendSym :: [a] ~> [a] ~> [a]+data AppendSym xs+type instance App AppendSym xs = AppendSym1 xs++type AppendSym1 :: [a] -> [a] ~> [a]+data AppendSym1 xs ys+type instance App (AppendSym1 xs) ys = Append xs ys++-------------------------------------------------------------------------------+-- Map+-------------------------------------------------------------------------------++-- | List map+--+-- >>> :kind! Map NotSym [True, False]+-- Map NotSym [True, False] :: [Bool]+-- = [False, True]+--+-- >>> :kind! Map (Con1 Just) [1, 2, 3]+-- Map (Con1 Just) [1, 2, 3] :: [Maybe Natural]+-- = [Just 1, Just 2, Just 3]+--+type Map :: (a ~> b) -> [a] -> [b]+type family Map f xs where+    Map f '[]    = '[]+    Map f (x:xs) = f @@ x : Map f xs++type MapSym :: (a ~> b) ~> [a] ~> [b]+data MapSym f+type instance App MapSym f = MapSym1 f++type MapSym1  :: (a ~> b) -> [a] ~> [b]+data MapSym1 f xs+type instance App (MapSym1 f) xs = Map f xs++-------------------------------------------------------------------------------+-- Concat+-------------------------------------------------------------------------------++-- | List concat+--+-- >>> :kind! Concat [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]+-- Concat [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ] :: [Natural]+-- = [1, 2, 3, 4, 5, 6, 7, 8, 9]+--+type Concat :: [[a]] -> [a]+type family Concat xss where+    Concat '[] = '[]+    Concat (xs : xss) = Append xs (Concat xss)++type ConcatSym :: [[a]] ~> [a]+data ConcatSym xss+type instance App ConcatSym xss = Concat xss++-------------------------------------------------------------------------------+-- ConcatMap+-------------------------------------------------------------------------------++-- | List concatMap+type ConcatMap :: (a ~> [b]) -> [a] -> [b]+type family ConcatMap f xs where+    ConcatMap f '[]    = '[]+    ConcatMap f (x:xs) = Append (f @@ x) (ConcatMap f xs)++type ConcatMapSym :: (a ~> [b]) ~> [a] ~> [b]+data ConcatMapSym f+type instance App ConcatMapSym f = ConcatMapSym1 f++type ConcatMapSym1  :: (a ~> [b]) -> [a] ~> [b]+data ConcatMapSym1 f xs+type instance App (ConcatMapSym1 f) xs = ConcatMap f xs++-------------------------------------------------------------------------------+-- Map2+-------------------------------------------------------------------------------++-- | List binary map. I.e. 'liftA2' for lists.+--+-- Note: this is not 'ZipWith'.+--+-- >>> :kind! Map2 (Con2 '(,)) [1, 2, 3] ['x', 'y']+-- Map2 (Con2 '(,)) [1, 2, 3] ['x', 'y'] :: [(Natural, Char)]+-- = ['(1, 'x'), '(1, 'y'), '(2, 'x'), '(2, 'y'), '(3, 'x'), '(3, 'y')]+--+-- This function is a good example to highlight how to defunctionalize+-- definitions with anonymous functions.+--+-- The simple definition can be written using @concatMap@ and @map@ from+-- "Prelude":+--+-- >>> import Prelude as P (concatMap, map, (.), flip)+-- >>> let map2 f xs ys = P.concatMap (\x -> P.map (f x) ys) xs+-- >>> map2 (,) "abc" "xy"+-- [('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]+--+-- However, to make it easier (arguably) to defunctionalize, the @concatMap@ argument+-- lambda can be written in point-free form using combinators:+--+-- >>> let map2 f xs ys = P.concatMap (P.flip P.map ys P.. f) xs+-- >>> map2 (,) "abc" "xy"+-- [('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]+--+-- Alternatively, we could define a new "top-level" function+--+-- >>> let map2Aux f ys x = P.map (f x) ys+--+-- and use it to define @map2:+--+-- >>> let map2 f xs ys = P.concatMap (map2Aux f ys) xs+-- >>> map2 (,) "abc" "xy"+-- [('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]+--+type Map2 :: (a ~> b ~> c) -> [a] -> [b] -> [c]+type family Map2 f xs ys where+    Map2 f xs ys = ConcatMap (CompSym2 (FlipSym2 MapSym ys) f) xs++type Map2Sym :: (a ~> b ~> c) ~> [a] ~> [b] ~> [c]+data Map2Sym f+type instance App Map2Sym f = Map2Sym1 f++type Map2Sym1 :: (a ~> b ~> c) -> [a] ~> [b] ~> [c]+data Map2Sym1 f xs+type instance App (Map2Sym1 f) xs = Map2Sym2 f xs++type Map2Sym2 :: (a ~> b ~> c) -> [a] -> [b] ~> [c]+data Map2Sym2 f xs ys+type instance App (Map2Sym2 f xs) ys = Map2 f xs ys++-------------------------------------------------------------------------------+-- Sequence+-------------------------------------------------------------------------------++-- | List sequence+--+-- >>> :kind! Sequence [[1,2,3],[4,5,6]]+-- Sequence [[1,2,3],[4,5,6]] :: [[Natural]]+-- = [[1, 4], [1, 5], [1, 6], [2, 4], [2, 5], [2, 6], [3, 4], [3, 5], [3, 6]]+--+type Sequence :: [[a]] -> [[a]]+type family Sequence xss where+    Sequence '[]         = '[ '[] ]+    Sequence (xs ': xss) = Map2 (Con2 '(:)) xs (Sequence xss)++type SequenceSym :: [[a]] ~> [[a]]+data SequenceSym xss+type instance App SequenceSym xss = Sequence xss++-------------------------------------------------------------------------------+-- Foldr+-------------------------------------------------------------------------------++-- | List right fold+--+-- Using 'Foldr' we can define a @Curry@ type family:+--+-- >>> type Curry args res = Foldr (Con2 (->)) args res+-- >>> :kind! Curry String [Int, Bool]+-- Curry String [Int, Bool] :: *+-- = Int -> Bool -> [Char]+--+type Foldr :: (a ~> b ~> b) -> b -> [a] -> b+type family Foldr f z xs where+    Foldr f z '[]      = z+    Foldr f z (x : xs) = f @@ x @@ (Foldr f z xs)++type FoldrSym :: (a ~> b ~> b) ~> b ~> [a] ~> b+data FoldrSym f+type instance App FoldrSym f = FoldrSym1 f++type FoldrSym1 :: (a ~> b ~> b) -> b ~> [a] ~> b+data FoldrSym1 f z+type instance App (FoldrSym1 f) z = FoldrSym2 f z++type FoldrSym2 :: (a ~> b ~> b) -> b -> [a] ~> b+data FoldrSym2 f z xs+type instance App (FoldrSym2 f z) xs = Foldr f z xs++-------------------------------------------------------------------------------+-- Foldl+-------------------------------------------------------------------------------++-- | List left fold+--+type Foldl :: (b ~> a ~> b) -> b -> [a] -> b+type family Foldl f z xs where+    Foldl f z '[]      = z+    Foldl f z (x : xs) = Foldl f (f @@ z @@ x) xs++type FoldlSym :: (b ~> a ~> b) ~> b ~> [a] ~> b+data FoldlSym f+type instance App FoldlSym f = FoldlSym1 f++type FoldlSym1 :: (b ~> a ~> b) -> b ~> [a] ~> b+data FoldlSym1 f z+type instance App (FoldlSym1 f) z = FoldlSym2 f z++type FoldlSym2 :: (b ~> a ~> b) -> b -> [a] ~> b+data FoldlSym2 f z xs+type instance App (FoldlSym2 f z) xs = Foldl f z xs++-------------------------------------------------------------------------------+-- ZipWith+-------------------------------------------------------------------------------++-- | Zip with+--+-- >>> :kind! ZipWith (Con2 '(,)) [1, 2, 3] ['x', 'y']+-- ZipWith (Con2 '(,)) [1, 2, 3] ['x', 'y'] :: [(Natural, Char)]+-- = ['(1, 'x'), '(2, 'y')]+--+type ZipWith :: (a ~> b ~> c) -> [a] -> [b] -> [c]+type family ZipWith f xs ys where+    ZipWith f '[] ys = '[]+    ZipWith f (x : xs) '[] = '[]+    ZipWith f (x : xs) (y : ys) = f @@ x @@ y : ZipWith f xs ys++type ZipWithSym :: (a ~> b ~> c) ~> [a] ~> [b] ~> [c]+data ZipWithSym f+type instance App ZipWithSym f = ZipWithSym1 f++type ZipWithSym1 :: (a ~> b ~> c) -> [a] ~> [b] ~> [c]+data ZipWithSym1 f xs+type instance App (ZipWithSym1 f) xs = ZipWithSym2 f xs++type ZipWithSym2 :: (a ~> b ~> c) -> [a] -> [b] ~> [c]+data ZipWithSym2 f xs ys+type instance App (ZipWithSym2 f xs) ys = ZipWith f xs ys++-------------------------------------------------------------------------------+-- Filter+-------------------------------------------------------------------------------++-- | Filter list+type Filter :: (a ~> Bool) -> [a] -> [a]+type family Filter p xs where+    Filter f '[] = '[]+    Filter f (x ': xs) = FilterAux (f @@  x) x f xs++type FilterAux :: Bool -> a -> (a ~> Bool) -> [a] -> [a]+type family FilterAux b x p xs where+    FilterAux 'True  x p xs = x ': Filter p xs+    FilterAux 'False x p xs =      Filter p xs++type FilterSym :: (a ~> Bool) ~> [a] ~> [a]+data FilterSym p+type instance App FilterSym p = FilterSym1 p++type FilterSym1  :: (a ~> Bool) -> [a] ~> [a]+data FilterSym1 p xs+type instance App (FilterSym1 p) xs = Filter p xs++-------------------------------------------------------------------------------+-- Reverse+-------------------------------------------------------------------------------++-- | Reverse list+--+-- >>> :kind! Reverse [1,2,3,4]+-- Reverse [1,2,3,4] :: [Natural]+-- = [4, 3, 2, 1]+--+type Reverse :: [a] -> [a]+type family Reverse xs where+    Reverse xs = Foldl (FlipSym1 (Con2 '(:))) '[] xs++type ReverseSym :: [a] ~> [a]+data ReverseSym xs+type instance App ReverseSym xs = Reverse xs