diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for ranged-list
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Yoshikuni Jujo (c) 2020
+
+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 Yoshikuni Jujo 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,885 @@
+# ranged-list
+
+## What's this
+
+This package provides lists whose lengths are determined by the type and
+lists whose ranges of lengths are determined by the type.
+
+```haskell
+sample1 :: LengthL 3 Integer
+sample1 = 1 :. 2 :. 3 :. NilL
+
+sample2 :: LengthR 3 Integer
+sample2 = NilR :+ 1 :+ 2 :+ 3
+
+sample3 :: RangeL 2 5 Integer
+sample3 = 1 :. 2 :. 3 :.. 4 :.. NilL
+
+sample4 :: RangeR 2 5 Integer
+sample4 = NilR :++ 1 :++ 2 :+ 3 :+ 4
+```
+
+`LengthL 3 Integer` and `LengthR 3 Integer` are lists who have just 3 `Integer`.
+`RangeL 2 5 Integer` and `RangeR 2 5 Integer` are lists whose element numbers
+are 2 at minimum and 5 at maximum.
+`LengthL 3 Integer` and `RangeL 2 5 Integer` are
+pushed or poped a element from left.
+`LengthR 3 Integer` and `RangeR 2 5 Integer` are
+pushed or poped a element from right.
+
+## Motivation
+
+Suppose you want to take elements from list. You can use `take` like following.
+
+```
+xs = take 3 "Hello, world!"
+```
+
+The length of `xs` is lesser or equal `3`.
+But you cannot use this knowledge when you write next code.
+You should check the argument of a next function.
+
+```haskell
+fun :: [Char] -> ...
+fun [] = ...
+fun [x] = ...
+fun [x, y] = ...
+fun [x, y, z] = ...
+fun _ = error "bad argument"
+```
+If you use `LengthL 3 Char`,
+you don't need to mind the argument has more than 3 elements.
+
+```haskell
+fun :: LengthL 3 Char -> ...
+fun (x :. y :. z :. NilL) = ...
+```
+
+## LengthL
+
+### To make rectangles from a number list
+
+Suppose you want to make a value which represent a rectangle.
+You have a number list.
+The numbers are a left border, a top border, a width and a height of
+a rectangle in order.
+The numbers of the first rectangle are followed by
+the numbers of a second rectangle,
+and the numbers of the second rectangle are followed by
+the numbers of a third rectangle,
+and so on.
+
+```
+[left1, top1, width1, height1, left2, top2, width2, height2, left3, ...]
+```
+
+The list of numbers defined above are covert to a following list.
+
+```
+[Rect left1 top1 width1 height1, Rect left2 top2 width2 height2, Rect left3 ...]
+```
+
+The code is following. (View `sample/rectangle.hs`)
+
+```haskell:sample/rectangle.hs
+import Data.Length.Length
+
+data Rect = Rect {
+	left :: Double, top :: Double,
+	width :: Double, height :: Double } derivins Show
+
+makeRect :: Length 4 Double -> Rect
+makeRect (l :. t :. w :. h :. NilL) = Rect l t w h
+
+main :: IO ()
+main = print $ map makeRect . fst $ chunksL [3, 5, 15, 2, 8, 4, 1, 9, 3, 5]
+```
+
+The function `chunksL` return a value of type `([LengthL n a], RangeL 0 (n - 1) a)`.
+The first value of this tuple is a list of `n` elements of type `a`.
+And the second value of this tuple is rest elements.
+The number of the rest elements is `0` at minimum and `n - 1` at maximum.
+
+Try running.
+
+```
+% stack ghc sample/rectangle.hs
+% ./sample/rectangle
+[Rect {left = 3.0, top = 5.0, width = 15.0, height = 2.0},
+Rect {left = 8.0, top = 4.0, width = 1.0, height = 9.0)}
+```
+
+### To take Word64 from bit list
+
+Let's define function to take a 64 bit word from bit list. (View `sample/word64.hs`)
+The language extensions and the import list are following.
+
+```haskell:sample/word64.hs
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE DAtaKinds, TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import GHC.TypeNats
+import Data.Foldable
+import Data.List.Length
+import Data.List.Range
+import Data.Bits
+import Data.Word
+import Numeric
+```
+
+You define function `takeL` to take `n` elements from list.
+
+```haskell:sample/word64.hs
+takeL :: (LoosenLMax 0 (n - 1) n, Unfoldr 0 n n, ListToLengthL n) =>
+	a -> [a] -> LengthL n a
+takeL d = either ((`fillL` d) . loosenLMax) fst . splitL
+```
+
+The function `splitL` split a list and get n element lengthed list (`LengthL n a`) and a rest of the list.
+If the list does not contain enough elements, then it returns a left value. It is a list of type `RangeL 0 (n - 1) a`.
+The function `loosenLMax` convert the type `RangeL 0 (n - 1)` into `RangeL 0 n`.
+And the function `fillL` fill the list with default value `d` to get a list `LengthL n a`.
+Try it.
+
+```
+% stack ghci sample/word64.hs
+> :set -XDataKinds
+> takeL '@' "Hello, world!" :: LengthL 5 Char
+'H' :. ('e' :. ('l' :. ('l' :. ('o' :. NilL))))
+> takeL 'W' "Hi!" :: LengthL 5 Char
+'H' :. ('i' :. ('!' :. ('@' :. ('@' :. NilL))))
+```
+
+You define data type which represent a bit as follow.
+
+```haskell:sample/word64.hs
+data Bit = O | I deriving Show
+
+boolToBit :: Bool -> Bit
+boolToBit = \case False -> O; True -> I
+
+bitToNum63 :: (Num n, Bits n) => Bit -> n
+bitToNum63 = \case O -> 0; I -> 1 `shiftL` 63
+```
+
+`O` is 0 and `I` is 1.
+Function `boolToBit` converts a value of `Bool` into a value of `Bit`.
+Function `bitToNum63` converts a value of `Bit` into a number.
+It converte the bit as a 63rd bit.
+
+You define the function which convert a bit list into 64 bit word.
+
+```haskell:sample/word64.hs
+bitsToWord64 :: LengthL 64 Bit -> Word64
+bitsToWord64 = foldl' (\w b -> w `shiftR` 1 .|. bitToNum63 b) 0
+```
+
+It gets a bit from the left end.
+It put the bit on a 63rd position of a 64 bit word.
+Then it gets a next bit.
+It shifts 64 bit word to the right.
+And it put the bit on a 63rd position of a 64 bit word.
+It continue in the same way.
+
+You define the function which take 64 bit word from a bit list expressed
+as string.
+
+```haskell:sample/word64.hs
+takeWord64 :: String -> Word64
+takeWord64 = bitsToWord64 . takeL O . (boolToBit . (== '*') <$>)
+```
+
+The argument of this function is a string.
+The string represent a bit sequence.
+Character \'\*\' is 1 and character \'.\' is 0.
+
+You define sample string and try it in function `main`.
+
+```haskell:sample/word64.hs
+sample1, sample2 :: String
+sample1 = "...*..*..*...........*...**********...*************............******"
+sample2 = "...*..*..*...........*.."
+
+main :: IO ()
+main = do
+	putStrLn $ takeWord64 sample1 `showHex` ""
+	putStrLn $ takeWord64 sample2 `showHex` ""
+```
+
+Try it.
+
+```
+% stack ghc sample/word64.hs
+% ./sample/word64
+8007ffc7fe200248
+200248
+```
+
+## LengthR
+
+### To push and pop from right
+
+A value of the type `LengthR n a` is a list of values of the type `a`.
+The length of the list is `n`.
+And you can push and pop an element from right.
+Try it. (view `sample/LengthR.hs`)
+
+```haskell:sample/LengthR.hs
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module LengthR where
+
+import Data.List.Length
+
+hello :: LengthR 5 Char
+hello = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'
+```
+
+The value `hello` is a list of characters which length is `5`.
+Let\'s push the character `'!'` from right.
+
+```
+% stack ghci sample/LengthR.hs
+> hello
+((((NilR :+ 'h') :+ 'e') :+ 'l') :+ 'l') :+ 'o'
+> hello :+ '!'
+(((((NilR :+ 'h') :+ 'e') :+ 'l') :+ 'l') :+ 'o') :+ '!'
+```
+
+### To show 4 points of rectangles
+
+#### function `fourPoints` and headers
+
+You want to calculate four points of rectangle
+from the left-top point, width and height of the rectangle.
+You define function `fourPoints`. (View `sample/fourPointsOfRect.hs`)
+
+```haskell:sample/fourPointsOfRect.hs
+fourPoints :: LengthR 4 Double -> LengthR 4 (Double, Double)
+fourPoints (NilR :+ l :+ t :+ w :+ h) =
+	NilR :+ (l, t) :+ (l + w, t) :+ (l, t + h) :+ (l + w, t + h)
+```
+
+You add language extensions and modules to import.
+
+```haskell:sample/fourPointsOfRect.hs
+{-# LANGUAGE BlockArguments, LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+import Control.Monad.Fix
+import Control.Monad.Catch
+import Data.List.Length
+import Text.Read
+```
+
+Try it.
+
+```
+% stack ghci sample/fourPointsOfRect.hs
+> fourPoints $ NilR :+ 300 :+ 200 :+ 50 :+ 30
+(((NilR :+ (300.0,200.0)) :+ (350.0,200.0)) :+ (300.0,230.0)) :+ (350.0,230.0)
+```
+
+#### to input values interactively
+
+You want to input values of a left bound, a top bound, a width and a height
+interactively.
+You want to delete the last value and reinput a new value.
+First of all, you define two data type,
+`DeleteOr a` and `NothingToDeleteException`.
+
+```haskell:sample/fourPointsOfRect.hs
+data DeleteOr a = Delete | Value a deriving Show
+data NothingToDeleteException = NothingToDeleteException deriving Show
+instance Exception NothingToDeleteException
+```
+
+And you define the function `getElems` as a class function.
+
+```haskell:sample/fourPointsOfRect.hs
+class GetElems n v where
+	getElems :: MonadThrow m =>
+		LengthR n a -> m (Maybe (DeleteOr a)) -> m (LengthR (n + v) a)
+
+instance GetElems 0 0 where getElems NilR _ = pure NilR
+
+instance {-# OVERLAPPABLE #-} 1 <= n => GetElems n 0 where
+	getElems xs@(_ :+ _) _ = pure xs
+
+instance {-# OVERLAPPABLE #-} GetElems 1 (v - 1) => GetElems 0 v where
+	getElems NilR gt = gt >>= \case
+		Nothing -> getElems NilR gt
+		Just Delete -> throwM NothingToDeleteException
+		Just (Value x) -> getElem @1 @(v - 1) (NilR :+ x) gt
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, GetElems (n - 1) (v + 1), GetElems (n + 1) (v - 1)) =>
+	GetElems n v where
+	getElems xa@(xs :+ _) gt = gt >>= \case
+		Nothing -> getElems xa gt
+		Just Delete -> getElems @(n - 1) @(v + 1) xs gt
+		Just (Value x) -> getElems @(n + 1) @(v - 1) (xa :+ x) gt
+```
+
+##### class GetElems n v
+
+The class function `getElems` has two arguments.
+The first argument is a list of values which are already inputed.
+The second argument is a monad which returns 3 kinds of values,
+a value which represents to delete, a new value to push to the list
+or a value which represents to do nothing.
+
+##### instance GetElems 0 0
+
+`n == 0` and `v == 0` means that the function `getElems` get
+ a list of no elements and return a list of no elements.
+
+##### instance GetElems n 0
+
+`v == 0` means that the function `getElems` get a list and
+return the list as it is.
+
+##### instance GetElems 0 v
+
+`n == 0` means that there are no already inputed elements.
+The monad returns 3 kind of values.
+If it returns `Nothing`, then it rerun the whole as `getElems NilR gt`.
+If it returns `Just Delete`, then `NothingToDeleteException` occurs.
+If it returns `Just (Value x)`,
+then it set the already-inputed elements to `NilR :+ x` and rerun the whole.
+
+##### instance GetElems n v
+
+The monad `gt` returns 3 kind of values.
+If it returns `Nothing`, then rerun the whole as `getElems xa gt`.
+If it returns `Just Delete`,
+then it remove an element from the already-inputed list
+and rerun the whole.
+If it returns `Just (Value x)`,
+then it set the already-inputed elements to `xa :+ x` and rerun the whole.
+
+##### to try it
+
+Try it.
+
+```
+% stack ghci sample/fourPointsOfRect.hs
+> :set -XDataKinds -XBlockArguments -XLambdaCase
+> getElems NilR (Just . Value <$> getLine) :: IO (LengthR 3 String)
+foo
+bar
+baz
+((NilR :+ "foo") :+ "bar") :+ "baz"
+> gt = (<$> getLine) \case "" -> Nothing; "d' -> Just Delete; s -> Just (Value s)
+> getElems NilR gt :: IO (LengthR 3 String)
+foo
+bar
+d
+boo
+
+baz
+((NilR :+ "foo") :+ "boo") :+ "baz"
+> getElems NilR gt :: IO (LengthR 3 String)
+foo
+bar
+d
+d
+hoge
+piyo
+baz
+((NilR :+ "hoge") :+ "piyo") :+ "baz"
+> getElems NilR gt :: IO (LengthR 3 String)
+foo
+bar
+d
+d
+d
+*** Exception: NothingToDeleteException
+```
+
+### function `titles`
+
+You define the function `titles` which show values as string with title.
+
+```haskell:sample/fourPointsOfRect.hs
+titles :: (Show a, Applicative (LengthR n)) =>
+	Int -> LengthR n String -> LengthR n a -> LengthR n String
+titles n ts xs = (\t x -> t ++ replicate (n - length t) ' ' ++ ": " ++ show x)
+	<$> ts <*> xs
+```
+
+Try it.
+
+```
+% stack ghci sample/fourPointsOfRect.hs
+> titles 5 (NilR :+ "foo" :+ "bar" :+ "baz") (NilR :+ 123 :+ 456 :+ 789)
+((NilR :+ "foo  : 123") :+ "bar  : 456") :+ "baz  : 789"
+```
+
+### function `printResult`
+
+You define the function `printResult` which show values expressing a rectangle
+and 4 points of rectangle.
+
+```haskell:sample/fourPointsOfRect.hs
+printResult :: LengthR 4 Double -> IO ()
+printResult r = do
+	putStrLn ""
+	putStrLn `mapM_` titles 6 t r; putStrLn ""
+	putStrLn `mapM_` titles 12 u (fourPoints r); putStrLn ""
+	where
+	t = NilR :+ "left :+ "top" :+ "width" :+ "height"
+	u = NIlR :+ "left-top" :+ "right-top" :+ "left-bottom" :+ "right-bottom"
+```
+
+Try it.
+
+```
+% stack ghci sample/fourPointsOfRect.hs
+> printResult $ NilR :+ 300 :+ 200 :+ 70 :+ 50
+
+left  : 300.0
+top   : 200.0
+width : 70.0
+height: 50.0
+
+left-top    : (300.0,200.0)
+right-top   : (370.0,200.0)
+left-bottom : (300.0,250.0)
+right-bottom: (370.0,250.0)
+```
+
+### function `getRect`
+
+You define the function `getRect` which gets user input to make rectangle.
+
+```haskell:sample/fourPointsOfRect.hs
+getRect :: forall n . GetElems n (4 - n) =>
+	LengthR n Double -> IO (LengthR 4 Double)
+getRect xs = (<$) <$> id <*> printRect =<<
+	getElems @n @(4 - n) xs ((<$> getLine) \case
+		"d" -> Just Delete; l -> Value <*> readMaybe l)
+	`catch`
+	\(_ :: NothingToDeleteException) ->
+		putStrLn *** Nothing to delete." >> getRect @0 NilR
+```
+
+It gets a user input with `getLine`.
+If it is `"d"`, then it deletes the last input.
+If there are nothing to delete, then `NothingToDeleteException` occur.
+It catches this exception and shows error message and rerun `getRect`.
+
+### function `main`
+
+You define function `main`.
+
+```haskell:sample/fourPointsOfRect.hs
+main :: IO ()
+main = getRect NilR >>= fix \go xa@(xs :+ _) -> getLine >>= \case
+	"q" -> pure ()
+	"d" -> go =<< getRect xs
+	_ -> putStrLn "q or d" >> go xa
+```
+
+It call function `getRect` with list of `0` elements (`NilR`).
+And it repeats function `getRect` with list of `4 - 1` elements (`xs`)
+if you input `"d"`.
+
+```
+% stack ghc sample/fourPointsOfRect.hs
+% ./sample/fourPointsOfRect
+500
+300
+75
+50
+
+left  : 500.0
+top   : 300.0
+width : 75.0
+height: 50.0
+
+left-top    : (500.0,300.0)
+right-top   : (575.0,300.0)
+left-bottom : (500.0,350.0)
+right-bottom: (575.0,350.0)
+
+d
+d
+125
+100
+
+left  : 500.0
+top   : 300.0
+width : 125.0
+height: 100.0
+
+left-top    : (500.0,300.0)
+right-top   : (625.0,300.0)
+left-bottom : (500.0,400.0)
+right-bottom: (625.0,400.0)
+
+d
+d
+d
+d
+d
+*** Nothing to delete.
+2000
+1500
+90
+50
+
+left  : 2000.0
+top   : 1500.0
+width : 90.0
+height: 50.0
+
+left-top    : (2000.0,1500.0)
+right-top   : (2090.0,1500.0)
+left-bottom : (2000.0,1550.0)
+right-bottom: (2090.0,1550.0)
+
+q
+```
+
+## RangeL and RangeR
+
+### To specify the range of a number of elements of a list
+
+You can specify the range of a number of elements of a list.
+There is a data type `RangeL n m a`.
+It represents a list which have a type `a` element.
+And its length is `n` at minimum and `m` at maximum.
+
+```
+% stack ghci
+> :module Data.List.Range
+> :set -XDataKinds
+> 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL :: RangeL 3 8 Char
+'h' :. ('e' :. ('l' :. ('l' :.. ('o' :.. NilL))))
+```
+
+### To get passwords
+
+Suppose you want to get a password
+whose length is 8 at minimum and 127 at maximum.
+First of all, you define headers.
+
+```haskell:sample/password.hs
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import Data.List.Range
+import System.IO
+
+import qualified Data.ByteString.Char8 as BSC
+```
+
+You define `type Password`.
+
+```haskell:sample/password.hs
+type Password = RangeL 8 127 Char
+```
+
+It is a list of `Char`.
+Its length is 8 at minimum and 127 at maximum.
+
+You define a function `getRangedString`.
+It recieves a user input.
+It return a just value if the length of the input is within range.
+It return a nothing value if the length of the input is out of range.
+
+```haskell:sample/password.hs
+getRangedPassword :: Unfoldr 0 n m => IO (Maybe (RangeL n m Char))
+getRangedPassword = do
+	e <- hGetEcho stdin
+	hSetEcho stdin False
+	unfoldrMRangeMaybe ((/= '\n') <$> hLookAhead stdin) getChar
+		<* hSetEcho stdin e
+```
+
+It makes echo of stdin off.
+It gets characters until you input `'\n'`.
+And it makes echo of stdin on.
+
+```
+% stack ghci sample/password.hs
+> :set -XDataKinds
+> getRangedPassword :: IO (Maybe Password)
+(Input "foobarbaz")
+Just ('f' :. ('o' :. ('o' :. ('b' :. ('a' :. ('r' :. ('b' :. ('a' :. ('z' :..NilL)))))))))
+> getRangedPassword :: IO (Maybe Password)
+(Input "foo")
+Nothing
+> getRangedPassword :: IO (Maybe (RangeL 2 5 Char))
+(Input "foobar")
+Nothing
+> r
+```
+
+You want to convert a value of type `Password` into a value of `ByteString`.
+You can use other packages if you get password as a value of `ByteString`.
+
+```haskell:sample/password.hs
+passwordToByteString :: Password -> BSC.ByteString
+passwordToByteString = foldr BSC.cons ""
+```
+
+You define function `main` to try it.
+
+```haskell:sample/password.hs
+main :: IO ()
+main = do
+	p <- getRangedPassword
+	print p
+	maybe (eror "bad password length") BSC.putStrLn $ passwordToByteString <$> p
+```
+
+Try it.
+
+```
+% stack ghc sample/password.hs
+% ./sample/password
+(Input "foobarbaz")
+Just ('f' :. ('o' :. ('o' :. ('b' :. ('a' :. ('r' :. ('b' :. ('a' :. ('z' :.. NilL)))))))))
+foobarbaz
+```
+
+### Finger Tree
+
+The next example is Finger Tree.
+
+[Finger Trees: A Simple General-purpose Data Structure](https://www.staff.city.ac.uk/~ross/papers/FingerTree.html)
+
+#### Language Extension and Import List
+
+Let's make headers.
+
+```haskell:sample/fingertree.hs
+{-# LANGUAGE ScopedTypeVariables, TypeApplications, InstanceSigs #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}You
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+import Data.List.Range
+```
+
+#### Types
+
+You can describe Finger Tree as follows.
+
+```haskell:sample/fingertree.hs
+data FingerTree a
+	= Enpty | Single a
+	| Deep (DigitL a) (FingerTree (Node a)) (DigitR a)
+	deriving Show
+
+type Node = RangeL 2 3
+type DigitL = RangeL 1 4
+type DigitR = RangeR 1 4
+```
+
+A list of type `Node a` contains two or three elements of type `a`.
+A list of type `DigitL a` contains one elements at minimum and
+four elements at maximum.
+A list of type `DigitR a` contains the same number of elements as `DigitL a`.
+But you can push and pop a element from right.
+
+#### To push from left
+
+You define the function which Add a new element to the left of the sequence.
+First of all you define the function to push an element to a list of type `DigitL a`.
+
+```haskell:sample/fingertree.hs
+infixr 5 <||
+
+(<||) :: a -> DigitL a -> Either (DigitL a) (DigitL a, Node a)
+a <|| b :. NilL = Left $ a :. b :.. NilL
+a <|| b :. c :.. NilL = Left $ a :. b :.. c :.. NilL
+a <|| b :. c :.. d :.. NilL = Left $ a :. b :.. c :.. d :.. NilL
+a <|| b :. c :.. d :.. e :.. NilL =
+	Right (a :. b :.. NilL, c :. d :. e :.. NilL)
+```
+
+If the original list has fewer elements than four,
+then it return a left value list which contains the added value.
+If the original list has just four elements,
+then it returns a right value tuple which contain the value of type `DigitL a`
+and the value of type `Node a`.
+
+You can define the function which add a new element to the left of the sequence.
+
+```haskell:sample/fingertree.hs
+infixr 5 <|
+
+(<|) :: a -> FingerTree a -> FingerTree a
+a <| Empty = Single a
+a <| Single a = Deep (a :. NilL) Empty (NilR :+ b)
+a <| Deep pr m sf = case a <|| pr of
+	Left pr' -> Deep pr' m sf
+	Right (pr', n3) -> Deep pr' (n3 <| m) sf
+```
+
+It pushes three of the elements as a `Node`, leaving two behind.
+
+You also require the liftings of `<|`.
+
+```haskell:sample/fingertree.hs
+infixr 5 <|.
+
+(<|.) :: Foldable t => t a -> FingerTree a -> FingerTree a
+(<|.) = flip $ foldr (<|)
+```
+
+To make finger tree from a list or other foldable structure,
+you define a function `toTree`.
+
+```haskell:sample/fingertree.hs
+toTree :: Foldable t => t a -> FingerTree a
+toTree = (<|. Empty)
+```
+
+#### To push from right
+
+Adding to the right end of the sequence is the mirror image of the above.
+
+```haskell:sample/fingertree.hs
+infixl 5 ||>, |>, |>.
+
+(||>) :: DigitR a -> a -> Either (DigitR a) (Node a, DigitR a)
+NilR :+ a ||> b = Left $ NilR :++ a :+ b
+NilR :++ a :+ b ||> c = Left $ NilR :++ a :++ b :+ c
+NIlR :++ a :++ b :+ c ||> d = Left $ NilR :++ a :++ b :++ c :+ d
+NilR :++ a :++ b :++ c :+ d ||> e =
+	Right (a :. b :. c :.. NilL, NilR :++ d :+ e)
+
+(|>) :: FingerTree a -> a -> FingerTree a
+Empty |> a = Single a
+Single a |> b = Deep (a :. NilL) Empty (NilR :+ b)
+Deep pr m sf |> a = case sf ||> a of
+	Left sf' -> Deep pr m sf'
+	Right (n3, sf') -> Deep pr (m |> n3) sf'
+
+(|>.) :: Foldable t => FingerTree a -> t a -> FingerTree a
+(|>.) = foldl (|>)
+```
+
+#### To pop from left
+
+To deconstruct a sequence, you define a function `uncons`.
+
+```haskell:sample/fingertree.hs
+uncons :: FingerTree a -> Maybe (a, FingerTree a)
+uncons Empty = Nothing
+uncons (Single x) = Just (x, Empty)
+uncons (Deep (a :. pr') m sf) = Just (a, deepL pr' m sf)
+
+deepL :: RangeL 0 3 a -> FingerTree (Node a) -> DigitR a -> FingerTree a
+deepL NilL m sf = case uncons m of
+	Nothing -> toTree sf
+	Just (n, m') -> Deep (loosenL n) m' sf
+deepL (a :.. pr) m sf = Deep (loosenL $ a :. pr) m sf
+```
+
+Since the prefix `pr` of a `Deep` tree contains at least one element,
+you can get its head.
+However, the tail of the prefix may be empty,
+and thus unsuitable as a first argument to the Deep constructor.
+Hence you define a smart constructor that differs from `Deep` by allowing the
+prefix to contain zero to three elements,
+and in the empty case uses a `uncons` of the middle tree to construct a tree of
+the correct shape.
+
+#### Concatenation
+
+First of all you define a function which devide a list into a list of `Node`.
+The original list has 3 elements at minimum and 12 elements at maximum.
+The returned list has 1 node at minimum and 4 nodes at maximum.
+The function has a type like the following.
+
+```haskell
+fun :: RangeL 3 12 a -> RangeL 1 4 (Node a)
+```
+
+You can define a more general function like the following.
+
+```haskell
+fun :: RangeL 3 m a -> RangeL 1 w (Node a)
+```
+
+`m` is 3 times `w`.
+
+You define a class.
+
+```haskell:sample/fingertree.hs
+class Nodes m w where nodes :: RangeL 3 m a -> RangeL 1 w (Node a)
+```
+
+And you define instance when `m` is 3 and `w` is 1.
+
+```haskell:sample/fingertree.hs
+instance Nodes 3 1 where nodes = (:. NilL) . loosenL	
+```
+
+And you define instance of general case.
+
+```haskell:sample/fingertree.hs
+instance {-# OVERLAPPABLE #-} (2 <= w, Nodes (m - 3) (w - 1)) => Nodes m w where
+	nodes :: forall a . RangeL 3 m a -> RangeL 1 w (Node a)
+	nodes (a :. b :. c :. NilL) = (a :. b :. c :.. NilL) :. NilL
+	nodes (a :. b :. c :. d :.. NilL) =
+		(a :. b :. NilL) :. (c :. d :. NilL) :.. NilL
+	nodes (a :. b :. c :. d :.. e :.. NilL) =
+		(a :. b :. c :.. NilL) :. (d :. e :. NilL) :.. NilL
+	nodes (a :. b :. c :. d :.. e :.. f :.. xs) =
+		(a :. b :. c :.. NilL) .:..
+			nodes @(m - 3) @(w - 1) (d :. e :. f :. xs)
+```
+
+Try it.
+
+```
+% stack ghci sample/fingertree.hs
+> :set -XTypeApplications -XDataKinds
+> xs = 1 :. 2 :. 3 :. 4 :.. 5 :.. 6 :.. 7 :.. 8 :.. NilL :: RangeL 3 12 Integer
+> nodes @12 @4 xs
+(1 :. (2 :. (3 :.. NilL))) :. ((4 :. (5 :. (6 :.. NilL))) :.. ((7 :. (8 :. NilL)) :.. NilL))
+> :type it
+it :: Num a => RangeL 1 4 (Node a)
+```
+
+You can combine the two digit argument into a list of Nodes
+with the function `nodes`.
+You can obtain a recursive function by
+generalizing the concatenation function to take an additional list of elements.
+
+```haskell:sample/fingertree.hs
+app3 :: FingerTree a -> RangeL 1 4 a -> FingerTree a -> FingerTree a
+app3 Empty m xs = m <|. xs
+app3 xs m Empty = xs |>. m
+app3 (Single x) m xs = x <| m <|. xs
+app3 xs m (Single x) = xs |>. m |> x
+app3 (Deep pr1 m1 sf1) m (Deep pr2 m2 sf2) =
+	Deep pr1 (app3 m1 (nodes $ sf1 ++.. m ++. pr2) m2) sf2
+```
+
+To concatenate two finger trees, you take a head element from a second sequence.
+
+```haskell:sample/fingertree.hs
+(><) :: FingerTree a -> FingerTree a -> FingerTree a
+l >< r = case uncons r of Nothing -> l; Just (x, r') -> app3 l (x :. NilL) r'
+```
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/ranged-list.cabal b/ranged-list.cabal
new file mode 100644
--- /dev/null
+++ b/ranged-list.cabal
@@ -0,0 +1,85 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 42c7def6fb4ed75b8b978a1de4cdf116653323fb1cee0e251bceaa00ef7be780
+
+name:           ranged-list
+version:        0.1.0.0
+synopsis:       The list like structure whose length or range of length can be specified
+description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/ranged-list#readme>
+category:       List
+homepage:       https://github.com/YoshikuniJujo/ranged-list#readme
+bug-reports:    https://github.com/YoshikuniJujo/ranged-list/issues
+author:         Yoshikuni Jujo
+maintainer:     PAF01143@nifty.ne.jp
+copyright:      Yoshikuni Jujo
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+data-files:
+    rectangle.hs
+    word64.hs
+    LengthR.hs
+    fourPointsOfRect.hs
+    password.hs
+    fingertree.hs
+data-dir:       sample
+
+source-repository head
+  type: git
+  location: https://github.com/YoshikuniJujo/ranged-list
+
+library
+  exposed-modules:
+      Data.List.Length
+      Data.List.Range
+      Data.List.Range.Nat
+  other-modules:
+      Control.Monad.Identity
+      Control.Monad.State
+      Data.List.Length.LengthL
+      Data.List.Length.LengthR
+      Data.List.Range.RangeL
+      Data.List.Range.RangeR
+      Paths_ranged_list
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , typecheck-plugin-nat-simple
+  default-language: Haskell2010
+
+test-suite ranged-list-doctest
+  type: exitcode-stdio-1.0
+  main-is: doctests.hs
+  other-modules:
+      Paths_ranged_list
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , doctest
+    , ranged-list
+    , typecheck-plugin-nat-simple
+  default-language: Haskell2010
+
+test-suite ranged-list-test
+  type: exitcode-stdio-1.0
+  main-is: spec.hs
+  other-modules:
+      Paths_ranged_list
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , ranged-list
+    , typecheck-plugin-nat-simple
+  default-language: Haskell2010
diff --git a/sample/LengthR.hs b/sample/LengthR.hs
new file mode 100644
--- /dev/null
+++ b/sample/LengthR.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module LengthR where
+
+import Data.List.Length
+
+hello :: LengthR 5 Char
+hello = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'
diff --git a/sample/fingertree.hs b/sample/fingertree.hs
new file mode 100644
--- /dev/null
+++ b/sample/fingertree.hs
@@ -0,0 +1,108 @@
+{-# LANGUAGE ScopedTypeVariables, TypeApplications, InstanceSigs #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+import Data.List.Range
+
+data FingerTree a
+	= Empty | Single a
+	| Deep (DigitL a) (FingerTree (Node a)) (DigitR a)
+	deriving Show
+
+type Node = RangeL 2 3
+type DigitL = RangeL 1 4
+type DigitR = RangeR 1 4
+
+infixr 5 <||
+
+(<||) :: a -> DigitL a -> Either (DigitL a) (DigitL a, Node a)
+a <|| b :. NilL = Left $ a :. b :.. NilL
+a <|| b :. c :.. NilL = Left $ a :. b :.. c :.. NilL
+a <|| b :. c :.. d :.. NilL = Left $ a :. b :.. c :.. d :.. NilL
+a <|| b :. c :.. d :.. e :.. NilL =
+	Right (a :. b :.. NilL, c :. d :. e :.. NilL)
+
+infixr 5 <|
+
+(<|) :: a -> FingerTree a -> FingerTree a
+a <| Empty = Single a
+a <| Single b = Deep (a :. NilL) Empty (NilR :+ b)
+a <| Deep pr m sf = case a <|| pr of
+	Left pr' -> Deep pr' m sf
+	Right (pr', n3) -> Deep pr' (n3 <| m) sf
+
+infixr 5 <|.
+
+(<|.) :: Foldable t => t a -> FingerTree a -> FingerTree a
+(<|.) = flip $ foldr (<|)
+
+toTree :: Foldable t => t a -> FingerTree a
+toTree = (<|. Empty)
+
+infixl 5 ||>, |>, |>.
+
+(||>) :: DigitR a -> a -> Either (DigitR a) (Node a, DigitR a)
+NilR :+ a ||> b = Left $ NilR :++ a :+ b
+NilR :++ a :+ b ||> c = Left $ NilR :++ a :++ b :+ c
+NilR :++ a :++ b :+ c ||> d = Left $ NilR :++ a :++ b :++ c :+ d
+NilR :++ a :++ b :++ c :+ d ||> e =
+	Right (a :. b :. c :.. NilL, NilR :++ d :+ e)
+
+(|>) :: FingerTree a -> a -> FingerTree a
+Empty |> a = Single a
+Single a |> b = Deep (a :. NilL) Empty (NilR :+ b)
+Deep pr m sf |> a = case sf ||> a of
+	Left sf' -> Deep pr m sf'
+	Right (n3, sf') -> Deep pr (m |> n3) sf'
+
+(|>.) :: Foldable t => FingerTree a -> t a -> FingerTree a
+(|>.) = foldl (|>)
+
+uncons :: FingerTree a -> Maybe (a, FingerTree a)
+uncons Empty = Nothing
+uncons (Single x) = Just (x, Empty)
+uncons (Deep (a :. pr') m sf) = Just (a, deepL pr' m sf)
+
+deepL :: RangeL 0 3 a -> FingerTree (Node a) -> DigitR a -> FingerTree a
+deepL NilL m sf = case uncons m of
+	Nothing -> toTree sf
+	Just (n, m') -> Deep (loosenL n) m' sf
+deepL (a :.. pr) m sf = Deep (loosenL $ a :. pr) m sf
+
+class Nodes m w where nodes :: RangeL 3 m a -> RangeL 1 w (Node a)
+
+instance Nodes 3 1 where nodes = (:. NilL) . loosenL
+
+instance {-# OVERLAPPABLE #-} (2 <= w, Nodes (m - 3) (w - 1)) => Nodes m w where
+	nodes :: forall a . RangeL 3 m a -> RangeL 1 w (Node a)
+	nodes (a :. b :. c :. NilL) = (a :. b :. c :.. NilL) :. NilL
+	nodes (a :. b :. c :. d :.. NilL) =
+		(a :. b :. NilL) :. (c :. d :. NilL) :.. NilL
+	nodes (a :. b :. c :. d :.. e :.. NilL) =
+		(a :. b :. c :.. NilL) :. (d :. e :. NilL) :.. NilL
+	nodes (a :. b :. c :. d :.. e :.. f :.. xs) =
+		(a :. b :. c :.. NilL) .:..
+			nodes @(m - 3) @(w - 1) (d :. e :. f :. xs)
+
+app3 :: FingerTree a -> RangeL 1 4 a -> FingerTree a -> FingerTree a
+app3 Empty m xs = m <|. xs
+app3 xs m Empty = xs |>. m
+app3 (Single x) m xs = x <| m <|. xs
+app3 xs m (Single x) = xs |>. m |> x
+app3 (Deep pr1 m1 sf1) m (Deep pr2 m2 sf2) =
+	Deep pr1 (app3 m1 (nodes $ sf1 ++.. m ++. pr2) m2) sf2
+
+(><) :: FingerTree a -> FingerTree a -> FingerTree a
+l >< r = case uncons r of Nothing -> l; Just (x, r') -> app3 l (x :. NilL) r'
+
+main :: IO ()
+main = do
+	let	h = toTree "Hello, "
+		w = toTree "world!"
+	print h
+	print $ uncons h
+	print $ h >< w
diff --git a/sample/fourPointsOfRect.hs b/sample/fourPointsOfRect.hs
new file mode 100644
--- /dev/null
+++ b/sample/fourPointsOfRect.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE BlockArguments, LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+import Control.Monad.Fix
+import Control.Monad.Catch
+import Data.List.Length
+import Text.Read
+
+fourPoints :: LengthR 4 Double -> LengthR 4 (Double, Double)
+fourPoints (NilR :+ l :+ t :+ w :+ h) =
+	NilR :+ (l, t) :+ (l + w, t) :+ (l, t + h) :+ (l + w, t + h)
+
+data DeleteOr a = Delete | Value a deriving Show
+data NothingToDeleteException = NothingToDeleteException deriving Show
+instance Exception NothingToDeleteException
+
+class GetElems n v where
+	getElems :: MonadThrow m =>
+		LengthR n a -> m (Maybe (DeleteOr a)) -> m (LengthR (n + v) a)
+
+instance GetElems 0 0 where getElems NilR _ = pure NilR
+
+instance {-# OVERLAPPABLE #-} 1 <= n => GetElems n 0 where
+	getElems xs@(_ :+ _) _ = pure xs
+
+instance {-# OVERLAPPABLE #-} GetElems 1 (v - 1) => GetElems 0 v where
+	getElems NilR gt = gt >>= \case
+		Nothing -> getElems NilR gt
+		Just Delete -> throwM NothingToDeleteException
+		Just (Value x) -> getElems @1 @(v - 1) (NilR :+ x) gt
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, GetElems (n - 1) (v + 1), GetElems (n + 1) (v - 1)) =>
+	GetElems n v where
+	getElems xa@(xs :+ _) gt = gt >>= \case
+		Nothing -> getElems xa gt
+		Just Delete -> getElems @(n - 1) @(v + 1) xs gt
+		Just (Value x) -> getElems @(n + 1) @(v - 1) (xa :+ x) gt
+
+titles :: (Show a, Applicative (LengthR n)) =>
+	Int -> LengthR n String -> LengthR n a -> LengthR n String
+titles n ts xs = (\t x -> t ++ replicate (n - length t) ' ' ++ ": " ++ show x)
+	<$> ts <*> xs
+
+printResult :: LengthR 4 Double -> IO ()
+printResult r = do
+	putStrLn ""
+	putStrLn `mapM_` titles 6 t r; putStrLn ""
+	putStrLn `mapM_` titles 12 u (fourPoints r); putStrLn ""
+	where
+	t = NilR :+ "left" :+ "top" :+ "width" :+ "height"
+	u = NilR :+ "left-top" :+ "right-top" :+ "left-bottom" :+ "right-bottom"
+
+getRect :: forall n . GetElems n (4 - n) =>
+	LengthR n Double -> IO (LengthR 4 Double)
+getRect xs = (<$) <$> id <*> printResult =<<
+	getElems @n @(4 - n) xs ((<$> getLine) \case
+		"d" -> Just Delete; l -> Value <$> readMaybe l)
+	`catch`
+	\(_ :: NothingToDeleteException) ->
+		putStrLn "*** Nothing to delete." >> getRect @0 NilR
+
+main :: IO ()
+main = getRect NilR >>= fix \go xa@(xs :+ _) -> getLine >>= \case
+	"q" -> pure ();
+	"d" -> go =<< getRect xs
+	_ -> putStrLn "q or d" >> go xa
diff --git a/sample/password.hs b/sample/password.hs
new file mode 100644
--- /dev/null
+++ b/sample/password.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import Data.List.Range
+import System.IO
+
+import qualified Data.ByteString.Char8 as BSC
+
+type Password = RangeL 8 127 Char
+
+getRangedPassword :: Unfoldr 0 n m => IO (Maybe (RangeL n m Char))
+getRangedPassword = do
+	e <- hGetEcho stdin
+	hSetEcho stdin False
+	unfoldrMRangeMaybe ((/= '\n') <$> hLookAhead stdin) getChar
+		<* hSetEcho stdin e
+
+passwordToByteString :: Password -> BSC.ByteString
+passwordToByteString = foldr BSC.cons ""
+
+main :: IO ()
+main = do
+	p <- getRangedPassword
+	print p
+	maybe (error "bad password length") BSC.putStrLn $ passwordToByteString <$> p
diff --git a/sample/rectangle.hs b/sample/rectangle.hs
new file mode 100644
--- /dev/null
+++ b/sample/rectangle.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import Data.List.Length
+
+data Rect = Rect {
+	left :: Double, top :: Double,
+	width :: Double, height :: Double } deriving Show
+
+makeRect :: LengthL 4 Double -> Rect
+makeRect (l :. t :. w :. h :. NilL) = Rect l t w h
+
+main :: IO ()
+main = print $ map makeRect . fst $ chunksL [3, 5, 15, 2, 8, 4, 1, 9, 3, 5]
diff --git a/sample/word64.hs b/sample/word64.hs
new file mode 100644
--- /dev/null
+++ b/sample/word64.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import GHC.TypeNats
+import Data.Foldable
+import Data.List.Length
+import Data.List.Range
+import Data.Bits
+import Data.Word
+import Numeric
+
+takeL :: (LoosenLMax 0 (n - 1) n, Unfoldr 0 n n, ListToLengthL n) =>
+	a -> [a] -> LengthL n a
+takeL d = either ((`fillL` d) . loosenLMax) fst . splitL
+
+data Bit = O | I deriving Show
+
+boolToBit :: Bool -> Bit
+boolToBit = \case False -> O; True -> I
+
+bitToNum63 :: (Num n, Bits n) => Bit -> n
+bitToNum63 = \case O -> 0; I -> 1 `shiftL` 63
+
+bitsToWord64 :: LengthL 64 Bit -> Word64
+bitsToWord64 = foldl' (\w b -> w `shiftR` 1 .|. bitToNum63 b) 0
+
+takeWord64 :: String -> Word64
+takeWord64 = bitsToWord64 . takeL O . (boolToBit . (== '*') <$>)
+
+main :: IO ()
+main = do
+	putStrLn $ takeWord64 sample1 `showHex` ""
+	putStrLn $ takeWord64 sample2 `showHex` ""
+
+sample1, sample2 :: String
+sample1 = "...*..*..*...........*...**********...*************............******"
+sample2 = "...*..*..*...........*.."
diff --git a/src/Control/Monad/Identity.hs b/src/Control/Monad/Identity.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Identity.hs
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Control.Monad.Identity (Identity(..)) where
+
+newtype Identity a = Identity { runIdentity :: a } deriving Show
+
+instance Functor Identity where fmap = (Identity .) . (. runIdentity)
+
+instance Applicative Identity where
+	pure = Identity; Identity f <*> Identity x = Identity $ f x
+
+instance Monad Identity where Identity x >>= f = f x
diff --git a/src/Control/Monad/State.hs b/src/Control/Monad/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/State.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE BlockArguments #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Control.Monad.State (StateL(..), StateR(..)) where
+
+import Control.Arrow (first, second)
+
+---------------------------------------------------------------------------
+
+-- * STATE LEFT
+-- * STATE RIGHT
+
+---------------------------------------------------------------------------
+-- STATE LEFT
+---------------------------------------------------------------------------
+
+newtype StateL s a = StateL { runStateL :: s -> (a, s) }
+
+instance Functor (StateL s) where f `fmap` StateL k = StateL $ (f `first`) . k
+
+instance Applicative (StateL s) where
+	pure = StateL . (,)
+	StateL kf <*> mx =
+		StateL \s -> let (f, s') = kf s in (f <$> mx) `runStateL` s'
+
+instance Monad (StateL s) where
+	StateL k >>= f = StateL \s -> let (x, s') = k s in f x `runStateL` s'
+
+---------------------------------------------------------------------------
+-- STATE RIGHT
+---------------------------------------------------------------------------
+
+newtype StateR s a = StateR { runStateR :: s -> (s, a) }
+
+instance Functor (StateR s) where f `fmap` StateR k = StateR $ (f `second`) . k
+
+instance Applicative (StateR s) where
+	pure = StateR . flip (,)
+	StateR kf <*> mx =
+		StateR \s -> let (s', f) = kf s in (f <$> mx) `runStateR` s'
+
+instance Monad (StateR s) where
+	StateR k >>= f = StateR \s -> let (s', x) = k s in f x `runStateR` s'
diff --git a/src/Data/List/Length.hs b/src/Data/List/Length.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Length.hs
@@ -0,0 +1,187 @@
+{-# LANGUAGE BlockArguments, TupleSections #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.List.Length (
+	-- * LENGTHED LIST LEFT
+	-- ** Type
+	LengthL, RangeL(NilL, (:.)),
+	-- ** AddL
+	AddL, (++.),
+	-- ** Unfoldr
+	-- *** class
+	Unfoldr,
+	-- *** without monad
+	repeatL, fillL, unfoldr, unfoldrWithBase,
+	-- *** with monad
+	unfoldrM, unfoldrMWithBase,
+	-- ** ZipL
+	ZipL, zipL, zipWithL, zipWithML,
+	-- ** ListToLengthL
+	ListToLengthL, splitL, chunksL, chunksL',
+	-- * LENGTHED LIST RIGHT
+	-- ** Type
+	LengthR, RangeR(NilR, (:+)),
+	-- ** AddR
+	AddR, (+++),
+	-- ** Unfoldl
+	-- *** class
+	Unfoldl,
+	-- *** without monad
+	repeatR, fillR, unfoldl, unfoldlWithBase,
+	-- *** with monad
+	unfoldlM, unfoldlMWithBase,
+	-- ** ZipR
+	ZipR, zipR, zipWithR, zipWithMR,
+	-- ** ListToLengthR
+	ListToLengthR, listToLengthR, chunksR, chunksR',
+	-- * LEFT TO RIGHT
+	LeftToRight, (++.+), leftToRight,
+	-- * RIGHT TO LEFT
+	RightToLeft, (++..), rightToLeft ) where
+
+import GHC.TypeNats (type (-))
+import Control.Arrow (first, (***))
+import Data.List.Range (
+	RangeL(..), AddL, (++.), LoosenLMax, loosenLMax, Unfoldr,
+	ZipL, zipL, zipWithL, zipWithML,
+	RangeR(..), AddR, (+++), LoosenRMax, loosenRMax, Unfoldl,
+	ZipR, zipR, zipWithR, zipWithMR,
+	LeftToRight, (++.+), leftToRight, RightToLeft, (++..), rightToLeft )
+import Data.List.Length.LengthL (
+	LengthL, unfoldr, unfoldrWithBase, unfoldrM, unfoldrMWithBase,
+	ListToLengthL, splitL )
+import Data.List.Length.LengthR (
+	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,
+	ListToLengthR, listToLengthR )
+
+---------------------------------------------------------------------------
+
+-- LENGTH LEFT
+-- LENGTH RIGHT
+
+---------------------------------------------------------------------------
+-- LENGTH LEFT
+---------------------------------------------------------------------------
+
+repeatL :: Unfoldr 0 n n => a -> LengthL n a
+repeatL = fillL NilL
+
+{-^
+
+To repeat a value of type @a@ to construct a list of type @LengthL n a@.
+
+>>> :set -XDataKinds
+>>> repeatL 'c' :: LengthL 5 Char
+'c' :. ('c' :. ('c' :. ('c' :. ('c' :. NilL))))
+
+-}
+
+fillL :: Unfoldr n m m => RangeL n m a -> a -> LengthL m a
+fillL = (`unfoldrWithBase` \x -> (x, x))
+
+{-^
+
+To fill a list of type @LengthL n a@ with a value of type @a@.
+
+>>> :set -XDataKinds
+>>> fillL ('a' :. 'b' :.. NilL) 'c' :: LengthL 5 Char
+'a' :. ('b' :. ('c' :. ('c' :. ('c' :. NilL))))
+
+-}
+
+chunksL :: ListToLengthL n => [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
+chunksL = either ([] ,) (uncurry first . ((:) *** chunksL)) . splitL
+
+{-^
+
+To separate a list to multiple lengthed lists.
+It return separeted lengthed lists and a not enough length fragment.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> chunksL @3 "foo bar"
+(['f' :. ('o' :. ('o' :. NilL)),' ' :. ('b' :. ('a' :. NilL))],'r' :.. NilL)
+
+-}
+
+chunksL' :: (Unfoldr 0 n n, LoosenLMax 0 (n - 1) n, ListToLengthL n) =>
+	a -> [a] -> [LengthL n a]
+chunksL' z xs = case chunksL xs of
+	(cs, NilL) -> cs; (cs, rs) -> cs ++ [loosenLMax rs `fillL` z]
+
+{-^
+
+It is like chunksL.
+But if there is a not enough length fragment, then it fill with a default value.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> print `mapM_` chunksL' @3 '@' "foo bar"
+'f' :. ('o' :. ('o' :. NilL))
+' ' :. ('b' :. ('a' :. NilL))
+'r' :. ('@' :. ('@' :. NilL))
+
+-}
+
+---------------------------------------------------------------------------
+-- LENGTH RIGHT
+---------------------------------------------------------------------------
+
+repeatR :: Unfoldl 0 n n => a -> LengthR n a
+repeatR = (`fillR` NilR)
+
+{-^
+
+To repeat a value of type @a@ to construct a list of type @LengthR n a@.
+
+>>> :set -XDataKinds
+>>> repeatR 'c' :: LengthR 5 Char
+((((NilR :+ 'c') :+ 'c') :+ 'c') :+ 'c') :+ 'c'
+
+-}
+
+fillR :: Unfoldl n m m => a -> RangeR n m a -> LengthR m a
+fillR = unfoldlWithBase \x -> (x, x)
+
+{-^
+
+To fill a list of type @LengthR n a@ with a default value.
+
+>>> :set -XDataKinds
+>>> fillR 'c' (NilR :++ 'a' :+ 'b') :: LengthR 5 Char
+((((NilR :+ 'c') :+ 'c') :+ 'c') :+ 'a') :+ 'b'
+
+-}
+
+chunksR :: ListToLengthR n => [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
+chunksR = either ([] ,) (uncurry first . ((:) *** chunksR)) . listToLengthR
+
+{-^
+
+To separate a list to multiple lengthed lists.
+It return separated lengthed lists and a not enough length fragment.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> chunksR @3 "foo bar"
+([((NilR :+ 'o') :+ 'o') :+ 'f',((NilR :+ 'a') :+ 'b') :+ ' '],NilR :++ 'r')
+
+-}
+
+chunksR' :: (Unfoldl 0 n n, LoosenRMax 0 (n - 1) n, ListToLengthR n) =>
+	a -> [a] -> [LengthR n a]
+chunksR' z xs = case chunksR xs of
+	(cs, NilR) -> cs; (cs, rs) -> cs ++ [z `fillR` loosenRMax rs]
+
+{-^
+
+It is like @chunksR@.
+But if there is a not enough length fragment, then it fill with a default value.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> print `mapM_` chunksR' @3 '@' "foo bar"
+((NilR :+ 'o') :+ 'o') :+ 'f'
+((NilR :+ 'a') :+ 'b') :+ ' '
+((NilR :+ '@') :+ '@') :+ 'r'
+
+-}
diff --git a/src/Data/List/Length/LengthL.hs b/src/Data/List/Length/LengthL.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Length/LengthL.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.List.Length.LengthL (
+	LengthL, unfoldr, unfoldrWithBase, unfoldrM, unfoldrMWithBase,
+	ListToLengthL, splitL ) where
+
+import GHC.TypeNats (type (-), type (<=))
+import Control.Arrow (first, (+++))
+import Control.Monad.State (StateL(..))
+import Data.List.Range.RangeL (LengthL, RangeL(..), Unfoldr, unfoldrMRangeWithBase)
+
+---------------------------------------------------------------------------
+
+-- * TYPE
+-- * UNFOLDR
+-- * LIST TO LENGTH LEFT
+
+---------------------------------------------------------------------------
+-- TYPE
+---------------------------------------------------------------------------
+
+---------------------------------------------------------------------------
+-- UNFOLDR
+---------------------------------------------------------------------------
+
+unfoldr :: Unfoldr 0 n n => (s -> (a, s)) -> s -> LengthL n a
+unfoldr = unfoldrWithBase NilL
+
+{-^
+
+To evaluate function repeatedly to construct a list of type @LengthL n a@.
+The function recieve a state and return an element value and a new state.
+
+>>> :set -XDataKinds
+>>> unfoldr (\n -> (2 * n, n + 1)) 0 :: LengthL 5 Integer
+0 :. (2 :. (4 :. (6 :. (8 :. NilL))))
+
+-}
+
+unfoldrWithBase ::
+	Unfoldr n m m => RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
+unfoldrWithBase xs = (fst .) . runStateL . unfoldrMWithBase xs . StateL
+
+{-^
+
+It is like @unfoldr@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
+>>> unfoldrWithBase xs (\n -> (2 * n, n + 1)) 0 :: LengthL 5 Integer
+123 :. (456 :. (0 :. (2 :. (4 :. NilL))))
+
+-}
+
+unfoldrM :: (Monad m, Unfoldr 0 n n) => m a -> m (LengthL n a)
+unfoldrM = unfoldrMWithBase NilL
+
+{-^
+
+It is like @unfoldr@. But it use a monad as an argument instead of a function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n +1)
+>>> unfoldrM count :: IO (LengthL 5 Integer)
+1 :. (2 :. (3 :. (4 :. (5 :. NilL))))
+
+-}
+
+unfoldrMWithBase ::
+	(Monad m, Unfoldr n w w) => RangeL n w a -> m a -> m (LengthL w a)
+unfoldrMWithBase = (`unfoldrMRangeWithBase` undefined)
+
+{-^
+
+It is like @unfoldrM@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)
+>>> unfoldrMWithBase (123 :. 456 :.. NilL) count :: IO (LengthL 5 Integer)
+123 :. (456 :. (1 :. (2 :. (3 :. NilL))))
+
+-}
+
+---------------------------------------------------------------------------
+-- LIST TO LENGTH LEFT
+---------------------------------------------------------------------------
+
+class ListToLengthL n where
+	splitL :: [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
+
+	{-^
+
+	To take a lengthed list from a list.
+	If an original list has not enough elements, then it return
+	a left value.
+
+	>>> :set -XTypeApplications -XDataKinds
+	>>> splitL @4 "Hi!"
+	Left ('H' :.. ('i' :.. ('!' :.. NilL)))
+	>>> splitL @4 "Hello!"
+	Right ('H' :. ('e' :. ('l' :. ('l' :. NilL))),"o!")
+
+	-}
+
+instance ListToLengthL 1 where
+	splitL = \case [] -> Left NilL; x : xs -> Right (x :. NilL, xs)
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, 1 <= (n - 1), ListToLengthL (n - 1)) => ListToLengthL n where
+	splitL = \case
+		[] -> Left NilL
+		x : xs -> (x :..) +++ ((x :.) `first`) $ splitL xs
diff --git a/src/Data/List/Length/LengthR.hs b/src/Data/List/Length/LengthR.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Length/LengthR.hs
@@ -0,0 +1,131 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.List.Length.LengthR (
+	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,
+	ListToLengthR, listToLengthR ) where
+
+import GHC.TypeNats (type (-), type (<=))
+import Control.Arrow (first, (+++))
+import Control.Monad.State (StateR(..))
+import Data.List.Range.RangeR (RangeR(..), Unfoldl, unfoldlMRangeWithBase)
+
+---------------------------------------------------------------------------
+
+-- TYPE
+-- UNFOLDL
+-- LIST TO LENGTH RIGHT
+
+---------------------------------------------------------------------------
+-- TYPE
+---------------------------------------------------------------------------
+
+type LengthR n = RangeR n n
+
+{-^
+
+@LengthR n a@ is a list which have just n members of type @a@.
+You can push and pop an element from right.
+
+>>> :set -XDataKinds
+>>> sampleLengthR = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o' :: LengthR 5 Char
+
+-}
+
+---------------------------------------------------------------------------
+-- UNFOLDL
+---------------------------------------------------------------------------
+
+unfoldl :: Unfoldl 0 n n => (s -> (s, a)) -> s -> LengthR n a
+unfoldl f s = unfoldlWithBase f s NilR
+
+{-^
+
+To eveluate function repeatedly to construct a list of type @LengthR n a@.
+The function recieve a state and return a new state and an element value.
+
+>>> :set -XDataKinds
+>>> unfoldl (\n -> (n + 1, 2 * n)) 0 :: LengthR 5 Integer
+((((NilR :+ 8) :+ 6) :+ 4) :+ 2) :+ 0
+
+-}
+
+unfoldlWithBase ::
+	Unfoldl n m m => (s -> (s, a)) -> s -> RangeR n m a -> LengthR m a
+unfoldlWithBase f = (snd .) . flip (runStateR . unfoldlMWithBase (StateR f))
+
+{-^
+
+It is like @unfoldl@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
+>>> unfoldlWithBase (\n -> (n + 1, 2 * n)) 0 xs :: LengthR 5 Integer
+((((NilR :+ 4) :+ 2) :+ 0) :+ 123) :+ 456
+
+-}
+
+unfoldlM :: (Monad m, Unfoldl 0 n n) => m a -> m (LengthR n a)
+unfoldlM = (`unfoldlMWithBase` NilR)
+
+{-^
+
+It is like @unfoldl@. But it use monad as an argument instead of function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)
+>>> unfoldlM count :: IO (LengthR 5 Integer)
+((((NilR :+ 5) :+ 4) :+ 3) :+ 2) :+ 1
+
+-}
+
+unfoldlMWithBase ::
+	(Monad m, Unfoldl n w w) => m a -> RangeR n w a -> m (LengthR w a)
+unfoldlMWithBase = unfoldlMRangeWithBase undefined
+
+{-^
+
+It is like @unfoldlM@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)
+>>> unfoldlMWithBase count (NilR :++ 123 :+ 456) :: IO (LengthR 5 Integer)
+((((NilR :+ 3) :+ 2) :+ 1) :+ 123) :+ 456
+
+-}
+
+---------------------------------------------------------------------------
+-- LIST TO LENGTH RIGHT
+---------------------------------------------------------------------------
+
+class ListToLengthR n where
+	listToLengthR :: [a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
+
+	{-^
+
+	To take a lengthed list from a list.
+	If an original list has not enough elements, then it return a left value.
+
+	>>> :set -XTypeApplications -XDataKinds
+	>>> listToLengthR @4 "Hi!"
+	Left (((NilR :++ '!') :++ 'i') :++ 'H')
+	>>> listToLengthR @4 "Hello!"
+	Right ((((NilR :+ 'l') :+ 'l') :+ 'e') :+ 'H',"o!")
+
+	-}
+
+instance ListToLengthR 1 where
+	listToLengthR = \case [] -> Left NilR; x : xs -> Right (NilR :+ x, xs)
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, 1 <= (n - 1), ListToLengthR (n - 1)) => ListToLengthR n where
+	listToLengthR = \case
+		[] -> Left NilR
+		x : xs -> (:++ x) +++ ((:+ x) `first`) $ listToLengthR xs
diff --git a/src/Data/List/Range.hs b/src/Data/List/Range.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Range.hs
@@ -0,0 +1,372 @@
+{-# LANGUAGE BlockArguments, LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# OPTIOnS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+module Data.List.Range (
+	-- * RANGED LIST LEFT
+	module Data.List.Range.RangeL,
+	-- ** Repeat and Unfoldr Min and Max
+	-- *** repeat
+	repeatLMin, repeatLMax,
+	-- *** unfoldr
+	unfoldrMin, unfoldrMax,
+	-- *** unfoldrM
+	unfoldrMMin, unfoldrMMax,
+	-- * RANGED LIST RIGHT
+	module Data.List.Range.RangeR,
+	-- ** Repeat and Unfoldl Min and Max
+	-- *** repeat
+	repeatRMin, repeatRMax,
+	-- *** unfoldl
+	unfoldlMin, unfoldlMax,
+	-- *** unfoldlM
+	unfoldlMMin, unfoldlMMax,
+	-- * LEFT TO RIGHT
+	LeftToRight, (++.+), leftToRight,
+	-- * RIGHT TO LEFT
+	RightToLeft, (++..), rightToLeft ) where
+
+import GHC.TypeNats (type (+), type (-), type (<=))
+import Data.List.Length.LengthL (unfoldr, unfoldrM)
+import Data.List.Length.LengthR (unfoldl, unfoldlM)
+import Data.List.Range.RangeL
+import Data.List.Range.RangeR
+
+---------------------------------------------------------------------------
+
+-- * RANGED LIST LEFT
+--	+ MIN
+--	+ MAX
+-- * RANGED LIST RIGHT
+--	+ MIN
+--	+ MAX
+-- * LEFT TO RIGHT
+--	+ CLASS
+--	+ INSTANCE
+--	+ FUNCTION
+-- * RIGHT TO LEFT
+--	+ CLASS
+--	+ INSTANCE
+--	+ FUNCTION
+
+---------------------------------------------------------------------------
+-- RANGED LIST LEFT
+---------------------------------------------------------------------------
+
+-- MIN
+
+repeatLMin :: (LoosenLMax n n m, Unfoldr 0 n n) => a -> RangeL n m a
+repeatLMin = unfoldrMin \x -> (x, x)
+
+{-^
+
+To repeat a value minimum number of times.
+
+>>> :set -XDataKinds
+>>> repeatLMin 123 :: RangeL 3 5 Integer
+123 :. (123 :. (123 :. NilL))
+
+-}
+
+unfoldrMin ::
+	(LoosenLMax n n m, Unfoldr 0 n n) => (s -> (a, s)) -> s -> RangeL n m a
+unfoldrMin f = loosenLMax . unfoldr f
+
+{-^
+
+To evaluate a function to construct values minimum number of times.
+The function recieve a state and return a value and a new state.
+
+>>> :set -XDataKinds
+>>> unfoldrMin (\n -> (n * 3, n + 1)) 1 :: RangeL 3 5 Integer
+3 :. (6 :. (9 :. NilL))
+
+-}
+
+unfoldrMMin ::
+	(Monad m, LoosenLMax n n w, Unfoldr 0 n n) => m a -> m (RangeL n w a)
+unfoldrMMin f = loosenLMax <$> unfoldrM f
+
+{-^
+
+It is like @unfoldrMin@. But it use a monad instead of a function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldrMMin count :: IO (RangeL 3 5 Integer)
+3 :. (6 :. (9 :. NilL))
+
+-}
+
+-- MAX
+
+repeatLMax :: (LoosenLMin m m n, Unfoldr 0 m m) => a -> RangeL n m a
+repeatLMax = unfoldrMax \x -> (x, x)
+
+{-^
+
+To repeat a value maximum number of times.
+
+>>> :set -XDataKinds
+>>> repeatLMax 123 :: RangeL 3 5 Integer
+123 :. (123 :. (123 :. (123 :.. (123 :.. NilL))))
+
+-}
+
+unfoldrMax ::
+	(LoosenLMin m m n, Unfoldr 0 m m) => (s -> (a, s)) -> s -> RangeL n m a
+unfoldrMax f = loosenLMin . unfoldr f
+
+{-^
+
+To evaluate a function to construct values maximum number of times.
+The function recieve a state and return a value and a new state.
+
+>>> :set -XDataKinds
+>>> unfoldrMax (\n -> (n * 3, n + 1)) 1 :: RangeL 3 5 Integer
+3 :. (6 :. (9 :. (12 :.. (15 :.. NilL))))
+
+-}
+
+unfoldrMMax ::
+	(Monad m, LoosenLMin w w n, Unfoldr 0 w w) => m a -> m (RangeL n w a)
+unfoldrMMax f = loosenLMin <$> unfoldrM f
+
+{-^
+
+It is like @unfoldrMax@. But it use a monad instead of a function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldrMMax count :: IO (RangeL 3 5 Integer)
+3 :. (6 :. (9 :. (12 :.. (15 :.. NilL))))
+
+-}
+
+---------------------------------------------------------------------------
+-- RANGED LIST RIGHT
+---------------------------------------------------------------------------
+
+-- MIN
+
+repeatRMin :: (LoosenRMax n n m, Unfoldl 0 n n) => a -> RangeR n m a
+repeatRMin = unfoldlMin \x -> (x, x)
+
+{-^
+
+To repeat a value minimum number of times.
+
+>>> :set -XDataKinds
+>>> repeatRMin 123 :: RangeR 3 5 Integer
+((NilR :+ 123) :+ 123) :+ 123
+
+-}
+
+unfoldlMin ::
+	(LoosenRMax n n m, Unfoldl 0 n n) => (s -> (s, a)) -> s -> RangeR n m a
+unfoldlMin f = loosenRMax . unfoldl f
+
+{-^
+
+To evaluate a function to construct values minimum number of times.
+The function recieves a state and return a value and a new state.
+
+>>> :set -XDataKinds
+>>> unfoldlMin (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Integer
+((NilR :+ 9) :+ 6) :+ 3
+
+-}
+
+unfoldlMMin ::
+	(Monad m, LoosenRMax n n w, Unfoldl 0 n n) => m a -> m (RangeR n w a)
+unfoldlMMin f = loosenRMax <$> unfoldlM f
+
+{-^
+
+It is like @unfoldlMax@. But it uses a monad instead of a function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldlMMin count :: IO (RangeR 3 5 Integer)
+((NilR :+ 9) :+ 6) :+ 3
+
+-}
+
+-- MAX
+
+repeatRMax :: (LoosenRMin m m n, Unfoldl 0 m m) => a -> RangeR n m a
+repeatRMax = unfoldlMax \x -> (x, x)
+
+{-^
+
+To repeat a value maximum number of times.
+
+>>> :set -XDataKinds
+>>> repeatRMax 123 :: RangeR 3 5 Integer
+((((NilR :++ 123) :++ 123) :+ 123) :+ 123) :+ 123
+
+-}
+
+unfoldlMax ::
+	(LoosenRMin m m n, Unfoldl 0 m m) => (s -> (s, a)) -> s -> RangeR n m a
+unfoldlMax f = loosenRMin . unfoldl f
+
+{-^
+
+To eveluate a function to construct values maximum number of times.
+The function recieves a state and return a value and a new state.
+
+>>> :set -XDataKinds
+>>> unfoldlMax (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Integer
+((((NilR :++ 15) :++ 12) :+ 9) :+ 6) :+ 3
+
+-}
+
+unfoldlMMax ::
+	(Monad m, LoosenRMin w w n, Unfoldl 0 w w) => m a -> m (RangeR n w a)
+unfoldlMMax f = loosenRMin <$> unfoldlM f
+
+{-^
+
+It is like @unfoldlMax@. But it uses a monad instead of function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldlMMax count :: IO (RangeR 3 5 Integer)
+((((NilR :++ 15) :++ 12) :+ 9) :+ 6) :+ 3
+
+-}
+
+---------------------------------------------------------------------------
+-- LEFT TO RIGHT
+---------------------------------------------------------------------------
+
+-- CLASS
+
+infixl 5 ++.+
+
+class LeftToRight n m v w where
+	(++.+) :: RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
+
+	{-^
+
+	To concatenate a right-list and a left-list and return a right-list.
+
+	>>> :set -XDataKinds
+	>>> sampleLeftToRight1 = NilR :++ 'f' :++ 'o' :+ 'o' :: RangeR 1 4 Char
+	>>> sampleLeftToRight2 = 'b' :. 'a' :. 'r' :.. NilL :: RangeL 2 3 Char
+	>>> sampleLeftToRight1 ++.+ sampleLeftToRight2
+	(((((NilR :++ 'f') :++ 'o') :++ 'o') :+ 'b') :+ 'a') :+ 'r'
+	>>> :type sampleLeftToRight1 ++.+ sampleLeftToRight2
+	sampleLeftToRight1 ++.+ sampleLeftToRight2 :: RangeR 3 7 Char
+
+	-}
+
+-- INSTANCE
+
+instance LeftToRight n m 0 0 where n ++.+ _ = n
+
+instance {-# OVERLAPPABLE #-} (
+	PushR (n - 1) (m - 1), LoosenRMax n m (m + w),
+	LeftToRight n (m + 1) 0 (w - 1) ) => LeftToRight n m 0 w where
+	(++.+) n = \case NilL -> loosenRMax n; x :.. v -> n .:++ x ++.+ v
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= v, LeftToRight (n + 1) (m + 1) (v - 1) (w - 1)) =>
+	LeftToRight n m v w where
+	(++.+) :: forall a .
+		RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
+	n ++.+ x :. v = (n :+ x :: RangeR (n + 1) (m + 1) a) ++.+ v
+
+-- FUNCTION
+
+leftToRight ::
+	forall v w a . LeftToRight 0 0 v w => RangeL v w a -> RangeR v w a
+leftToRight = ((NilR :: RangeR 0 0 a) ++.+)
+
+{-^
+
+To convert a left-list to a right-list.
+
+>>> :set -XDataKinds -fno-warn-tabs
+>>> :{
+	sampleLeftToRight :: RangeL 3 8 Char
+	sampleLeftToRight = 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL
+:}
+
+>>> leftToRight sampleLeftToRight
+((((NilR :++ 'h') :++ 'e') :+ 'l') :+ 'l') :+ 'o'
+
+-}
+
+---------------------------------------------------------------------------
+-- RIGHT TO LEFT
+---------------------------------------------------------------------------
+
+-- CLASS
+
+infixr 5 ++..
+
+class RightToLeft n m v w where
+	(++..) :: RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
+
+	{-^
+
+	To concatenate a right-list and a left-list and return a left-list.
+
+	>>> :set -XDataKinds
+	>>> sampleRightToLeft1 = NilR :++ 'f' :++ 'o' :+ 'o' :: RangeR 1 4 Char
+	>>> sampleRightToLeft2 = 'b' :. 'a' :. 'r' :.. NilL :: RangeL 2 3 Char
+	>>> sampleRightToLeft1 ++.. sampleRightToLeft2
+	'f' :. ('o' :. ('o' :. ('b' :.. ('a' :.. ('r' :.. NilL)))))
+
+	-}
+
+-- INSTANCE
+
+instance RightToLeft 0 0 v w where _ ++.. v = v
+
+instance {-# OVERLAPPABLE #-} (
+	PushL (v - 1) (w - 1), LoosenLMax v w (m + w),
+	RightToLeft 0 (m - 1) v (w + 1) ) => RightToLeft 0 m v w where
+	(++..) = \case NilR -> loosenLMax; n :++ x -> (n ++..) . (x .:..)
+
+instance {-# OVERLAPPABLE #-} (
+	1 <= n, RightToLeft (n - 1) (m - 1) (v + 1) (w + 1) ) =>
+	RightToLeft n m v w where
+	(++..) :: forall a .
+		RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
+	n :+ x ++.. v = n ++.. (x :. v :: RangeL (v + 1) (w + 1) a)
+
+-- FUNCTION
+
+rightToLeft ::
+	forall n m a . RightToLeft n m 0 0 => RangeR n m a -> RangeL n m a
+rightToLeft = (++.. (NilL :: RangeL 0 0 a))
+
+{-^
+
+To convert a right-list to a left-list.
+
+>>> :set -XDataKinds
+>>> :{
+	sampleRightToLeft :: RangeR 3 8 Char
+	sampleRightToLeft = NilR :++ 'h' :++ 'e' :+ 'l' :+ 'l' :+ 'o'
+:}
+
+>>> rightToLeft sampleRightToLeft
+'h' :. ('e' :. ('l' :. ('l' :.. ('o' :.. NilL))))
+
+-}
diff --git a/src/Data/List/Range/Nat.hs b/src/Data/List/Range/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Range/Nat.hs
@@ -0,0 +1,152 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.List.Range.Nat (
+	-- * RangedNatL
+	RangedNatL, natL, toIntL, fromIntL, splitAtL,
+	-- * RangedNatR
+	RangedNatR, natR, toIntR, fromIntR, splitAtR ) where
+
+import GHC.TypeNats (type (-))
+import Data.Bool (bool)
+import Data.List.Length (repeatL, repeatR)
+import Data.List.Range (
+	RangeL, Unfoldr, unfoldrRangeMaybe, ZipL, zipWithL,
+	RangeR, Unfoldl, unfoldlRangeMaybe, ZipR, zipWithR )
+
+---------------------------------------------------------------------------
+
+-- * RANGED NAT LEFT
+-- * RANGED NAT RIGHT
+
+---------------------------------------------------------------------------
+-- RANGED NAT LEFT
+---------------------------------------------------------------------------
+
+type RangedNatL n m = RangeL n m ()
+
+natL :: Unfoldr 0 n n => RangedNatL n n
+natL = repeatL ()
+
+{-^
+
+To make @RangedNatL@.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> :module + Data.List.Range
+>>> loosenL (natL @5) :: RangedNatL 3 8
+() :. (() :. (() :. (() :.. (() :.. NilL))))
+
+-}
+
+toIntL :: Foldable (RangeL n m) => RangedNatL n m -> Int
+toIntL = length
+
+{-^
+
+To convert from @RangedNatL@ to @Int@.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> :module + Data.List.Range
+>>> toIntL (loosenL (natL @5) :: RangedNatL 3 8)
+5
+
+-}
+
+fromIntL :: Unfoldr 0 n m => Int -> Maybe (RangedNatL n m)
+fromIntL = unfoldrRangeMaybe \s -> bool Nothing (Just ((), s - 1)) (s > 0)
+
+{-^
+
+To convert from @Int@ to @RangedNatL@.
+
+>>> :set -XDataKinds
+>>> fromIntL 5 :: Maybe (RangedNatL 3 8)
+Just (() :. (() :. (() :. (() :.. (() :.. NilL)))))
+
+-}
+
+splitAtL :: ZipL n m v w => RangedNatL n m ->
+	RangeL v w a -> (RangeL n m a, RangeL (v - m) (w - n) a)
+splitAtL = zipWithL $ flip const
+
+{-^
+
+To split a list at position which is specified by number.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> :module + Data.List.Range
+>>> xs = 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL :: RangeL 3 8 Char
+>>> splitAtL (natL @2) xs
+('h' :. ('e' :. NilL),'l' :. ('l' :.. ('o' :.. NilL)))
+>>> :type splitAtL (natL @2) xs
+splitAtL (natL @2) xs :: (RangeL 2 2 Char, RangeL 1 6 Char)
+
+-}
+
+---------------------------------------------------------------------------
+-- RANGED NAT RIGHT
+---------------------------------------------------------------------------
+
+type RangedNatR n m = RangeR n m ()
+
+natR :: Unfoldl 0 n n => RangedNatR n n
+natR = repeatR ()
+
+{-^
+
+To make @RangedNatR@.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> :module + Data.List.Range
+>>> loosenR (natR @5) :: RangedNatR 3 8
+((((NilR :++ ()) :++ ()) :+ ()) :+ ()) :+ ()
+
+-}
+
+toIntR :: Foldable (RangeR n m) => RangedNatR n m -> Int
+toIntR = length
+
+{-^
+
+To convert from @RangedNatR@ to @Int@.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> :module + Data.List.Range
+>>> toIntR (loosenR (natR @5) :: RangedNatR 3 8)
+5
+
+-}
+
+fromIntR :: Unfoldl 0 n m => Int -> Maybe (RangedNatR n m)
+fromIntR = unfoldlRangeMaybe \s -> bool Nothing (Just (s - 1, ())) (s > 0)
+
+{-^
+
+To convert @Int@ to @RangedNatR@.
+
+>>> :set -XDataKinds
+>>> fromIntR 5 :: Maybe (RangedNatR 3 8)
+Just (((((NilR :++ ()) :++ ()) :+ ()) :+ ()) :+ ())
+
+-}
+
+splitAtR :: ZipR n m v w => RangeR n m a ->
+	RangedNatR v w -> (RangeR (n - w) (m - v) a, RangeR v w a)
+splitAtR = zipWithR const
+
+{-^
+
+To split a list at position which is specified by number.
+
+>>> :set -XTypeApplications -XDataKinds
+>>> :module + Data.List.Range
+>>> xs = NilR :++ 'h' :++ 'e' :+ 'l' :+ 'l' :+ 'o' :: RangeR 3 8 Char
+>>> splitAtR xs (natR @2)
+(((NilR :++ 'h') :++ 'e') :+ 'l',(NilR :+ 'l') :+ 'o')
+>>> :type splitAtR xs (natR @2)
+splitAtR xs (natR @2) :: (RangeR 1 6 Char, RangeR 2 2 Char)
+
+-}
diff --git a/src/Data/List/Range/RangeL.hs b/src/Data/List/Range/RangeL.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Range/RangeL.hs
@@ -0,0 +1,643 @@
+{-# LANGUAGE BlockArguments, LambdaCase, TupleSections #-}
+{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
+{-# LANGUAGE GADTs, TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+module Data.List.Range.RangeL (
+	LengthL,
+	-- ** Type
+	RangeL(..),
+	-- ** PushL
+	PushL, (.:..),
+	-- ** AddL
+	AddL, (++.),
+	-- ** LoosenLMin and LoosenLMax
+	-- *** loosenL
+	loosenL,
+	-- *** loosenLMin
+	LoosenLMin, loosenLMin,
+	-- *** loosenLMax
+	LoosenLMax, loosenLMax,
+	-- ** Unfoldr
+	-- *** class
+	Unfoldr,
+	-- *** unfoldrRange
+	-- **** without monad
+	unfoldrRange, unfoldrRangeWithBase, unfoldrRangeWithBaseWithS,
+	-- **** with monad
+	unfoldrMRange, unfoldrMRangeWithBase,
+	-- *** unfoldrRangeMaybe
+	-- **** without monad
+	unfoldrRangeMaybe, unfoldrRangeMaybeWithBase,
+	-- **** with monad
+	unfoldrMRangeMaybe, unfoldrMRangeMaybeWithBase,
+	-- ** ZipL
+	ZipL, zipL, zipWithL, zipWithML ) where
+
+import GHC.TypeNats (Nat, type (+), type (-), type (<=))
+import GHC.Exts (IsList(..))
+import Control.Arrow (first, second, (***), (&&&))
+import Control.Monad.Identity (Identity(..))
+import Control.Monad.State (StateL(..))
+import Data.Foldable (toList)
+import Data.Bool (bool)
+import Data.Maybe (isJust, fromMaybe)
+import Data.String
+
+type LengthL n = RangeL n n
+
+{-^
+
+The value of @LengthL n a@ is a list which have just @n@ members of type @a@.
+You can push and pop an element from left.
+
+>>> :set -XDataKinds
+>>> sampleLengthL = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :. NilL :: LengthL 5 Char
+
+-}
+
+---------------------------------------------------------------------------
+
+-- * TYPE
+--	+ RANGE LEFT
+--	+ INSTANCE FUNCTOR
+--	+ INSTANCE FOLDABLE
+-- * PUSH
+-- * ADD
+-- * LOOSEN
+-- 	+ LOOSEN LEFT
+-- 	+ LOOSEN LEFT MIN
+-- 	+ LOOSEN LEFT MAX
+-- * UNFOLDR
+-- 	+ CLASS
+-- 	+ INSTANCE
+-- 	+ UNFOLDR RANGE
+-- 	+ UNFOLDR RANGE MAYBE
+-- * ZIP
+--	+ CLASS
+--	+ FUNCTION
+
+---------------------------------------------------------------------------
+-- TYPE
+---------------------------------------------------------------------------
+
+-- RANGE LEFT
+
+data RangeL :: Nat -> Nat -> * -> * where
+	NilL :: 0 <= m => RangeL 0 m a
+	(:..) :: 1 <= m => a -> RangeL 0 (m - 1) a -> RangeL 0 m a
+	(:.) :: (1 <= n, 1 <= m) =>
+		a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
+
+{-^
+
+The value of @RangeL n m a@ is a list of type @a@ values whose element number is
+at minimum @n@, and at maximum @m@.
+You can push and pop an element from left.
+
+>>> :set -XDataKinds
+>>> sampleRangeL = 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL :: RangeL 3 8 Char
+
+-}
+
+infixr 6 :., :..
+
+deriving instance Show a => Show (RangeL n m a)
+
+-- INSTANCE FUNCTOR
+
+instance Functor (RangeL 0 0) where _ `fmap` NilL = NilL
+
+instance {-# OVERLAPPABLE #-}
+	Functor (RangeL 0 (m - 1)) => Functor (RangeL 0 m) where
+	fmap f = \case NilL -> NilL; x :.. xs -> f x :.. (f <$> xs)
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, Functor (RangeL (n - 1) (m - 1))) => Functor (RangeL n m) where
+	f `fmap` (x :. xs) = f x :. (f <$> xs)
+
+-- INSTANCE FOLDABLE
+
+instance Foldable (RangeL 0 0) where foldr _ z NilL = z
+
+instance {-# OVERLAPPABLE #-}
+	Foldable (RangeL 0 (m - 1)) => Foldable (RangeL 0 m) where
+	foldr (-<) z = \case NilL -> z; x :.. xs -> x -< foldr (-<) z xs
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Foldable (RangeL (n - 1) (m - 1))) =>
+	Foldable (RangeL n m) where
+	foldr (-<) z (x :. xs) = x -< foldr (-<) z xs
+
+instance Applicative (LengthL 0) where pure _ = NilL; _ <*> _ = NilL
+
+instance {-# OVERLAPPABLE #-} (Functor (RangeL 0 m), Applicative (RangeL 0 (m - 1)), Unfoldr 0 0 m) => Applicative (RangeL 0 m) where
+	pure = unfoldrRange (const True) (\x -> (x, x))
+	NilL <*> _ = NilL
+	_ <*> NilL = NilL
+	f :.. fs <*> x :.. xs = f x :.. (fs <*> xs)
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeL n m), Applicative (RangeL (n - 1) (m - 1)), Unfoldr 0 n m) => Applicative (RangeL n m) where
+	pure = unfoldrRange (const True) (\x -> (x, x))
+	f :. fs <*> x :. xs = f x :. (fs <*> xs)
+
+instance Applicative (LengthL 0) => Monad (LengthL 0) where
+	NilL >>= _ = NilL
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (LengthL n), Monad (LengthL (n - 1))) => Monad (LengthL n) where
+	x :. xs >>= f = y :. (xs >>= \z -> case f z of _ :. zs -> zs)
+		where y :. _ = f x
+
+-- INSTANCE ISSTRING
+
+instance Unfoldr 0 n m => IsString (RangeL n m Char) where
+	fromString s = fromMaybe (error $ "The string " ++ show s ++ " is not within range.")
+		$ unfoldrRangeMaybe (\case "" -> Nothing; c : cs -> Just (c, cs)) s
+
+instance (Foldable (RangeL n m), Unfoldr 0 n m) => IsList (RangeL n m a) where
+	type Item (RangeL n m a) = a
+	fromList lst = fromMaybe (error $ "The list is not within range.")
+		$ unfoldrRangeMaybe (\case [] -> Nothing; x : xs -> Just (x, xs)) lst
+	toList = Data.Foldable.toList
+
+---------------------------------------------------------------------------
+-- PUSH
+---------------------------------------------------------------------------
+
+infixr 5 .:..
+
+class PushL n m where
+	(.:..) :: a -> RangeL n m a -> RangeL n (m + 1) a
+
+	{-^
+
+	To push an optional element.
+
+	>>> :set -XDataKinds
+	>>> samplePushL = 'e' :. 'l' :. 'l' :. 'o' :.. NilL :: RangeL 3 7 Char
+	>>> 'h' .:.. samplePushL
+	'h' :. ('e' :. ('l' :. ('l' :.. ('o' :.. NilL))))
+	>>> :type 'h' .:.. samplePushL
+	'h' .:.. samplePushL :: RangeL 3 8 Char
+
+	-}
+
+instance PushL 0 m where
+	(.:..) x = \case NilL -> x :.. NilL; xs@(_ :.. _) -> x :.. xs
+
+instance {-# OVERLAPPABLE #-} (1 <= n, PushL (n - 1) (m - 1)) => PushL n m where
+	x .:.. y :. ys = x :. (y .:.. ys)
+
+---------------------------------------------------------------------------
+-- ADD
+---------------------------------------------------------------------------
+
+infixr 5 ++.
+
+class AddL n m v w where
+	(++.) :: RangeL n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
+
+	{-^
+
+	To concatenate two lists
+	whose types are @RangeL n m a@ and @RangeL v w a@.
+
+	>>> :set -XDataKinds
+	>>> sampleAddL1 = 'f' :. 'o' :. 'o' :.. NilL :: RangeL 2 5 Char
+	>>> sampleAddL2 = 'b' :. 'a' :.. 'r' :.. NilL :: RangeL 1 6 Char
+	>>> sampleAddL1 ++. sampleAddL2
+	'f' :. ('o' :. ('o' :. ('b' :.. ('a' :.. ('r' :.. NilL)))))
+	>>> :type sampleAddL1 ++. sampleAddL2
+	sampleAddL1 ++. sampleAddL2 :: RangeL 3 11 Char
+
+	-}
+
+instance AddL 0 0 v w where NilL ++. ys = ys
+
+instance {-# OVERLAPPABLE #-}
+	(PushL v (m + w - 1), AddL 0 (m - 1) v w, LoosenLMax v w (m + w)) =>
+	AddL 0 m v w where
+	(++.) :: forall a .  RangeL 0 m a -> RangeL v w a -> RangeL v (m + w) a
+	NilL ++. ys = loosenLMax ys
+	x :.. xs ++. ys = x .:.. (xs ++. ys :: RangeL v (m + w - 1) a)
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, AddL (n - 1) (m - 1) v w) => AddL n m v w where
+	x :. xs ++. ys = x :. (xs ++. ys)
+
+---------------------------------------------------------------------------
+-- LOOSEN
+---------------------------------------------------------------------------
+
+-- LOOSEN LEFT
+
+loosenL :: (LoosenLMin n m v, LoosenLMax v m w) => RangeL n m a -> RangeL v w a
+loosenL = loosenLMax . loosenLMin
+
+{-^
+
+To loosen a range of an element number.
+
+>>> :set -XDataKinds
+>>> sampleLoosenL = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :.. NilL :: RangeL 4 6 Char
+>>> loosenL sampleLoosenL :: RangeL 2 8 Char
+'h' :. ('e' :. ('l' :.. ('l' :.. ('o' :.. NilL))))
+
+-}
+
+-- LOOSEN LEFT MIN
+
+class LoosenLMin n m v where
+	loosenLMin :: RangeL n m a -> RangeL v m a
+
+	{-^
+
+	To loosen a lower bound of an element number.
+
+	>>> :set -XDataKinds -fno-warn-tabs
+	>>> :{
+		sampleLoosenLMin :: RangeL 4 6 Char
+		sampleLoosenLMin = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :.. NilL
+	:}
+
+	>>> loosenLMin sampleLoosenLMin :: RangeL 2 6 Char
+	'h' :. ('e' :. ('l' :.. ('l' :.. ('o' :.. NilL))))
+
+	-}
+
+instance LoosenLMin 0 m 0 where
+	loosenLMin = \case NilL -> NilL; xs@(_ :.. _) -> xs
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, LoosenLMin (n - 1) (m - 1) 0) => LoosenLMin n m 0 where
+	loosenLMin (x :. xs) = x :.. loosenLMin xs
+	
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, LoosenLMin (n - 1) (m - 1) (v - 1)) => LoosenLMin n m v where
+	loosenLMin (x :. xs) = x :. loosenLMin xs
+
+-- LOOSEN LEFT MAX
+
+class LoosenLMax n m w where
+	loosenLMax :: RangeL n m a -> RangeL n w a
+
+	{-^
+
+	To loosen an upper bound of an element number.
+
+	>>> :set -XDataKinds -fno-warn-tabs
+	>>> :{
+		sampleLoosenLMax :: RangeL 4 6 Char
+		sampleLoosenLMax = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :.. NilL
+	:}
+
+	>>> loosenLMax sampleLoosenLMax :: RangeL 4 8 Char
+	'h' :. ('e' :. ('l' :. ('l' :. ('o' :.. NilL))))
+
+	-}
+
+instance LoosenLMax 0 0 w where loosenLMax NilL = NilL
+
+instance {-# OVERLAPPABLE #-}
+	LoosenLMax 0 (m - 1) (w - 1) => LoosenLMax 0 m w where
+	loosenLMax = \case NilL -> NilL; (x :.. xs) -> x :.. loosenLMax xs
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, LoosenLMax (n - 1) (m - 1) (w - 1)) => LoosenLMax n m w where
+	loosenLMax (x :. xs) = x :. loosenLMax xs
+
+---------------------------------------------------------------------------
+-- UNFOLDR
+---------------------------------------------------------------------------
+
+-- CLASS
+
+class Unfoldr n v w where
+	unfoldrMRangeWithBase :: Monad m =>
+		RangeL n w a -> m Bool -> m a -> m (RangeL v w a)
+
+	{-^
+	
+	It is like @unfoldrMRange@. But it has already prepared values.
+
+	>>> :set -XDataKinds
+	>>> :module + Data.IORef
+	>>> r <- newIORef 1
+	>>> check = (< 3) <$> readIORef r
+	>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+	>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
+	>>> unfoldrMRangeWithBase xs check count :: IO (RangeL 3 5 Integer)
+	123 :. (456 :. (3 :. (6 :.. NilL)))
+	
+	-}
+
+	unfoldrMRangeMaybeWithBase :: Monad m =>
+		RangeL n w a -> m Bool -> m a -> m (Maybe (RangeL v w a))
+
+	{-^
+	
+	It is like @unfoldrMRangeMaybe@.
+	But it has already prepared values.
+
+	>>> :set -XDataKinds -fno-warn-tabs
+	>>> :module + Data.IORef
+	>>> r <- newIORef 1
+	>>> check = (< 3) <$> readIORef r
+	>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+	>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
+	>>> :{
+		unfoldrMRangeMaybeWithBase xs check count
+			:: IO (Maybe (RangeL 3 5 Integer))
+	:}
+	Just (123 :. (456 :. (3 :. (6 :.. NilL))))
+	
+	-}
+
+-- INSTANCE
+
+instance Unfoldr 0 0 0 where
+	unfoldrMRangeWithBase NilL _ _ = pure NilL
+	unfoldrMRangeMaybeWithBase NilL p _ = bool (Just NilL) Nothing <$> p
+
+instance {-# OVERLAPPABLE #-} Unfoldr 0 0 (w - 1) => Unfoldr 0 0 w where
+	unfoldrMRangeWithBase NilL p f =
+		(p >>=) . bool (pure NilL) $ f >>= \x ->
+			(x :..) <$> unfoldrMRangeWithBase NilL p f
+	unfoldrMRangeWithBase (x :.. xs) p f =
+		(x :..) <$> unfoldrMRangeWithBase xs p f
+
+	unfoldrMRangeMaybeWithBase NilL p f =
+		(p >>=) . bool (pure $ Just NilL) $ f >>= \x ->
+			((x :..) <$>) <$> unfoldrMRangeMaybeWithBase NilL p f
+	unfoldrMRangeMaybeWithBase (x :.. xs) p f =
+		((x :..) <$>) <$> unfoldrMRangeMaybeWithBase xs p f
+
+instance {-# OVERLAPPABLE #-}
+	Unfoldr 0 (v - 1) (w - 1) => Unfoldr 0 v w where
+	unfoldrMRangeWithBase NilL p f =
+		f >>= \x -> (x :.) <$> unfoldrMRangeWithBase NilL p f
+	unfoldrMRangeWithBase (x :.. xs) p f =
+		(x :.) <$> unfoldrMRangeWithBase xs p f
+
+	unfoldrMRangeMaybeWithBase NilL p f =
+		(p >>=) . bool (pure Nothing) $ f >>= \x ->
+			((x :.) <$>) <$> unfoldrMRangeMaybeWithBase NilL p f
+	unfoldrMRangeMaybeWithBase (x :.. xs) p f =
+		((x :.) <$>) <$> unfoldrMRangeMaybeWithBase xs p f
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, Unfoldr (n - 1) (v - 1) (w - 1)) => Unfoldr n v w where
+	unfoldrMRangeWithBase (x :. xs) p f =
+		(x :.) <$> unfoldrMRangeWithBase xs p f
+
+	unfoldrMRangeMaybeWithBase (x :. xs) p f =
+		((x :.) <$>) <$> unfoldrMRangeMaybeWithBase xs p f
+
+-- UNFOLDR RANGE
+
+unfoldrRange :: Unfoldr 0 v w =>
+	(s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
+unfoldrRange = unfoldrRangeWithBase NilL
+
+{-^
+
+To evaluate a function to construct a list.
+The function recieve a state and return an element and a new state.
+First argument is a predication which is evaluated
+when an element number is greater than a minimum and not greater than a maximum.
+
+>>> :set -XDataKinds
+>>> next n = (n * 3, n + 1)
+>>> unfoldrRange (< 2) next 1 :: RangeL 3 5 Int
+3 :. (6 :. (9 :. NilL))
+
+>>> unfoldrRange (< 5) next 1 :: RangeL 3 5 Int
+3 :. (6 :. (9 :. (12 :.. NilL)))
+
+>>> unfoldrRange (< 10) next 1 :: RangeL 3 5 Int
+3 :. (6 :. (9 :. (12 :.. (15 :.. NilL))))
+
+-}
+
+unfoldrRangeWithBase :: Unfoldr n v w =>
+	RangeL n w a -> (s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
+unfoldrRangeWithBase xs p f = fst . unfoldrRangeWithBaseWithS xs p f
+
+{-^
+
+It is like @unfoldrRange@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
+>>> unfoldrRangeWithBase xs (< 3) (\n -> (n * 3, n + 1)) 1 :: RangeL 3 5 Integer
+123 :. (456 :. (3 :. (6 :.. NilL)))
+
+-}
+
+unfoldrRangeWithBaseWithS :: Unfoldr n v w =>
+	RangeL n w a -> (s -> Bool) -> (s -> (a, s)) -> s -> (RangeL v w a, s)
+unfoldrRangeWithBaseWithS xs p f =
+	runStateL $ unfoldrMRangeWithBase xs (StateL $ p &&& id) (StateL f)
+
+{-^
+
+It is like @unfoldrRangeWithBase@.
+But it return not only a list but also a state value.
+
+>>> :set -XDataKinds
+>>> next n = (n * 3, n + 1)
+>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
+>>> unfoldrRangeWithBaseWithS xs (< 3) next 1 :: (RangeL 3 5 Integer, Integer)
+(123 :. (456 :. (3 :. (6 :.. NilL))),3)
+
+-}
+
+unfoldrMRange :: (Unfoldr 0 v w, Monad m) => m Bool -> m a -> m (RangeL v w a)
+unfoldrMRange = unfoldrMRangeWithBase NilL
+
+{-^
+
+It is like @unfoldrRange@. But it use a monad instead of a function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldrMRange ((< 5) <$> readIORef r) count :: IO (RangeL 3 5 Integer)
+3 :. (6 :. (9 :. (12 :.. NilL)))
+
+-}
+
+-- UNFOLDR RANGE MAYBE
+
+unfoldrRangeMaybe :: Unfoldr 0 v w =>
+	(s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
+unfoldrRangeMaybe = unfoldrRangeMaybeWithBase NilL
+
+{-^
+
+To eveluate a function to construct a list.
+The function recieve a state and
+return a nothing value or an element and a new state.
+If number of created elements is less than a minimum number of list elements or
+greater than a maximum number, then return Nothing.
+
+>>> :set -XDataKinds
+>>> next n0 n = if n < n0 then Just (n * 3, n + 1) else Nothing
+>>> unfoldrRangeMaybe (next 2) 1 :: Maybe (RangeL 3 5 Int)
+Nothing
+
+>>> unfoldrRangeMaybe (next 5) 1 :: Maybe (RangeL 3 5 Int)
+Just (3 :. (6 :. (9 :. (12 :.. NilL))))
+
+>>> unfoldrRangeMaybe (next 10) 1 :: Maybe (RangeL 3 5 Int)
+Nothing
+
+-}
+
+unfoldrRangeMaybeWithBase :: Unfoldr n v w =>
+	RangeL n w a -> (s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
+unfoldrRangeMaybeWithBase xs f =
+	fst . unfoldrRangeMaybeWithBaseGen xs (isJust &&& id)
+		(maybe (error "never occur") (f `second`)) . f
+
+{-^
+
+It is like @unfoldrRangeMaybe@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Int
+>>> next n = if n < 3 then Just (n * 3, n + 1) else Nothing
+>>> unfoldrRangeMaybeWithBase xs next 1 :: Maybe (RangeL 3 5 Int)
+Just (123 :. (456 :. (3 :. (6 :.. NilL))))
+
+-}
+
+type St a s r = Maybe (a, s) -> (r, Maybe (a, s))
+
+unfoldrRangeMaybeWithBaseGen :: Unfoldr n v w =>
+	RangeL n w a -> St a s Bool -> St a s a -> St a s (Maybe (RangeL v w a))
+unfoldrRangeMaybeWithBaseGen xs p f =
+	runStateL $ unfoldrMRangeMaybeWithBase xs (StateL p) (StateL f)
+
+unfoldrMRangeMaybe :: (Unfoldr 0 v w, Monad m) =>
+	m Bool -> m a -> m (Maybe (RangeL v w a))
+unfoldrMRangeMaybe = unfoldrMRangeMaybeWithBase NilL
+
+{-^
+
+It is like @unfoldrRangeMaybe@.
+But it use a monad instead of a function.
+The first argument monad return boolean value.
+It create values while this boolean value is True.
+If this boolean value is False before to create enough values or
+True after to create full values, then @unfoldrMRangeMaybe@ return Nothing.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> check n0 = (< n0) <$> readIORef r
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldrMRangeMaybe (check 2) count :: IO (Maybe (RangeL 3 5 Integer))
+Nothing
+
+>>> writeIORef r 1
+>>> unfoldrMRangeMaybe (check 5) count :: IO (Maybe (RangeL 3 5 Integer))
+Just (3 :. (6 :. (9 :. (12 :.. NilL))))
+
+>>> writeIORef r 1
+>>> unfoldrMRangeMaybe (check 10) count :: IO (Maybe (RangeL 3 5 Integer))
+Nothing
+
+-}
+
+---------------------------------------------------------------------------
+-- ZIP
+---------------------------------------------------------------------------
+
+-- CLASS
+
+class ZipL n m v w where
+	zipWithML :: Monad q =>
+		(a -> b -> q c) -> RangeL n m a -> RangeL v w b ->
+		q (RangeL n m c, RangeL (v - m) (w - n) b)
+
+	{-^
+
+	It is like @zipWithL@.
+	But it use a function which return a monad instead of a simple value.
+
+	>>> :set -XDataKinds -fno-warn-tabs
+	>>> ns = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Int
+	>>> :{
+		cs :: RangeL 5 7 Char
+		cs = 'a' :. 'b' :. 'c' :. 'd' :. 'e' :. 'f' :.. NilL
+	:}
+
+	>>> zipWithML (\n -> putStrLn . replicate n) ns cs
+	a
+	bb
+	ccc
+	(() :. (() :. (() :.. NilL)),'d' :. ('e' :.. ('f' :.. NilL)))
+
+	-}
+
+instance ZipL 0 0 v w where zipWithML _ NilL = pure . (NilL ,)
+
+instance {-# OVERLAPPABLE #-} (
+	1 <= v, LoosenLMin v w (v - m), LoosenLMax (v - m) (w - 1) w,
+	ZipL 0 (m - 1) (v - 1) (w - 1) ) => ZipL 0 m v w where
+	zipWithML _ NilL ys = pure (NilL, loosenLMin ys)
+	zipWithML (%) (x :.. xs) (y :. ys) =
+		x % y >>= \z -> ((z :..) *** loosenLMax) <$> zipWithML (%) xs ys
+
+instance {-# OVERLAPPABLE #-} (
+	1 <= n, 1 <= v, n <= w, m <= v,
+	ZipL (n - 1) (m - 1) (v - 1) (w - 1) ) => ZipL n m v w where
+	zipWithML (%) (x :. xs) (y :. ys) =
+		x % y >>= \z -> ((z :.) `first`) <$> zipWithML (%) xs ys
+
+-- FUNCTION
+
+zipL :: ZipL n m v w => RangeL n m a -> RangeL v w b ->
+	(RangeL n m (a, b), RangeL (v - m) (w - n) b)
+zipL = zipWithL (,)
+
+{-^
+
+To recieve two lists and return a tuple list and rest of the second list.
+The first list must be shorter or equal than the second list.
+
+>>> :set -XDataKinds
+>>> sampleZipL1 = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Integer
+>>> sampleZipL2 = 7 :. 6 :. 5 :. 4 :. 3 :. 2 :.. NilL :: RangeL 5 7 Integer
+>>> zipL sampleZipL1 sampleZipL2
+((1,7) :. ((2,6) :. ((3,5) :.. NilL)),4 :. (3 :.. (2 :.. NilL)))
+>>> :type zipL sampleZipL1 sampleZipL2
+zipL sampleZipL1 sampleZipL2
+  :: (RangeL 2 4 (Integer, Integer), RangeL 1 5 Integer)
+
+-}
+
+zipWithL :: ZipL n m v w => (a -> b -> c) -> RangeL n m a -> RangeL v w b ->
+	(RangeL n m c, RangeL (v - m) (w - n) b)
+zipWithL op = (runIdentity .) . zipWithML ((Identity .) . op)
+
+{-^
+
+It is like @zipL@.
+But it evaluate a function to make values instead of put together in tuples.
+
+>>> :set -XDataKinds
+>>> sampleZipWithL1 = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Integer
+>>> sampleZipWithL2 = 7 :. 6 :. 5 :. 4 :. 3 :. 2 :.. NilL :: RangeL 5 7 Integer
+>>> zipWithL (+) sampleZipWithL1 sampleZipWithL2
+(8 :. (8 :. (8 :.. NilL)),4 :. (3 :.. (2 :.. NilL)))
+>>> :type zipWithL (+) sampleZipWithL1 sampleZipWithL2
+zipWithL (+) sampleZipWithL1 sampleZipWithL2
+  :: (RangeL 2 4 Integer, RangeL 1 5 Integer)
+
+-}
diff --git a/src/Data/List/Range/RangeR.hs b/src/Data/List/Range/RangeR.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/Range/RangeR.hs
@@ -0,0 +1,627 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
+{-# LANGUAGE GADTs, TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
+	UndecidableInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+module Data.List.Range.RangeR (
+	-- ** Type
+	RangeR(..),
+	-- ** PushR
+	PushR, (.:++),
+	-- ** AddR
+	AddR, (+++),
+	-- ** LoosenRMin and LoosenRMax
+	-- *** loosenR
+	loosenR,
+	-- *** loosenRMin
+	LoosenRMin, loosenRMin,
+	-- *** loosenRMax
+	LoosenRMax, loosenRMax,
+	-- ** Unfoldl
+	-- *** class
+	Unfoldl,
+	-- *** unfoldlRange
+	-- **** without monad
+	unfoldlRange, unfoldlRangeWithBase, unfoldlRangeWithBaseWithS,
+	-- **** with monad
+	unfoldlMRange, unfoldlMRangeWithBase,
+	-- *** unfoldlRangeMaybe
+	-- **** without monad
+	unfoldlRangeMaybe, unfoldlRangeMaybeWithBase,
+	-- **** with monad
+	unfoldlMRangeMaybe, unfoldlMRangeMaybeWithBase,
+	-- ** ZipR
+	ZipR, zipR, zipWithR, zipWithMR ) where
+
+import GHC.TypeNats (Nat, type (+), type (-), type (<=))
+import GHC.Exts
+import Control.Arrow (first, second, (***), (&&&))
+import Control.Monad.Identity (Identity(..))
+import Control.Monad.State (StateR(..))
+import Data.Foldable
+import Data.Bool (bool)
+import Data.Maybe (isJust, fromMaybe)
+-- import Data.String
+
+---------------------------------------------------------------------------
+
+-- * TYPE
+--	+ RANGE RIGHT
+--	+ INSTANCE FUNCTOR
+--	+ INSTANCE FOLDABLE
+-- * PUSH
+-- * ADD
+-- * LOOSEN
+--	+ LOOSEN RIGHT
+--	+ LOOSEN RIGHT MIN
+--	+ LOOSEN RIGHT MAX
+-- * UNFOLDL
+--	+ CLASS
+--	+ INSTANCE
+--	+ UNFOLDL RANGE
+--	+ UNFOLDL RANGE MAYBE
+-- * ZIP
+--	+ CLASS AND INSTANCE
+--	+ FUNCTION
+
+---------------------------------------------------------------------------
+-- TYPE
+---------------------------------------------------------------------------
+
+-- RANGE RIGHT
+
+data RangeR :: Nat -> Nat -> * -> * where
+	NilR :: 0 <= m => RangeR 0 m a
+	(:++) :: 1 <= m => RangeR 0 (m - 1) a -> a -> RangeR 0 m a
+	(:+) :: (1 <= n, 1 <= m) =>
+		RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
+
+{-^
+
+@RangeR n m a@ is a list of type @a@ values whose element number is
+at minimum @n@, and at maximum @m@.
+You can push and pop an element from right.
+
+>>> :set -XDataKinds
+>>> sampleRangeR = NilR :++ 'h' :++ 'e' :+ 'l' :+ 'l' :+ 'o' :: RangeR 3 8 Char
+
+-}
+
+infixl 6 :+, :++
+
+deriving instance Show a => Show (RangeR n m a)
+
+-- INSTANCE FUNCTOR
+
+instance Functor (RangeR 0 0) where _ `fmap` NilR = NilR
+
+instance {-# OVERLAPPABLE #-}
+	Functor (RangeR 0 (m - 1)) => Functor (RangeR 0 m) where
+	fmap f = \case NilR -> NilR; xs :++ x -> (f <$> xs) :++ f x
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, Functor (RangeR (n - 1) (m - 1))) => Functor (RangeR n m) where
+	f `fmap` (xs :+ x) = (f <$> xs) :+ f x
+
+-- INSTANCE FOLDABLE
+
+instance Foldable (RangeR 0 0) where foldr _ z NilR = z
+
+instance {-# OVERLAPPABLE #-}
+	Foldable (RangeR 0 (m - 1)) => Foldable (RangeR 0 m) where
+	foldr (-<) z = \case NilR -> z; xs :++ x -> foldr (-<) (x -< z) xs
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Foldable (RangeR (n - 1) (m - 1))) =>
+	Foldable (RangeR n m) where
+	foldr (-<) z (xs :+ x) = foldr (-<) (x -< z) xs
+
+instance Applicative (RangeR 0 0) where pure _ = NilR; _ <*> _ = NilR
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeR n n), Applicative (RangeR (n - 1) (n - 1)), Unfoldl 0 n n) => Applicative (RangeR n n) where
+	pure = unfoldlRange (const True) (\x -> (x, x))
+	fs :+ f <*> xs :+ x = (fs <*> xs) :+ f x
+
+instance {-# OVERLAPPABLE #-} (Functor (RangeR 0 m), Applicative (RangeR 0 (m - 1)), Unfoldl 0 0 m) => Applicative (RangeR 0 m) where
+	pure = unfoldlRange (const True) (\x -> (x, x))
+	NilR <*> _ = NilR
+	_ <*> NilR = NilR
+	fs :++ f <*> xs :++ x = (fs <*> xs) :++ f x
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeR n m), Applicative (RangeR (n - 1) (m - 1)), Unfoldl 0 n m) => Applicative (RangeR n m) where
+	pure = unfoldlRange (const True) (\x -> (x, x))
+	fs :+ f <*> xs :+ x = (fs <*> xs) :+ f x
+
+instance Applicative (RangeR 0 0) => Monad (RangeR 0 0) where NilR >>= _ = NilR
+
+
+instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (RangeR n n), Monad (RangeR (n - 1) (n - 1))) => Monad (RangeR n n) where
+	xs :+ x >>= f = (xs >>= \z -> case f z of zs :+ _ -> zs) :+ y
+		where _ :+ y = f x
+
+-- INSTANCE ISSTRING
+
+instance Unfoldl 0 n m => IsString (RangeR n m Char) where
+	fromString s = fromMaybe (error $ "The string " ++ show s ++ " is not within range.")
+		. unfoldlRangeMaybe (\case "" -> Nothing; c : cs -> Just (cs, c)) $ reverse s
+
+instance (Foldable (RangeR n m), Unfoldl 0 n m) => IsList (RangeR n m a) where
+	type Item (RangeR n m a) = a
+	fromList lst = fromMaybe (error $ "The list is not within range.")
+		. unfoldlRangeMaybe (\case [] -> Nothing; x : xs -> Just (xs, x)) $ reverse lst
+	toList = Data.Foldable.toList
+
+---------------------------------------------------------------------------
+-- PUSH
+---------------------------------------------------------------------------
+
+infixl 5 .:++
+
+class PushR n m where
+	(.:++) :: RangeR n m a -> a -> RangeR n (m + 1) a
+
+	{-^
+
+	To push an optional element.
+
+	>>> :set -XDataKinds
+	>>> samplePushR = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :: RangeR 3 7 Char
+	>>> samplePushR .:++ 'o'
+	((((NilR :++ 'h') :++ 'e') :+ 'l') :+ 'l') :+ 'o'
+	>>> :type samplePushR .:++ 'o'
+	samplePushR .:++ 'o' :: RangeR 3 8 Char
+
+	-}
+
+instance PushR 0 m where
+	(.:++) = \case NilR -> (NilR :++); xs@(_ :++ _) -> (xs :++)
+
+instance {-# OVERLAPPABLE #-} (1 <= n, PushR (n - 1) (m - 1)) => PushR n m where
+	xs :+ x .:++ y = (xs .:++ x) :+ y
+
+---------------------------------------------------------------------------
+-- ADD
+---------------------------------------------------------------------------
+
+infixl 5 +++
+
+class AddR n m v w where
+	(+++) :: RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+
+	{-^
+
+	To concatenate two lists whose types are @RangeR n m a@ and @RangeR v w a@.
+
+	>>> :set -XDataKinds
+	>>> sampleRangeR1 = NilR :++ 'f' :+ 'o' :+ 'o' :: RangeR 2 5 Char
+	>>> sampleRangeR2 = NilR :++ 'b' :++ 'a' :+ 'r' :: RangeR 1 6 Char
+	>>> sampleRangeR1 +++ sampleRangeR2
+	(((((NilR :++ 'f') :++ 'o') :++ 'o') :+ 'b') :+ 'a') :+ 'r'
+	>>> :type sampleRangeR1 +++ sampleRangeR2
+	sampleRangeR1 +++ sampleRangeR2 :: RangeR 3 11 Char
+
+	-}
+
+instance AddR n m 0 0 where xs +++ NilR = xs
+
+instance {-# OVERLAPPABLE #-}
+	(PushR n (m + w - 1), AddR n m 0 (w - 1), LoosenRMax n m (m + w)) =>
+	AddR n m 0 w where
+	(+++) :: forall a . RangeR n m a -> RangeR 0 w a -> RangeR n (m + w) a
+	(+++) xs = \case
+		NilR -> loosenRMax xs
+		ys :++ y -> (xs +++ ys :: RangeR n (m + w - 1) a) .:++ y
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= v, AddR n m (v - 1) (w - 1)) => AddR n m v w where
+	xs +++ ys :+ y = (xs +++ ys) :+ y
+
+---------------------------------------------------------------------------
+-- LOOSEN
+---------------------------------------------------------------------------
+
+-- LOOSEN RIGHT
+
+loosenR :: (LoosenRMin n m v, LoosenRMax v m w) => RangeR n m a -> RangeR v w a
+loosenR = loosenRMax . loosenRMin
+
+{-^
+
+To loosen a range of element number.
+
+>>> :set -XDataKinds
+>>> sampleLoosenR = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o' :: RangeR 4 6 Char
+>>> loosenR sampleLoosenR :: RangeR 2 8 Char
+((((NilR :++ 'h') :++ 'e') :++ 'l') :+ 'l') :+ 'o'
+
+-}
+
+-- LOOSEN RIGHT MIN
+
+class LoosenRMin n m v where
+	loosenRMin :: RangeR n m a -> RangeR v m a
+
+	{-^
+
+	To loosen a lower bound of element number.
+
+	>>> :set -XDataKinds -fno-warn-tabs
+	>>> :{
+		sampleLoosenRMin :: RangeR 4 6 Char
+		sampleLoosenRMin = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'
+	:}
+
+	>>> loosenRMin sampleLoosenRMin :: RangeR 2 6 Char
+	((((NilR :++ 'h') :++ 'e') :++ 'l') :+ 'l') :+ 'o'
+
+	-}
+
+instance LoosenRMin 0 m 0 where
+	loosenRMin = \case NilR -> NilR; xs@(_ :++ _) -> xs
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, LoosenRMin (n - 1) (m - 1) 0) => LoosenRMin n m 0 where
+	loosenRMin (xs :+ x) = loosenRMin xs :++ x
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, LoosenRMin (n - 1) (m - 1) (v - 1)) => LoosenRMin n m v where
+	loosenRMin (xs :+ x) = loosenRMin xs :+ x
+
+-- LOOSEN RIGHT MAX
+
+class LoosenRMax n m w where
+	loosenRMax :: RangeR n m a -> RangeR n w a
+
+	{-^
+
+	To loosen an upper bound of element number.
+
+	>>> :set -XDataKinds -fno-warn-tabs
+	>>> :{
+		sampleLoosenRMax :: RangeR 4 6 Char
+		sampleLoosenRMax = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'
+	:}
+
+	>>> loosenRMax sampleLoosenRMax :: RangeR 4 8 Char
+	((((NilR :++ 'h') :+ 'e') :+ 'l') :+ 'l') :+ 'o'
+
+	-}
+
+instance LoosenRMax 0 0 m where loosenRMax NilR = NilR
+
+instance {-# OVERLAPPABLE #-}
+	LoosenRMax 0 (m - 1) (w - 1) => LoosenRMax 0 m w where
+	loosenRMax = \case NilR -> NilR; xs :++ x -> loosenRMax xs :++ x
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, LoosenRMax (n - 1) (m - 1) (w - 1)) => LoosenRMax n m w where
+	loosenRMax (xs :+ x) = loosenRMax xs :+ x
+
+---------------------------------------------------------------------------
+-- UNFOLDL
+---------------------------------------------------------------------------
+
+-- CLASS
+
+class Unfoldl n v w where
+	unfoldlMRangeWithBase :: Monad m =>
+		m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
+
+	{-^
+
+	It is like @unfoldlMRange@. But it has already prepared values.
+
+	>>> :set -XDataKinds
+	>>> :module + Data.IORef
+	>>> r <- newIORef 1
+	>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+	>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
+	>>> :{
+		unfoldlMRangeWithBase ((< 3) <$> readIORef r) count xs
+			:: IO (RangeR 3 5 Integer)
+	:}
+	(((NilR :++ 6) :+ 3) :+ 123) :+ 456
+
+	-}
+
+	unfoldlMRangeMaybeWithBase :: Monad m =>
+		m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
+
+	{-^
+
+	It is like @unfoldrMRangeMaybe@. But it has already prepared values.
+
+	>>> :set -XDataKinds
+	>>> :module + Data.IORef
+	>>> r <- newIORef 1
+	>>> check = (< 3) <$> readIORef r
+	>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+	>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
+	>>> :{
+		unfoldlMRangeMaybeWithBase check count xs
+			:: IO (Maybe (RangeR 3 5 Integer))
+	:}
+	Just ((((NilR :++ 6) :+ 3) :+ 123) :+ 456)
+
+	-}
+
+-- INSTANCE
+
+instance Unfoldl 0 0 0 where
+	unfoldlMRangeWithBase _ _ NilR = pure NilR
+	unfoldlMRangeMaybeWithBase p _ NilR = bool (Just NilR) Nothing <$> p
+
+instance {-# OVERLAPPABLE #-} Unfoldl 0 0 (w - 1) => Unfoldl 0 0 w where
+	unfoldlMRangeWithBase p f = \case
+		NilR -> (p >>=) . bool (pure NilR) $ f >>= \x ->
+			(:++ x) <$> unfoldlMRangeWithBase p f NilR
+		xs :++ x -> (:++ x) <$> unfoldlMRangeWithBase p f xs
+
+	unfoldlMRangeMaybeWithBase p f = \case
+		NilR -> (p >>=) . bool (pure $ Just NilR) $ f >>= \x ->
+			((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f NilR
+		xs :++ x -> ((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs
+
+instance {-# OVERLAPPABLE #-} Unfoldl 0 (v - 1) (w - 1) => Unfoldl 0 v w where
+	unfoldlMRangeWithBase p f = \case
+		NilR -> f >>= \x -> (:+ x) <$> unfoldlMRangeWithBase p f NilR
+		xs :++ x -> (:+ x) <$> unfoldlMRangeWithBase p f xs
+
+	unfoldlMRangeMaybeWithBase p f = \case
+		NilR -> (p >>=) . bool (pure Nothing) $ f >>= \x ->
+			((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f NilR
+		xs :++ x -> ((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs
+
+instance {-# OVERLAPPABLE #-}
+	(1 <= n, Unfoldl (n - 1) (v - 1) (w - 1)) => Unfoldl n v w where
+	unfoldlMRangeWithBase p f (xs :+ x) =
+		(:+ x) <$> unfoldlMRangeWithBase p f xs
+
+	unfoldlMRangeMaybeWithBase p f (xs :+ x) =
+		((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs
+
+-- UNFOLDL RANGE
+
+unfoldlRange :: Unfoldl 0 v w =>
+	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
+unfoldlRange p f s = unfoldlRangeWithBase p f s NilR
+
+{-^
+
+To eveluate a function to construct a list.
+The function recieve a state and return an element and a new state.
+The first argument is a predication which is evaluated when an element number is
+greater than a minimum and not greater than a maximum.
+
+>>> :set -XDataKinds
+>>> unfoldlRange (< 2) (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Int
+((NilR :+ 9) :+ 6) :+ 3
+
+>>> unfoldlRange (< 5) (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Int
+(((NilR :++ 12) :+ 9) :+ 6) :+ 3
+
+>>> unfoldlRange (< 10) (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Int
+((((NilR :++ 15) :++ 12) :+ 9) :+ 6) :+ 3
+
+-}
+
+unfoldlRangeWithBase :: Unfoldl n v w =>
+	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
+unfoldlRangeWithBase p f = (snd .) . unfoldlRangeWithBaseWithS p f
+
+{-^
+
+It is like @unfoldlRange@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
+>>> unfoldlRangeWithBase (< 3) (\n -> (n + 1, n * 3)) 1 xs :: RangeR 3 5 Integer
+(((NilR :++ 6) :+ 3) :+ 123) :+ 456
+
+-}
+
+unfoldlRangeWithBaseWithS :: Unfoldl n v w =>
+	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
+unfoldlRangeWithBaseWithS p f =
+	flip $ runStateR . unfoldlMRangeWithBase (StateR $ id &&& p) (StateR f)
+
+{-^
+
+It is like @unfoldlRangeWithBase@.
+But it return not only a list but also a state value.
+
+>>> :set -XDataKinds -fno-warn-tabs
+>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
+>>> :{
+	unfoldlRangeWithBaseWithS (< 3) (\n -> (n + 1, n * 3)) 1 xs
+		:: (Integer, RangeR 3 5 Integer)
+:}
+(3,(((NilR :++ 6) :+ 3) :+ 123) :+ 456)
+
+-}
+
+unfoldlMRange :: (Unfoldl 0 v w, Monad m) => m Bool -> m a -> m (RangeR v w a)
+unfoldlMRange p f = unfoldlMRangeWithBase p f NilR
+
+{-^
+
+It is like @unfoldlRange@. But it use a monad instead of a function.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldlMRange ((< 5) <$> readIORef r) count :: IO (RangeR 3 5 Integer)
+(((NilR :++ 12) :+ 9) :+ 6) :+ 3
+
+-}
+
+-- UNFOLDL RANGE MAYBE
+
+unfoldlRangeMaybe ::
+	Unfoldl 0 v w => (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
+unfoldlRangeMaybe f s = unfoldlRangeMaybeWithBase f s NilR
+
+{-^
+
+To evaluate a function to construct a list.
+The function recieves a state and
+return a nothing value or an element and a new state.
+If the number of created elements is
+less than a minimum number of list elements or
+greater than a maximum number, then return @Nothing@.
+
+>>> :set -XDataKinds
+>>> count n0 n = if n < n0 then Just (n + 1, n * 3) else Nothing
+>>> unfoldlRangeMaybe (count 2) 1 :: Maybe (RangeR 3 5 Int)
+Nothing
+
+>>> unfoldlRangeMaybe (count 5) 1 :: Maybe (RangeR 3 5 Int)
+Just ((((NilR :++ 12) :+ 9) :+ 6) :+ 3)
+
+>>> unfoldlRangeMaybe (count 10) 1 :: Maybe (RangeR 3 5 Int)
+Nothing
+
+-}
+
+unfoldlRangeMaybeWithBase :: Unfoldl n v w =>
+	(s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
+unfoldlRangeMaybeWithBase f s xs =
+	snd $ unfoldlRangeMaybeWithBaseGen (id &&& isJust)
+		(maybe (error "never occur") (f `first`)) xs (f s)
+
+{-^
+
+It is like @unfoldlRangeMaybe@. But it has already prepared values.
+
+>>> :set -XDataKinds
+>>> count n = if n < 3 then Just (n + 1, n * 3) else Nothing
+>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Int
+>>> unfoldlRangeMaybeWithBase count 1 xs :: Maybe (RangeR 3 5 Int)
+Just ((((NilR :++ 6) :+ 3) :+ 123) :+ 456)
+
+-}
+
+type St s a r = Maybe (s, a) -> (Maybe (s, a), r)
+
+unfoldlRangeMaybeWithBaseGen :: Unfoldl n v w =>
+	St s a Bool -> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
+unfoldlRangeMaybeWithBaseGen p f =
+	runStateR . unfoldlMRangeMaybeWithBase (StateR p) (StateR f)
+
+unfoldlMRangeMaybe :: (Unfoldl 0 v w, Monad m) =>
+	m Bool -> m a -> m (Maybe (RangeR v w a))
+unfoldlMRangeMaybe p f = unfoldlMRangeMaybeWithBase p f NilR
+
+{-^
+
+It is like @unfoldlRangeMaybe@. But it use a monad instead of a function.
+The first argument monad returns a boolean value.
+It creates values while this boolean value is @True@.
+If this boolean value is @False@ before to create enough values or
+@True@ after to create full values, then @unfoldlMRangeMaybe@ returns Nothing.
+
+>>> :set -XDataKinds
+>>> :module + Data.IORef
+>>> r <- newIORef 1
+>>> check n0 = (< n0) <$> readIORef r
+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
+>>> unfoldlMRangeMaybe (check 2) count :: IO (Maybe (RangeR 3 5 Integer))
+Nothing
+
+>>> writeIORef r 1
+>>> unfoldlMRangeMaybe (check 5) count :: IO (Maybe (RangeR 3 5 Integer))
+Just ((((NilR :++ 12) :+ 9) :+ 6) :+ 3)
+
+>>> writeIORef r 1
+>>> unfoldlMRangeMaybe (check 10) count :: IO (Maybe (RangeR 3 5 Integer))
+Nothing
+
+-}
+
+---------------------------------------------------------------------------
+-- ZIP
+---------------------------------------------------------------------------
+
+-- CLASS AND INSTANCE
+
+class ZipR n m v w where
+	zipWithMR :: Monad q =>
+		(a -> b -> q c) -> RangeR n m a -> RangeR v w b ->
+		q (RangeR (n - w) (m - v) a, RangeR v w c)
+
+	{-^
+
+	It is like @zipWithR@.
+	But it uses a function which returns a monad instead of a simple value.
+
+	>>> :set -XDataKinds
+	>>> ns = NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 5 7 Int
+	>>> cs = NilR :++ 'a' :+ 'b' :+ 'c' :: RangeR 2 4 Char
+	>>> zipWithMR (\n -> putStrLn . replicate n) ns cs
+	cccccc
+	bbbbb
+	aaaa
+	(((NilR :++ 1) :++ 2) :+ 3,((NilR :++ ()) :+ ()) :+ ())
+
+	-}
+
+instance ZipR n m 0 0 where zipWithMR _ xs NilR = pure (xs, NilR)
+
+instance {-# OVERLAPPABLE #-} (
+	1 <= n, LoosenRMin n m (n - w), LoosenRMax (n - w) (m - 1) m,
+	ZipR (n - 1) (m - 1) 0 (w - 1) ) => ZipR n m 0 w where
+	zipWithMR _ xs NilR = pure (loosenRMin xs, NilR)
+	zipWithMR (%) (xs :+ x) (ys :++ y) =
+		x % y >>= \z -> (loosenRMax *** (:++ z)) <$> zipWithMR (%) xs ys
+
+instance {-# OVERLAPPABLE #-} (
+	1 <= n, 1 <= v, v <= m, w <= n,
+	ZipR (n - 1) (m - 1) (v - 1) (w - 1) ) => ZipR n m v w where
+	zipWithMR (%) (xs :+ x) (ys :+ y) =
+		x % y >>= \z -> ((:+ z) `second`) <$> zipWithMR (%) xs ys
+
+-- FUNCTION
+
+zipR :: ZipR n m v w => RangeR n m a -> RangeR v w b ->
+	(RangeR (n - w) (m - v) a, RangeR v w (a, b))
+zipR = zipWithR (,)
+
+{-^
+
+To recieve two lists and return a tuple list and rest of the first list.
+The second list must be shorter or equal than the first list.
+
+>>> :set -XDataKinds
+>>> sampleZipR1 = NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 5 7 Integer
+>>> sampleZipR2 = NilR :++ 3 :+ 2 :+ 1 :: RangeR 2 4 Integer
+>>> zipR sampleZipR1 sampleZipR2
+(((NilR :++ 1) :++ 2) :+ 3,((NilR :++ (4,3)) :+ (5,2)) :+ (6,1))
+>>> :type zipR sampleZipR1 sampleZipR2
+zipR sampleZipR1 sampleZipR2
+  :: (RangeR 1 5 Integer, RangeR 2 4 (Integer, Integer))
+
+-}
+
+zipWithR :: ZipR n m v w => (a -> b -> c) -> RangeR n m a -> RangeR v w b ->
+	(RangeR (n - w) (m - v) a, RangeR v w c)
+zipWithR op = (runIdentity .) . zipWithMR ((Identity .) . op)
+
+{-^
+
+It is like @zipR@.
+But it evaluates a function to make values instead of puts together in tuples.
+
+>>> :set -XDataKinds
+>>> sampleZipWithR1 = NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 5 7 Integer
+>>> sampleZipWithR2 = NilR :++ 7 :+ 6 :+ 5 :: RangeR 2 4 Integer
+>>> zipWithR (+) sampleZipWithR1 sampleZipWithR2
+(((NilR :++ 1) :++ 2) :+ 3,((NilR :++ 11) :+ 11) :+ 11)
+>>> :type zipWithR (+) sampleZipWithR1 sampleZipWithR2
+zipWithR (+) sampleZipWithR1 sampleZipWithR2
+  :: (RangeR 1 5 Integer, RangeR 2 4 Integer)
+
+-}
diff --git a/test/doctests.hs b/test/doctests.hs
new file mode 100644
--- /dev/null
+++ b/test/doctests.hs
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Main (main) where
+
+import Test.DocTest
+
+main :: IO ()
+main = doctest [
+	"-isrc",
+	"src/Data/List/Length.hs",
+	"src/Data/List/Range.hs",
+	"src/Data/List/Range/Nat.hs" ]
diff --git a/test/spec.hs b/test/spec.hs
new file mode 100644
--- /dev/null
+++ b/test/spec.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import Data.Bits
+import Data.Word
+
+import Data.List.Length
+import Data.List.Range
+
+main :: IO ()
+main = do
+	print $ foo 123; putStrLn ""
+	print $ bar 123; putStrLn ""
+	print baz; putStrLn ""
+	print hoge; putStrLn ""
+
+foo :: Word32 -> LengthL 32 Bool
+foo = unfoldr \w -> (w `testBit` 0, w `shiftR` 1)
+
+bar :: Word32 -> LengthR 32 Bool
+bar = unfoldl \w -> (w `shiftR` 1, w `testBit` 0)
+
+baz :: (RangeL 2 3 (Integer, Integer), RangeL 1 6 Integer)
+baz = zipWithL (,)
+	(1 :. 2 :. 3 :.. NilL :: RangeL 2 3 Integer)
+	(1 :. 2 :. 3 :. 4 :. 5 :.. NilL :: RangeL 4 8 Integer)
+
+hoge :: (RangeR 1 6 Integer, RangeR 2 3 (Integer, Integer))
+hoge = zipWithR (,)
+	(NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :: RangeR 4 8 Integer)
+	(NilR :++ 1 :+ 2 :+ 3 :: RangeR 2 3 Integer)