-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Size-parameterized vector types and functions.
--   
--   Size-parameterized vector types and functions using a data-type
--   promotion.
@package sized-vector
@version 0.0.1.0


-- | Type level peano natural number, some arithmetic functions and their
--   singletons.
module Data.Type.Natural

-- | Peano natural numbers. It will be promoted to the type-level natural
--   number.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Singleton type for <a>Nat</a>. When constructing data, use smart
--   constructors such as <a>sZ</a> and <a>sS</a>.
data SNat (n :: Nat)
SZ :: SNat Z
SS :: SNat n -> SNat (S n)

-- | The smart constructor for <tt>SZ</tt>.
sZ :: SNat Z

-- | The smart constructor for <tt>SS n</tt>.
sS :: SNat n -> SNat (S n)

-- | Minimum function.
min :: Nat -> Nat -> Nat

-- | Type-level minimum function.

-- | Singleton function for minimum function.
sMin :: SNat n -> SNat m -> SNat (Min n m)

-- | Maximum function.
max :: Nat -> Nat -> Nat

-- | Type-level maximum function.

-- | Singleton function for maximum.
sMax :: SNat n -> SNat m -> SNat (Max n m)

-- | Type-level addition.

-- | Addition for singleton numbers.
(%+) :: SNat n -> SNat m -> SNat (n :+: m)

-- | Type-level multiplication.

-- | Multiplication for singleton numbers.
(%*) :: SNat n -> SNat m -> SNat (n :*: m)
(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)

-- | Comparison witness via GADTs.
data Leq (n :: Nat) (m :: Nat)
ZeroLeq :: SNat m -> Leq Zero m
SuccLeqSucc :: Leq n m -> Leq (S n) (S m)

-- | Comparison via type-class.
class (:<=) (n :: Nat) (m :: Nat)

-- | Comparison function
data LeqInstance n m
leqRefl :: SNat n -> LeqInstance n n
leqSucc :: SNat n -> LeqInstance n (S n)
boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
propToClassLeq :: Leq n m -> LeqInstance n m

-- | Singleton type-class. This class will be removed soon after singletons
--   package available for the latest Haskell Paltform.
class Sing n
sing :: Sing n => SNat n

-- | Witness for <a>Sing</a> instance. This type will be removed soon after
--   singletons package available for the latest Haskell Paltform.
data SingInstance a
SingInstance :: SingInstance a

-- | Get witness for singleton integers. This function will be removed soon
--   after singletons package available for the latest Haskell Paltform.
singInstance :: SNat n -> SingInstance n

-- | Convert <a>Nat</a> into normal integers.
natToInt :: Integral n => Nat -> n

-- | Convert integral numbers into <a>Nat</a>
intToNat :: (Integral a, Ord a) => a -> Nat

-- | Convert 'SNat n' into normal integers.
sNatToInt :: Num n => SNat x -> n
type Zero = Z
type One = S Zero
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type Six = S Five
type Seven = S Six
type Eight = S Seven
type Nine = S Eight
type Ten = S Nine
type Eleven = S Ten
type Twelve = S Eleven
type Thirteen = S Twelve
type Fourteen = S Thirteen
type Fifteen = S Fourteen
type Sixteen = S Fifteen
type Seventeen = S Sixteen
type Eighteen = S Seventeen
type Nineteen = S Eighteen
type Twenty = S Nineteen
sZero :: SNat Z
sOne :: SNat One
sTwo :: SNat Two
sThree :: SNat Three
sFour :: SNat Four
sFive :: SNat Five
sSix :: SNat Six
sSeven :: SNat Seven
sEight :: SNat Eight
sNine :: SNat Nine
sTen :: SNat Ten
sEleven :: SNat Eleven
sTwelve :: SNat Twelve
sThirteen :: SNat Thirteen
sFourteen :: SNat Fourteen
sFifteen :: SNat Fifteen
sSixteen :: SNat Sixteen
sSeventeen :: SNat Seventeen
sEighteen :: SNat Eighteen
sNineteen :: SNat Nineteen
sTwenty :: SNat Twenty
type N0 = Z
type N1 = One
type N2 = Two
type N3 = Three
type N4 = Four
type N5 = Five
type N6 = Six
type N7 = Seven
type N8 = Eight
type N9 = Nine
type N10 = Ten
type N11 = Eleven
type N12 = Twelve
type N13 = Thirteen
type N14 = Fourteen
type N15 = Fifteen
type N16 = Sixteen
type N17 = Seventeen
type N18 = Eighteen
type N19 = Nineteen
type N20 = Twenty
sN0 :: SNat Z
sN1 :: SNat One
sN2 :: SNat Two
sN3 :: SNat Three
sN4 :: SNat Four
sN5 :: SNat Five
sN6 :: SNat Six
sN7 :: SNat Seven
sN8 :: SNat Eight
sN9 :: SNat Nine
sN10 :: SNat Ten
sN11 :: SNat Eleven
sN12 :: SNat Twelve
sN13 :: SNat Thirteen
sN14 :: SNat Fourteen
sN15 :: SNat Fifteen
sN16 :: SNat Sixteen
sN17 :: SNat Seventeen
sN18 :: SNat Eighteen
sN19 :: SNat Nineteen
sN20 :: SNat Twenty
instance Show Nat
instance Eq Nat
instance Ord Nat
instance Sing n => Sing ('S n)
instance Sing 'Z
instance n :<= m => 'S n :<= 'S m
instance 'Z :<= n
instance Num Nat


-- | Size-parameterized vector types and functions.
module Data.Vector.Sized
data Vector (a :: *) (n :: Nat)
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
sLength :: Vector a n -> SNat n
length :: Vector a n -> Int
append :: Vector a n -> Vector a m -> Vector a (n :+: m)
foldr :: (a -> b -> b) -> b -> Vector a n -> b
foldl :: (a -> b -> a) -> a -> Vector b n -> a
singleton :: a -> Vector a (S Z)
zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n
zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)
toList :: Vector a n -> [a]
fromList :: SNat n -> [a] -> Maybe (Vector a n)
unsafeFromList :: SNat n -> [a] -> Vector a n
fromList' :: Sing n => [a] -> Maybe (Vector a n)
unsafeFromList' :: Sing n => [a] -> Vector a n
all :: (a -> Bool) -> Vector a n -> Bool
splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))
drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)
take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n
map :: (a -> b) -> Vector a n -> Vector b n
head :: Vector a (S n) -> a
tail :: Vector a (S n) -> Vector a n
instance Show a => Show (Vector a n)
instance Eq a => Eq (Vector a n)