diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,15 @@
 
+# 0.4.0
+
+20200216
+
+ - add Para
+ - add Histo
+ - add NatF
+ - and examples 
+ - correct the Text Length example
+ - NatMap (mimick IntMap)
+
 # 0.3.0
 
 20200209
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -25,7 +25,9 @@
  
 Why fcf-like? The kind of signatures used for functions might be easier to 
 read for some people and the ability to apply partially a function is nice 
-tool to have.
+tool to have. The techniques that allows this are defunctionalization, 
+encoding the functions with empty data types and the use of open type family 
+to Eval the constructed expressions. 
  
 If you have other motivations, please do let us know! 
 
@@ -70,7 +72,98 @@
 cabal run orbits 
 ```
 
-The `ghci` and `:kind!` command in there are your friends!
+There is also another example that show how to use MapC, see
+[Haiku.hs](https://github.com/gspia/fcf-containers/blob/master/examples/Haiku.hs)
+
+```
+cabal run haiku 
+```
+
+
+## Random Notes
+
+### Partiality and anonymous functions
+
+In the end, everything has to be total. We just post-pone the totality checking
+with defunctionalization in a way by trying to evaluate our functions as late
+as possible with the `Eval` function. 
+
+We don't have lambdas, but if you can write the helper function in point-free
+form, it might can be used directly without any global function definition.
+Remember, that `(<=<)` corresponds to term-level `(.)` and `(=<<)` to 
+term-level function  application `($)`. See also Maguire's book 
+(Thinking with Types).
+
+
+### Conflicting family instance declarations
+
+Transforming term-level Haskell code is relatively straigthforward. Often, 
+local definitions in `where` and anonymous functions will be turned into 
+separate helper functions. 
+
+Occasionally, the pattern matching is not quite enough. Please, consider
+
+```
+isPrefixOf              :: (Eq a) => [a] -> [a] -> Bool
+isPrefixOf [] _         =  True
+isPrefixOf _  []        =  False
+isPrefixOf (x:xs) (y:ys)=  x == y && isPrefixOf xs ys
+```
+
+We could try to define it as 
+```
+data IsPrefixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsPrefixOf '[] _) = 'True
+type instance Eval (IsPrefixOf _ '[]) = 'False
+type instance Eval (IsPrefixOf (x ': xs) (y ': ys)) =
+         Eval ((Eval (TyEq x y)) && Eval (IsPrefixOf xs ys))
+```
+
+But ghc does not like this definition: the first two type instances are
+conflicting together. Instead, in these situations we can use a helper type 
+family:
+
+```
+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)
+```
+
+### Using `If`
+
+If possible, try to avoid using `Eval` in the if-branches. 
+For example, consider
+```
+    (If (Eval (s > 0) )
+        ( 'Just '( a, s TL.- 1 ))
+        'Nothing
+    )
+```
+and
+```
+    (If (Eval (s > 0))
+        (Eval (Pure ( 'Just '( a, s TL.- 1 ))))
+        (Eval (Pure 'Nothing))
+    )
+```
+
+Both compile and it is easy to end up in the latter form, especially if the 
+branch is more complex than in this example. 
+
+The former, however, is much better as it doesn't have to evaluate both branches
+and is thus more efficient.
+
+
+### Other
+
+
+The `ghci` and `:kind!` command are your friends!
 
 Source also contains a lot of examples, see
 [fcf-containers](https://github.com/gspia/fcf-containers/tree/master/src/Fcf).
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -17,8 +17,6 @@
 
 ## Morphisms:
  
-- Para with examples
-- Histo with examples
 - Apo with examples
 - Futu with examples
 - and other 
diff --git a/fcf-containers.cabal b/fcf-containers.cabal
--- a/fcf-containers.cabal
+++ b/fcf-containers.cabal
@@ -6,7 +6,7 @@
     contents of containers-package and show how these can be used. Everything is
     based on the ideas given in the first-class-families -package.
 Homepage:            https://github.com/gspia/fcf-containers
-Version:             0.3.0
+Version:             0.4.0
 Build-type:          Simple
 Author:              gspia
 Maintainer:          iahogsp@gmail.com
@@ -21,6 +21,7 @@
 library
   hs-source-dirs:    src
   exposed-modules:   Fcf.Data.MapC
+                   , Fcf.Data.NatMap
                    , Fcf.Data.Tree
                    , Fcf.Data.Set
                    , Fcf.Data.Symbol
diff --git a/src/Fcf/Alg/List.hs b/src/Fcf/Alg/List.hs
--- a/src/Fcf/Alg/List.hs
+++ b/src/Fcf/Alg/List.hs
@@ -31,9 +31,9 @@
 
 import           Fcf.Core (Eval, Exp, type (@@))
 import           Fcf.Classes (Map)
-import           Fcf.Combinators (type (=<<), type (<=<))
+import           Fcf.Combinators (type (=<<), type (<=<), Pure)
 import           Fcf.Data.List (Foldr, Concat, TakeWhile, DropWhile, Reverse
-                               , type (++), ZipWith)
+                               , type (++), ZipWith, Elem, Take, Unfoldr)
 import           Fcf.Utils (If, TyEq)
 import           Fcf.Data.Bool (type (&&), type  (||), Not)
 import           Fcf.Data.Nat
@@ -56,6 +56,7 @@
 type instance Eval (Map f 'NilF) = 'NilF
 type instance Eval (Map f ('ConsF a b)) = 'ConsF a (Eval (f b))
 
+--------------------------------------------------------------------------------
 
 -- | ListToFix can be used to turn a norma type-level list into the base
 -- functor type ListF, to be used with e.g. Cata. For examples in use, see
@@ -64,12 +65,20 @@
 -- Ideally, we would have one ToFix type-level function for which we could
 -- give type instances for different type-level types, like lists, trees
 -- etc. See TODO.md.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (ListToFix '[1,2,3])
+-- Eval (ListToFix '[1,2,3]) :: Fix (ListF Nat)
+-- = 'Fix ('ConsF 1 ('Fix ('ConsF 2 ('Fix ('ConsF 3 ('Fix 'NilF))))))
 data ListToFix :: [a] -> Exp (Fix (ListF a))
 type instance Eval (ListToFix '[]) = 'Fix 'NilF
 type instance Eval (ListToFix (a ': as)) = 'Fix ('ConsF a (Eval (ListToFix as)))
 
 -- | Example algebra to calculate list length.
 -- 
+-- === __Example__
+--
 -- >>> :kind! Eval (Cata LenAlg =<< ListToFix '[1,2,3])
 -- Eval (Cata LenAlg =<< ListToFix '[1,2,3]) :: Nat
 -- = 3
@@ -79,6 +88,8 @@
 
 -- | Example algebra to calculate the sum of Nats in a list.
 -- 
+-- === __Example__
+--
 -- >>> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])
 -- Eval (Cata SumAlg =<< ListToFix '[1,2,3,4]) :: Nat
 -- = 10
@@ -88,12 +99,114 @@
 
 -- | Example algebra to calculate the prod of Nats in a list.
 --
+-- === __Example__
+--
 -- >>> :kind! Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4])
 -- Eval (Cata ProdAlg =<< ListToFix '[1,2,3,4]) :: Nat
 -- = 24
 data ProdAlg :: Algebra (ListF Nat) Nat
 type instance Eval (ProdAlg 'NilF) = 1
 type instance Eval (ProdAlg ('ConsF a b)) = a TL.* b
+
+--------------------------------------------------------------------------------
+
+-- | Form a Fix-structure that can be used with Para.
+-- 
+-- === __Example__
+--
+-- >>> :kind! Eval (ListToParaFix '[1,2,3])
+-- Eval (ListToParaFix '[1,2,3]) :: Fix (ListF (Nat, [Nat]))
+-- = 'Fix
+--     ('ConsF
+--        '(1, '[2, 3])
+--        ('Fix ('ConsF '(2, '[3]) ('Fix ('ConsF '(3, '[]) ('Fix 'NilF))))))
+data ListToParaFix :: [a] -> Exp (Fix (ListF (a,[a])))
+type instance Eval (ListToParaFix '[]) = 'Fix 'NilF
+type instance Eval (ListToParaFix (a ': as)) =
+    'Fix ('ConsF '(a,as) (Eval (ListToParaFix as)))
+
+-- | Example from recursion-package by Vanessa McHale.
+-- 
+-- This removes duplicates from a list (by keeping the right-most one).
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2])
+-- Eval (Para DedupAlg =<< ListToParaFix '[1,1,3,2,5,1,3,2]) :: [Nat]
+-- = '[5, 1, 3, 2]
+data DedupAlg :: RAlgebra (ListF (a,[a])) [a]
+type instance Eval (DedupAlg 'NilF) = '[]
+type instance Eval (DedupAlg ('ConsF '(a,as) '(_fxs, past))) = Eval
+    (If (Eval (TyEq (Eval (Elem a past)) 'True ))
+        (Pure past)
+        (Pure (a ': as))
+    )
+
+
+-- | Example from Recursion Schemes by example by Tim Williams.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Sliding 3 '[1,2,3,4,5,6])
+-- Eval (Sliding 3 '[1,2,3,4,5,6]) :: [[Nat]]
+-- = '[ '[1, 2, 3], '[2, 3, 4], '[3, 4, 5], '[4, 5, 6], '[5, 6], '[6]]
+data Sliding :: Nat -> [a] -> Exp [[a]]
+type instance Eval (Sliding n lst) =
+    Eval (Para (SlidingAlg n) =<< ListToParaFix lst)
+
+-- | Tim Williams, Recursion Schemes by example, example for Para.
+-- See 'Sliding'-function.
+data SlidingAlg :: Nat -> RAlgebra (ListF (a, [a])) [[a]]
+type instance Eval (SlidingAlg _ 'NilF) = '[]
+type instance Eval (SlidingAlg n ('ConsF '(a,as) '(_fxs,past))) =
+    Eval (Take n (a ': as)) ': past
+
+
+-- | Tim Williams, Recursion Schemes by example, example for Histo.
+data EvensStrip :: ListF a (Ann (ListF a) [a]) -> Exp [a]
+type instance Eval (EvensStrip 'NilF) = '[]
+type instance Eval (EvensStrip ('ConsF x y)) = x ': Eval (Attr y)
+
+
+-- | Tim Williams, Recursion Schemes by example, example for Histo.
+data EvensAlg :: ListF a (Ann (ListF a) [a]) -> Exp [a]
+type instance Eval (EvensAlg 'NilF) = '[]
+type instance Eval (EvensAlg ('ConsF _ rst )) = Eval (EvensStrip =<< Strip rst)
+
+-- | This picks up the elements on even positions on a list and is an 
+-- example on how to use Histo. This example is
+-- from Tim Williams, Recursion Schemes by example.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Evens =<< RunInc 8)
+-- Eval (Evens =<< RunInc 8) :: [Nat]
+-- = '[2, 4, 6, 8]
+data Evens :: [a] -> Exp [a]
+type instance Eval (Evens lst) = Eval (Histo EvensAlg =<< ListToFix lst)
+
+-- | For the ListRunAlg
+data NumIter :: a -> Nat -> Exp (Maybe (a,Nat))
+type instance Eval (NumIter a s) =
+    (If (Eval (s > 0) )
+        ( 'Just '( a, s TL.- 1 ))
+        'Nothing
+    )
+
+-- | For the RunInc
+data ListRunAlg :: Nat -> Exp (Maybe (Nat,Nat))
+type instance Eval (ListRunAlg s) = Eval (NumIter s s )
+
+-- | Construct a run (that is, a natuaral number sequence from 1 to arg).
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (RunInc 8)
+-- Eval (RunInc 8) :: [Nat]
+-- = '[1, 2, 3, 4, 5, 6, 7, 8]
+data RunInc :: Nat -> Exp [Nat]
+type instance Eval (RunInc n) = Eval (Reverse =<< Unfoldr ListRunAlg n)
+
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Fcf/Alg/Morphism.hs b/src/Fcf/Alg/Morphism.hs
--- a/src/Fcf/Alg/Morphism.hs
+++ b/src/Fcf/Alg/Morphism.hs
@@ -52,13 +52,17 @@
 -- | Commonly used name describing the method 'Ana' eats.
 type CoAlgebra f a = a -> Exp (f a)
 
+-- | Commonly used name describing the method 'Para' eats.
+type RAlgebra f a = f (Fix f, a) -> Exp a
+
 --------------------------------------------------------------------------------
 
 
 -- | Write the function to give a 'Fix', and feed it in together with an
 -- 'Algebra'.
 -- 
--- Check Fcf.Alg.List to see example algebras in use.
+-- Check Fcf.Alg.List to see example algebras in use. There we have e.g.
+-- ListToFix-function.
 data Cata :: Algebra f a -> Fix f -> Exp a
 type instance Eval (Cata alg ('Fix b)) = alg @@ (Eval (Map (Cata alg) b))
 
@@ -100,6 +104,80 @@
 -- = 15
 data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a
 type instance Eval (Hylo alg coalg a) = Eval (Cata alg =<< Ana coalg a)
+
+
+-- Helper for Para so that we can do fmap
+data Fanout :: RAlgebra f a -> Fix f -> Exp ( Fix f, a)
+type instance Eval (Fanout ralg ('Fix f)) = '( 'Fix f, Eval (Para ralg ('Fix f)))
+
+
+-- | Write a function to give a 'Fix', and feed it in together with an
+-- 'RAlgebra'
+--
+-- Check Fcf.Alg.List to see example algebras in use. There we have e.g.
+-- ListToParaFix-function.
+data Para :: RAlgebra f a -> Fix f -> Exp a
+type instance Eval (Para ralg ('Fix  a)) =  ralg @@ (Eval (Map (Fanout ralg) a))
+
+--------------------------------------------------------------------------------
+
+-- | Annotate (f r) with attribute a
+-- (from Recursion Schemes by example, Tim Williams).
+newtype AnnF f a r = AnnF (f r, a)
+
+-- | Annotated fixed-point type. A cofree comonad
+-- (from Recursion Schemes by example, Tim Williams).
+type Ann f a = Fix (AnnF f a)
+
+-- | Attribute of the root node
+-- (from Recursion Schemes by example, Tim Williams).
+data Attr :: Ann f a -> Exp a
+type instance Eval (Attr ('Fix ( 'AnnF '(_, a)))) = a
+
+-- | Strip attribute from root
+-- (from Recursion Schemes by example, Tim Williams).
+data Strip :: Ann f a -> Exp (f (Ann f a))
+type instance Eval (Strip ('Fix ( 'AnnF '(x,_)))) = x
+
+-- | Annotation constructor
+-- (from Recursion Schemes by example, Tim Williams).
+data AnnConstr :: (f (Ann f a), a) -> Exp (Fix (AnnF f a))
+type instance Eval (AnnConstr fxp) = Eval (Pure ('Fix ('AnnF fxp)))
+
+-- | Synthesized attributes are created in a bottom-up traversal
+-- using a catamorphism
+-- (from Recursion Schemes by example, Tim Williams).
+-- 
+-- This is the algebra that is fed to the cata.
+data SynthAlg :: (f a -> Exp a) -> f (Ann f a) -> Exp (Ann f a)
+type instance Eval (SynthAlg alg faf) =
+    Eval (AnnConstr '(faf, Eval (alg  =<< Map Attr faf)))
+
+-- | Synthesized attributes are created in a bottom-up traversal
+-- using a catamorphism
+-- (from Recursion Schemes by example, Tim Williams).
+-- 
+-- For the example, see "Fcf.Data.Alg.Tree.Sizes".
+data Synthesize :: (f a -> Exp a) -> Fix f -> Exp (Ann f a)
+type instance Eval (Synthesize f fx) = Eval (Cata (SynthAlg f) fx)
+
+--------------------------------------------------------------------------------
+
+-- | Histo takes annotation algebra and takes a Fix-structure
+-- (from Recursion Schemes by example, Tim Williams).
+-- 
+-- This is a helper for 'Histo' as it is implemented with 'Cata'.
+data HistoAlg :: (f (Ann f a) -> Exp a) -> f (Ann f a) -> Exp (Ann f a)
+type instance Eval (HistoAlg alg faf) =
+    Eval (AnnConstr '(faf, Eval (alg faf)))
+
+-- | Histo takes annotation algebra and takes a Fix-structure
+-- (from Recursion Schemes by example, Tim Williams).
+-- 
+-- Examples can be found from "Fcf.Data.Alg.Tree" and "Fcf.Data.Alg.List"
+-- modules.
+data Histo :: (f (Ann f a) -> Exp a) -> Fix f -> Exp a
+type instance Eval (Histo alg fx) = Eval (Attr =<< Cata (HistoAlg alg) fx)
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Fcf/Alg/Tree.hs b/src/Fcf/Alg/Tree.hs
--- a/src/Fcf/Alg/Tree.hs
+++ b/src/Fcf/Alg/Tree.hs
@@ -116,11 +116,11 @@
 -- 
 -- __Example__
 --
--- >>> :kind! Eval (Fib 10)
--- Eval (Fib 10) :: Nat
+-- >>> :kind! Eval (FibHylo 10)
+-- Eval (FibHylo 10) :: Nat
 -- = 55
-data Fib :: Nat -> Exp Nat
-type instance Eval (Fib n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)
+data FibHylo :: Nat -> Exp Nat
+type instance Eval (FibHylo n) = Eval (Hylo SumNodesAlg BuildFibTreeCoA n)
 
 
 --------------------------------------------------------------------------------
@@ -129,7 +129,89 @@
 -- algorithms.
 data BTreeF a b = BEmptyF | BNodeF a b b
 
--- functor
+-- | BTreeF is a functor
 type instance Eval (Map f 'BEmptyF) = 'BEmptyF
 type instance Eval (Map f ('BNodeF a b1 b2)) = 'BNodeF a (Eval (f b1)) (Eval (f b2))
+
+--------------------------------------------------------------------------------
+
+-- | A kind of foldable sum class. Pun may or may not be intended.
+data FSum :: f a -> Exp a
+
+-- | Instances to make TreeF to be a foldable sum. After this one, we can write
+-- the 'Sizes' example.
+type instance Eval (FSum ('NodeF a '[])) = 0
+type instance Eval (FSum ('NodeF a (b ': bs))) = Eval (Sum (b ': bs))
+
+-- | Sizes example from Recursion Schemes by example, Tim Williams. This annotes
+-- each node with the size of its subtree.
+--
+-- __Example__
+--
+-- >>> :kind! Eval (Sizes =<< Ana BuildNodeCoA 1)
+-- Eval (Sizes =<< Ana BuildNodeCoA 1) :: Fix (AnnF (TreeF Nat) Nat)
+-- = 'Fix
+--     ('AnnF
+--        '( 'NodeF
+--             1
+--             '[ 'Fix
+--                  ('AnnF
+--                     '( 'NodeF
+--                          2
+--                          '[ 'Fix ('AnnF '( 'NodeF 4 '[], 1)),
+--                             'Fix ('AnnF '( 'NodeF 5 '[], 1))],
+--                        3)),
+--                'Fix
+--                  ('AnnF
+--                     '( 'NodeF
+--                          3
+--                          '[ 'Fix ('AnnF '( 'NodeF 6 '[], 1)),
+--                             'Fix ('AnnF '( 'NodeF 7 '[], 1))],
+--                        3))],
+--           7))
+type instance Eval (Sizes fx) = Eval (Synthesize ( ( (+) 1) <=< FSum) fx)
+data Sizes :: Fix f -> Exp (Ann f Nat)
+
+--------------------------------------------------------------------------------
+
+
+-- | A NatF functor that can be used with different morphisms. This tree-module
+-- is probably a wrong place to this one. Now it is here for the Fibonacci
+-- example.
+data NatF r = Succ r | Zero
+
+-- | NatF has to have functor-instances so that morphisms will work.
+type instance Eval (Map f 'Zero) = 'Zero
+type instance Eval (Map f ('Succ r)) = 'Succ (Eval (f r))
+
+-- | We want to be able to build NatF Fix-structures out of Nat's.
+data NatToFix :: Nat -> Exp (Fix NatF)
+type instance Eval (NatToFix n) = Eval
+    (If (Eval (n < 1))
+        (Pure ('Fix 'Zero))
+        (RecNTF =<< n - 1)
+    )
+
+-- helper for 'NatToFix' -function
+data RecNTF :: Nat -> Exp (Fix NatF)
+type instance Eval (RecNTF n) = 'Fix ('Succ (Eval (NatToFix n)))
+
+-- | Efficient Fibonacci algebra from Recursion Schemes by example, Tim Williams.
+data FibAlgebra :: NatF (Ann NatF Nat) -> Exp Nat
+type instance Eval (FibAlgebra 'Zero) = 0
+type instance Eval (FibAlgebra ('Succ ('Fix ('AnnF '( 'Zero, _) )))) = 1
+type instance Eval (FibAlgebra ('Succ ('Fix ('AnnF '( 'Succ ('Fix ('AnnF '( _, n))) , m) )))) = Eval (n + m)
+
+-- | Efficient Fibonacci type-level function
+-- (from Recursion Schemes by example, Tim Williams). Compare this to 
+-- 'FibHylo'.
+--
+-- __Example__
+--
+-- >>> :kind! Eval (FibHisto 100)
+-- Eval (FibHisto 100) :: Nat
+-- = 354224848179261915075
+data FibHisto :: Nat -> Exp Nat
+type instance Eval (FibHisto n) = Eval (Histo FibAlgebra =<< NatToFix n)
+
 
diff --git a/src/Fcf/Data/NatMap.hs b/src/Fcf/Data/NatMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/NatMap.hs
@@ -0,0 +1,521 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+{-|
+Module      : Fcf.Data.NatMap
+Description : NatMap data-type for the type-level programming (like IntMap)
+Copyright   : (c) gspia 2020-
+License     : BSD
+Maintainer  : gspia
+
+= Fcf.Data.NatNatMap
+
+NatMap provides an interface to mapping keys (Nat's) to values, which is
+similar to
+NatIntMap given by the containers-package. Note that the this module still misses
+some of the methods that can be found in containers. If you need some, please
+do open up an issue or better, make a PR.
+
+Many of the examples are from containers-package.
+
+-}
+
+--------------------------------------------------------------------------------
+
+module Fcf.Data.NatMap
+    ( -- * NatMap type
+      NatMap (..)
+
+    -- * Query
+    , Null
+    , Size
+    , Lookup
+    , Member
+    , NotMember
+    , Disjoint
+    , Elems
+    , Keys
+    , Assocs
+
+    -- * Construction
+    , Empty
+    , Singleton
+    , Insert
+    , InsertWith
+    , Delete
+
+    -- * Combine
+    , Union
+    , Difference
+    , Intersection
+
+    -- * Modify
+    , Adjust
+    , Map
+    , NatMapWithKey
+    , Foldr
+    , Filter
+    , FilterWithKey
+    , Partition
+
+    -- * List
+    , FromList
+    , ToList
+
+    )
+  where
+
+-- import qualified GHC.TypeLits as TL
+
+import           Fcf ( Eval, Exp, Fst, Snd, type (=<<), type (<=<), type (@@)
+                     , type (++), Not, If
+                     , Pure, TyEq, Length, Uncurry)
+import qualified Fcf as Fcf (Map, Foldr, Filter)
+import           Fcf.Data.List (Elem)
+
+import           Fcf.Data.Nat
+import           Fcf.Alg.Morphism
+import qualified Fcf.Alg.List as Fcf (Partition)
+
+--------------------------------------------------------------------------------
+
+-- For the doctests:
+
+-- $setup
+-- >>> import           Fcf (type (>=))
+-- >>> import           Fcf.Data.Nat
+-- >>> import           Fcf.Data.Symbol (Symbol,Append)
+
+--------------------------------------------------------------------------------
+
+
+-- | A type corresponding to IntMap in the containers.
+-- 
+-- The representation is based on type-level lists. Please, do not use
+-- that fact but rather use the exposed API. (We hope to change the 
+-- internal data type to balanced tree similar to the one used in containers.
+-- See TODO.md.)
+data NatMap v = NatMap [(Nat,v)]
+
+-- | Empty
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! (Eval Empty :: NatMap Symbol)
+-- (Eval Empty :: NatMap Symbol) :: NatMap Symbol
+-- = 'NatMap '[]
+--
+-- >>> :kind! (Eval Empty :: NatMap String)
+-- (Eval Empty :: NatMap String) :: NatMap [Char]
+-- = 'NatMap '[]
+-- 
+-- See also the other examples in this module.
+data Empty :: Exp (NatMap v)
+type instance Eval Empty = 'NatMap '[]
+
+-- | Singleton
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Singleton 1 "haa")
+-- Eval (Singleton 1 "haa") :: NatMap Symbol
+-- = 'NatMap '[ '(1, "haa")]
+data Singleton :: Nat -> v -> Exp (NatMap v)
+type instance Eval (Singleton k v) = 'NatMap '[ '(k,v)]
+
+-- | Use FromList to construct a NatMap from type-level list.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (FromList '[ '(1,"haa"), '(2,"hoo")])
+-- Eval (FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap Symbol
+-- = 'NatMap '[ '(1, "haa"), '(2, "hoo")]
+data FromList :: [(Nat,v)] -> Exp (NatMap v)
+type instance Eval (FromList lst) = 'NatMap lst
+
+-- | Insert
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")])
+-- Eval (Insert 3 "hih" =<< FromList '[ '(1,"haa"), '(2,"hoo")]) :: NatMap 
+--                                                                    Symbol
+-- = 'NatMap '[ '(3, "hih"), '(1, "haa"), '(2, "hoo")]
+data Insert :: Nat -> v -> NatMap v -> Exp (NatMap v)
+type instance Eval (Insert k v ('NatMap lst)) =
+    If (Eval (Elem k =<< Fcf.Map Fst lst))
+        ('NatMap lst)
+        ('NatMap ( '(k,v) ': lst))
+
+
+-- | InsertWith
+-- if old there, map
+-- if no old, add
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (InsertWith Append 5 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap
+--                                                                           Symbol
+-- = 'NatMap '[ '(5, "xxxa"), '(3, "b")]
+--
+-- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (InsertWith Append 7 "xxx" =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap
+--                                                                           Symbol
+-- = 'NatMap '[ '(5, "a"), '(3, "b"), '(7, "xxx")]
+--
+-- >>> :kind! Eval (InsertWith Append 7 "xxx" =<< Empty)
+-- Eval (InsertWith Append 7 "xxx" =<< Empty) :: NatMap Symbol
+-- = 'NatMap '[ '(7, "xxx")]
+data InsertWith :: (v -> v -> Exp v) -> Nat -> v -> NatMap v -> Exp (NatMap v)
+type instance Eval (InsertWith f k v ('NatMap lst)) =
+    If (Eval (Elem k =<< Fcf.Map Fst lst))
+        ('NatMap (Eval (Fcf.Map (InsWithHelp f k v) lst)))
+        ('NatMap (Eval (lst ++ '[ '(k,v)])))
+
+-- helper
+data InsWithHelp :: (v -> v -> Exp v) -> Nat -> v -> (Nat,v) -> Exp (Nat,v)
+type instance Eval (InsWithHelp f k1 vNew '(k2,vOld)) =
+    If (Eval (TyEq k1 k2))
+        '(k1, Eval (f vNew vOld))
+        '(k2, vOld)
+
+
+-- | Delete
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Delete 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap
+--                                                          Symbol
+-- = 'NatMap '[ '(3, "b")]
+--
+-- >>> :kind! Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Delete 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap
+--                                                          Symbol
+-- = 'NatMap '[ '(5, "a"), '(3, "b")]
+--
+-- >>> :kind! Eval (Delete 7 =<< Empty)
+-- Eval (Delete 7 =<< Empty) :: NatMap v
+-- = 'NatMap '[]
+data Delete :: Nat -> NatMap v -> Exp (NatMap v)
+type instance Eval (Delete k ('NatMap lst)) =
+    'NatMap (Eval (Fcf.Filter (Not <=< TyEq k <=< Fst) lst))
+
+-- | Adjust
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Adjust (Append "new ") 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap
+--                                                                          Symbol
+-- = 'NatMap '[ '(5, "new a"), '(3, "b")]
+--
+-- >>> :kind! Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Adjust (Append "new ") 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap
+--                                                                          Symbol
+-- = 'NatMap '[ '(5, "a"), '(3, "b")]
+--
+-- >>> :kind! Eval (Adjust (Append "new ") 7 =<< Empty)
+-- Eval (Adjust (Append "new ") 7 =<< Empty) :: NatMap Symbol
+-- = 'NatMap '[]
+data Adjust :: (v -> Exp v) -> Nat -> NatMap v -> Exp (NatMap v)
+type instance Eval (Adjust f k ('NatMap lst)) =
+    'NatMap (Eval (AdjustHelp f k lst))
+
+data AdjustHelp :: (v -> Exp v) -> k -> [(Nat,v)] -> Exp [(Nat,v)]
+type instance Eval (AdjustHelp _f _k '[]) = '[]
+type instance Eval (AdjustHelp f k ( '(k1,v) ': rst)) =
+    If (Eval (TyEq k k1))
+        ('(k, f @@ v) ': Eval (AdjustHelp f k rst))
+        ('(k1,v) ': Eval (AdjustHelp f k rst))
+
+
+-- | Lookup
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Lookup 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol
+-- = 'Just "a"
+--
+-- >>> :kind! Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Lookup 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Maybe Symbol
+-- = 'Nothing
+data Lookup :: Nat -> NatMap v -> Exp (Maybe v)
+type instance Eval (Lookup k ('NatMap '[])) = 'Nothing
+type instance Eval (Lookup k ('NatMap ('(k1,v) ': rst))) =
+     Eval (If (Eval (TyEq k k1))
+            (Pure ('Just v))
+            (Lookup k ('NatMap rst))
+          )
+
+-- | Member
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Member 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool
+-- = 'True
+-- >>> :kind! Eval (Member 7 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Member 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool
+-- = 'False
+data Member :: Nat -> NatMap v -> Exp Bool
+type instance Eval (Member k mp) =
+    Eval (Elem k =<< Keys mp)
+
+-- | NotMember
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (NotMember 5 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool
+-- = 'False
+-- >>> :kind! Eval (NotMember 7 =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (NotMember 7 =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool
+-- = 'True
+data NotMember :: Nat -> NatMap v -> Exp Bool
+type instance Eval (NotMember k mp) =
+    Eval (Not =<< Elem k =<< Keys mp)
+
+-- | Null
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Null =<< FromList '[ '(5,"a"), '(3,"b")]) :: Bool
+-- = 'False
+-- >>> :kind! Eval (Null =<< Empty)
+-- Eval (Null =<< Empty) :: Bool
+-- = 'True
+data Null :: NatMap v -> Exp Bool
+type instance Eval (Null ('NatMap '[])) = 'True
+type instance Eval (Null ('NatMap (_ ': _))) = 'False
+
+-- | Size
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Size =<< FromList '[ '(5,"a"), '(3,"b")]) :: Nat
+-- = 2
+data Size :: NatMap v -> Exp Nat
+type instance Eval (Size ('NatMap lst)) = Eval (Length lst)
+
+-- | Union
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) )
+-- Eval (Union (Eval (FromList '[ '(5,"a"), '(3,"b")])) (Eval (FromList '[ '(5,"A"), '(7,"c")])) ) :: NatMap 
+--                                                                                                      Symbol
+-- = 'NatMap '[ '(7, "c"), '(5, "a"), '(3, "b")]
+data Union :: NatMap v -> NatMap v -> Exp (NatMap v)
+type instance Eval (Union ('NatMap lst1) ('NatMap lst2)) =
+    'NatMap (Eval (Fcf.Foldr UComb lst1 lst2))
+
+data UComb :: (k,v) -> [(k,v)] -> Exp [(k,v)]
+type instance Eval (UComb '(k,v) lst) =
+    If (Eval (Elem k =<< Fcf.Map Fst lst))
+        lst
+        ('(k,v) ': lst)
+
+
+-- | Difference
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))
+-- Eval (Difference (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: NatMap 
+--                                                                                                          Symbol
+-- = 'NatMap '[ '(3, "a")]
+data Difference :: NatMap v -> NatMap v -> Exp (NatMap v)
+type instance Eval (Difference mp1 mp2) =
+    Eval (FilterWithKey (DiffNotMem mp2) mp1)
+
+-- helper
+data DiffNotMem :: NatMap v -> k -> v -> Exp Bool
+type instance Eval (DiffNotMem mp k _) =
+    Eval (Not =<< Elem k =<< Keys mp)
+
+
+-- | Intersection
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))
+-- Eval (Intersection (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: NatMap 
+--                                                                                                            Symbol
+-- = 'NatMap '[ '(5, "b")]
+data Intersection :: NatMap v -> NatMap v -> Exp (NatMap v)
+type instance Eval (Intersection mp1 mp2) =
+    Eval (FilterWithKey (InterMem mp2) mp1)
+
+-- helper
+data InterMem :: NatMap v -> Nat -> v -> Exp Bool
+type instance Eval (InterMem mp k _) = Eval (Elem k =<< Keys mp)
+
+
+-- | Disjoint
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")])))
+-- Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(5,"B"), '(7,"C")]))) :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(2,"B"), '(7,"C")])))
+-- Eval (Disjoint (Eval (FromList '[ '(3,"a"), '(5,"b")])) (Eval (FromList '[ '(2,"B"), '(7,"C")]))) :: Bool
+-- = 'True
+-- >>> :kind! Eval (Disjoint (Eval Empty) (Eval Empty))
+-- Eval (Disjoint (Eval Empty) (Eval Empty)) :: Bool
+-- = 'True
+data Disjoint :: NatMap v -> NatMap v -> Exp Bool
+type instance Eval (Disjoint mp1 mp2) =
+    Eval (Null =<< Intersection mp1 mp2)
+
+
+-- | Map
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Fcf.Data.NatMap.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Fcf.Data.NatMap.Map (Append "x") =<< FromList '[ '(5,"a"), '(3,"b")]) :: NatMap 
+--                                                                                  Symbol
+-- = 'NatMap '[ '(5, "xa"), '(3, "xb")]
+data Map :: (v -> Exp w) -> NatMap v -> Exp (NatMap w)
+type instance Eval (Map f mp) =
+    'NatMap (Eval (Fcf.Map (Second f) =<< Assocs mp))
+
+-- | NatMapWithKey
+--
+-- === __Example__
+-- 
+data NatMapWithKey :: (Nat -> v -> Exp w) -> NatMap v -> Exp (NatMap w)
+type instance Eval (NatMapWithKey f mp) =
+    'NatMap (Eval (Fcf.Map (Second (Uncurry f))
+        =<< MWKhelp
+        =<< Assocs mp))
+
+data MWKhelp :: [(Nat,v)] -> Exp [(Nat,(Nat,v))]
+type instance Eval (MWKhelp '[]) = '[]
+type instance Eval (MWKhelp ('(k,v) ': rst)) = '(k, '(k,v)) : Eval (MWKhelp rst)
+
+
+-- | Foldr
+--
+-- Fold the values in the map using the given right-associative binary operator, 
+-- such that 'foldr f z == foldr f z . elems'.
+--
+-- Note: the order of values in NatMap is not well defined at the moment.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Fcf.Data.NatMap.Foldr (+) 0  =<< (FromList '[ '(1,1), '(2,2)]))
+-- Eval (Fcf.Data.NatMap.Foldr (+) 0  =<< (FromList '[ '(1,1), '(2,2)])) :: Nat
+-- = 3
+data Foldr :: (v -> w -> Exp w) -> w -> NatMap v -> Exp w
+type instance Eval (Foldr f w mp) = Eval (Fcf.Foldr f w =<< Elems mp)
+
+
+-- | Elems
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Elems =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Symbol]
+-- = '["a", "b"]
+-- >>> :kind! Eval (Elems =<< Empty)
+-- Eval (Elems =<< Empty) :: [v]
+-- = '[]
+data Elems :: NatMap v -> Exp [v]
+type instance Eval (Elems ('NatMap lst)) = Eval (Fcf.Map Snd lst)
+
+-- | Keys
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Keys =<< FromList '[ '(5,"a"), '(3,"b")]) :: [Nat]
+-- = '[5, 3]
+-- >>> :kind! Eval (Keys =<< Empty)
+-- Eval (Keys =<< Empty) :: [Nat]
+-- = '[]
+data Keys :: NatMap v -> Exp [Nat]
+type instance Eval (Keys ('NatMap lst)) = Eval (Fcf.Map Fst lst)
+
+-- | Assocs
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (Assocs =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, 
+--                                                        Symbol)]
+-- = '[ '(5, "a"), '(3, "b")]
+-- >>> :kind! Eval (Assocs =<< Empty)
+-- Eval (Assocs =<< Empty) :: [(Nat, v)]
+-- = '[]
+data Assocs :: NatMap v -> Exp [(Nat,v)]
+type instance Eval (Assocs ('NatMap lst)) = lst
+
+-- | ToList
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")])
+-- Eval (ToList =<< FromList '[ '(5,"a"), '(3,"b")]) :: [(Nat, 
+--                                                        Symbol)]
+-- = '[ '(5, "a"), '(3, "b")]
+-- >>> :kind! Eval (ToList =<< Empty)
+-- Eval (ToList =<< Empty) :: [(Nat, v)]
+-- = '[]
+data ToList :: NatMap v -> Exp [(Nat,v)]
+type instance Eval (ToList ('NatMap lst)) = lst
+
+-- | Filter
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])
+-- Eval (Filter ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: NatMap 
+--                                                                Nat
+-- = 'NatMap '[ '(3, 30)]
+data Filter :: (v -> Exp Bool) -> NatMap v -> Exp (NatMap v)
+type instance Eval (Filter f ('NatMap lst)) =
+    'NatMap (Eval (Fcf.Filter (f <=< Snd) lst))
+
+-- | FilterWithKey
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)])
+-- Eval (FilterWithKey (>=) =<< FromList '[ '(3,5), '(6,4)]) :: NatMap
+--                                                                Nat
+-- = 'NatMap '[ '(6, 4)]
+data FilterWithKey :: (Nat -> v -> Exp Bool) -> NatMap v -> Exp (NatMap v)
+type instance Eval (FilterWithKey f ('NatMap lst)) =
+    'NatMap (Eval (Fcf.Filter (Uncurry f) lst))
+
+-- | Partition
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)])
+-- Eval (Partition ((>=) 35) =<< FromList '[ '(5,50), '(3,30)]) :: (NatMap 
+--                                                                    Nat, 
+--                                                                  NatMap Nat)
+-- = '( 'NatMap '[ '(3, 30)], 'NatMap '[ '(5, 50)])
+data Partition :: (v -> Exp Bool) -> NatMap v -> Exp (NatMap v, NatMap v)
+type instance Eval (Partition f ('NatMap lst)) =
+    Eval (PartitionHlp (Eval (Fcf.Partition (f <=< Snd) lst)))
+
+data PartitionHlp :: ([(Nat,v)],[(Nat,v)]) -> Exp (NatMap v, NatMap v)
+type instance Eval (PartitionHlp '(xs,ys)) = '( 'NatMap xs, 'NatMap ys)
+
+
diff --git a/src/Fcf/Data/Text.hs b/src/Fcf/Data/Text.hs
--- a/src/Fcf/Data/Text.hs
+++ b/src/Fcf/Data/Text.hs
@@ -210,7 +210,7 @@
 --
 -- === __Example__
 -- 
--- > :kind! Eval (Cons "h" ('Text '["a", "a", "m", "u"]))
+-- >>> :kind! Eval (Cons "h" ('Text '["a", "a", "m", "u"]))
 -- Eval (Cons "h" ('Text '["a", "a", "m", "u"])) :: Text
 -- = 'Text '["h", "a", "a", "m", "u"]
 data Cons :: Symbol -> Text -> Exp Text