diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+## 0.1
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/defun-core.cabal b/defun-core.cabal
new file mode 100644
--- /dev/null
+++ b/defun-core.cabal
@@ -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
diff --git a/src/DeFun/Bool.hs b/src/DeFun/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/DeFun/Bool.hs
@@ -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
diff --git a/src/DeFun/Core.hs b/src/DeFun/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/DeFun/Core.hs
@@ -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
diff --git a/src/DeFun/Function.hs b/src/DeFun/Function.hs
new file mode 100644
--- /dev/null
+++ b/src/DeFun/Function.hs
@@ -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)
diff --git a/src/DeFun/List.hs b/src/DeFun/List.hs
new file mode 100644
--- /dev/null
+++ b/src/DeFun/List.hs
@@ -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