diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2018, Alejandro Serrano
+
+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 Alejandro Serrano 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/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/kind-apply.cabal b/kind-apply.cabal
new file mode 100644
--- /dev/null
+++ b/kind-apply.cabal
@@ -0,0 +1,29 @@
+cabal-version:       >=1.10
+name:                kind-apply
+version:             0.1.0.0
+synopsis:            Utilities to work with lists of types
+description:         This packages reifies the concept of list of types, and application of those to list constructors.
+-- bug-reports:
+license:             BSD3
+license-file:        LICENSE
+author:              Alejandro Serrano
+maintainer:          trupill@gmail.com
+-- copyright:
+category:            Data
+build-type:          Simple
+
+source-repository head
+  type:     git
+  location: https://gitlab.com/trupill/kind-generics.git
+
+library
+  exposed-modules:     Data.PolyKinded,
+                       Data.PolyKinded.Atom,
+                       Data.PolyKinded.Functor,
+                       GHC.Generics.Extra
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.12 && <5
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall
diff --git a/src/Data/PolyKinded.hs b/src/Data/PolyKinded.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PolyKinded.hs
@@ -0,0 +1,74 @@
+{-# language DataKinds       #-}
+{-# language TypeOperators   #-}
+{-# language GADTs           #-}
+{-# language TypeFamilies    #-}
+{-# language KindSignatures  #-}
+{-# language TypeInType      #-}
+{-# language PatternSynonyms #-}
+{-# language UndecidableInstances   #-}
+{-# language FlexibleContexts       #-}
+{-# language ScopedTypeVariables    #-}
+{-# language MultiParamTypeClasses  #-}
+{-# language FunctionalDependencies #-}
+{-# language ConstraintKinds        #-}
+module Data.PolyKinded (
+  -- * Lists of types and application
+  LoT(..), (:@@:)
+  -- * Splitting types
+, SplitF, Nat(..), TyEnv(..), SplitN, Split
+) where
+
+infixr 5 :&&:
+-- | @LoT k@ represents a list of types which can be applied
+-- to a data type of kind @k@.
+data LoT k where
+  -- | Empty list of types.
+  LoT0    ::                LoT (*)
+  -- | Cons a type with a list of types.
+  (:&&:)  :: k -> LoT ks -> LoT (k -> ks)
+
+-- | Apply a list of types to a type constructor.
+--
+-- >>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0)
+-- Either Int Bool :: *
+type family (f :: k) :@@: (tys :: LoT k) :: * where
+  f :@@: 'LoT0        = f
+  f :@@: (a ':&&: as) = f a :@@: as
+
+-- | Split a type @t@ until the constructor @f@ is found.
+--
+-- >>> :kind! SplitF (Either Int Bool) Either
+-- Int :&&: Bool :&&: LoT0 :: LoT (* -> * -> *)
+-- >>> :kind! SplitF (Either Int Bool) (Either Int)
+-- Bool :&&: LoT0 :: LoT (* -> *)
+type SplitF (t :: d) (f :: k) = SplitF' t f 'LoT0
+type family SplitF' (t :: d) (f :: k) (p :: LoT l) :: LoT k where
+  SplitF' f     f acc = acc
+  SplitF' (t a) f acc = SplitF' t f (a ':&&: acc)
+
+-- | Simple natural numbers.
+data Nat = Z | S Nat
+
+-- | A type constructor and a list of types that can be applied to it.
+data TyEnv where
+  TyEnv :: forall k. k -> LoT k -> TyEnv
+
+-- | Split a type @t@ until its list of types has length @n@.
+--
+-- >>> :kind! SplitN (Either Int Bool) (S (S Z))
+-- TyEnv Either (Int :&&: Bool :&&: LoT0) :: TyEnv
+-- >>> :kind! SplitF (Either Int Bool) (S Z)
+-- TyEnv (Either Int) (Bool :&&: LoT0) :: TyEnv
+type family SplitN (n :: Nat) t :: TyEnv where 
+  SplitN n t = SplitN' n t 'LoT0
+type family SplitN' (n :: Nat) (t :: d) (p :: LoT d) :: TyEnv where
+  SplitN' 'Z     t            acc = 'TyEnv t acc
+  SplitN' ('S n) (t (a :: l)) acc = SplitN' n t (a ':&&: acc)
+
+-- | @Split t f x@ declares that the default way to split
+-- the type @t@ is into a type constructor @f@ and a list
+-- of types @x@.
+--
+-- > instance Split (Either a b) Either (a :&&: b :&&: LoT0)
+class (x ~ SplitF t f, t ~ (f :@@: x))
+      => Split t (f :: k) (x :: LoT k) | t -> k f x
diff --git a/src/Data/PolyKinded/Atom.hs b/src/Data/PolyKinded/Atom.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PolyKinded/Atom.hs
@@ -0,0 +1,43 @@
+{-# language GADTs           #-}
+{-# language TypeOperators   #-}
+{-# language TypeFamilies    #-}
+{-# language DataKinds       #-}
+{-# language PolyKinds       #-}
+{-# language ConstraintKinds #-}
+module Data.PolyKinded.Atom where
+
+import Data.Kind
+import Data.PolyKinded
+
+data TyVar d k where
+  VZ :: TyVar (x -> xs) x
+  VS :: TyVar xs k -> TyVar (x -> xs) k
+
+type V0 = 'Var 'VZ
+type V1 = 'Var ('VS 'VZ)
+type V2 = 'Var ('VS ('VS 'VZ))
+type V3 = 'Var ('VS ('VS ('VS 'VZ)))
+type V4 = 'Var ('VS ('VS ('VS ('VS 'VZ))))
+type V5 = 'Var ('VS ('VS ('VS ('VS ('VS 'VZ)))))
+type V6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))
+type V7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))
+type V8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))
+type V9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))
+
+data Atom d k where
+  Var    :: TyVar d k -> Atom d k
+  Kon    :: k         -> Atom d k
+  (:@:)  :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
+
+type f :$: x = 'Kon f ':@: x
+type a :~: b = 'Kon (~) ':@: a ':@: b
+
+type family Ty (t :: Atom d k) (tys :: LoT d) :: k where
+  Ty ('Var 'VZ)     (t ':&&: ts) = t
+  Ty ('Var ('VS v)) (t ':&&: ts) = Ty ('Var v) ts
+  Ty ('Kon t)       tys          = t
+  Ty (f ':@: x)     tys          = (Ty f tys) (Ty x tys)
+
+type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where
+  Satisfies '[]       tys = ()
+  Satisfies (c ': cs) tys = (Ty c tys, Satisfies cs tys)
diff --git a/src/Data/PolyKinded/Functor.hs b/src/Data/PolyKinded/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PolyKinded/Functor.hs
@@ -0,0 +1,51 @@
+{-# language DataKinds              #-}
+{-# language PolyKinds              #-}
+{-# language GADTs                  #-}
+{-# language TypeOperators          #-}
+{-# language MultiParamTypeClasses  #-}
+{-# language ScopedTypeVariables    #-}
+{-# language FunctionalDependencies #-}
+{-# language TypeApplications       #-}
+{-# language AllowAmbiguousTypes    #-}
+{-# language TypeFamilies           #-}
+-- | Poly-kinded 'Functor' type class.
+-- 'KFunctor' generalizes functors, bifunctors, profunctors, ...
+-- by declaring a list of 'Variance's for a type constructor.
+module Data.PolyKinded.Functor where
+
+import Data.PolyKinded
+
+-- | Declares that the type constructor @f@ is a generalized
+-- functor whose variances for each type argument are given by @v@.
+class KFunctor (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k) | f -> v where
+  -- | The generalized version of 'fmap', 'bimap', 'dimap', and so on.
+  kfmap :: Mappings v as bs -> f :@@: as -> f :@@: bs
+
+-- | The generalized version of 'fmap', 'bimap', 'dimap', and so on.
+-- This version uses 'Split' to obtain better type inference.
+kmapo :: forall t f v as bs. (Split t f as, KFunctor f v as bs)
+      => Mappings v as bs -> t -> f :@@: bs
+kmapo = kfmap @_ @f
+
+-- ** Mappings of different variance
+
+-- | Possible variances for each argument of a type constructor.
+data Variance = Co       -- ^ The functor is covariant in this position.
+              | Contra   -- ^ The functor is contravariant in this position.
+              | Phantom  -- ^ This position is not used in any constructor.
+type Variances = [Variance]
+
+-- | If a 'KFunctor' needs to map an @f ... a ...@ to an @f ... b ...@,
+-- a @Mapping v a b@ specifies which function needs to be provided
+-- for that position depending on its variance @v@.
+type family Mapping (v :: Variance) a b where
+  Mapping 'Co      a b = a -> b
+  Mapping 'Contra  a b = b -> a
+  Mapping 'Phantom a b = ()
+
+infixr 5 :^:
+-- | List of mappings for the list of variances @v@.
+data Mappings (v :: Variances) (x :: LoT k) (y :: LoT k) where
+  M0    :: Mappings '[] 'LoT0 'LoT0
+  (:^:) :: Mapping v a b -> Mappings vs as bs
+        -> Mappings (v ': vs) (a ':&&: as) (b ':&&: bs)
diff --git a/src/GHC/Generics/Extra.hs b/src/GHC/Generics/Extra.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Generics/Extra.hs
@@ -0,0 +1,22 @@
+{-# language KindSignatures  #-}
+{-# language ConstraintKinds #-}
+{-# language PolyKinds       #-}
+{-# language GADTs           #-}
+{-# language TypeOperators   #-}
+-- | Extensions to the "GHC.Generics" module.
+module GHC.Generics.Extra (
+  module GHC.Generics
+, (:=>:)(..)
+) where
+
+import Data.Kind
+import GHC.Generics
+
+-- | Constraints: used to represent constraints in a constructor.
+--
+-- > data Showable a = Show a => a -> X a
+-- >
+-- > instance Generic (Showable a) where
+-- >   type Rep (Showable a) = (Show a) :=>: (K1 R a)
+data (:=>:) (c :: Constraint) (f :: k -> *) (a :: k) where
+  SuchThat :: c => f a -> (c :=>: f) a