fixed-length-0.2: Lists with statically known length based on non-empty package.

Safe HaskellSafe
LanguageHaskell98

Data.FixedLength

Documentation

data T n a Source

Instances

Natural n => Functor (T n) Source 
Natural n => Applicative (T n) Source 
Natural n => Foldable (T n) Source 
Natural n => Traversable (T n) Source 
(Natural n, Eq a) => Eq (T n a) Source 
(Natural n, Show a) => Show (T n a) Source 

type family Position n :: * Source

Instances

type family List n :: * -> * Source

Instances

type List Zero = T Source 
type List (Succ n) = T (List n) Source 

type family Length f Source

Instances

type Length T = Zero Source 
type Length (T f) = Succ (Length f) Source 

data Index n Source

Instances

Natural n => Eq (Index n) Source 
Natural n => Ord (Index n) Source 

data Zero Source

Instances

data Succ pos Source

Constructors

Stop 
Succ pos 

Instances

Eq pos => Eq (Succ pos) Source 
Ord pos => Ord (Succ pos) Source 
Show pos => Show (Succ pos) Source 

toList :: Natural n => T n a -> [a] Source

showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS Source

map :: Natural n => (a -> b) -> T n a -> T n b Source

zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c Source

sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a) Source

repeat :: Natural n => a -> T n a Source

index :: Natural n => Index n -> T n a -> a Source

update :: Natural n => (a -> a) -> Index n -> T n a -> T n a Source

indices :: Natural n => T n (Index n) Source

indicesInt :: Natural n => T n Int Source

numFromIndex :: Natural n => Index n -> Word Source

type GE1 n = Succ n Source

type GE2 n = Succ (GE1 n) Source

type GE3 n = Succ (GE2 n) Source

type GE4 n = Succ (GE3 n) Source

type GE5 n = Succ (GE4 n) Source

type GE6 n = Succ (GE5 n) Source

type GE7 n = Succ (GE6 n) Source

type GE8 n = Succ (GE7 n) Source

i0 :: Index (GE1 n) Source

i1 :: Index (GE2 n) Source

i2 :: Index (GE3 n) Source

i3 :: Index (GE4 n) Source

i4 :: Index (GE5 n) Source

i5 :: Index (GE6 n) Source

i6 :: Index (GE7 n) Source

i7 :: Index (GE8 n) Source

fromFixedList :: List n a -> T n a Source

toFixedList :: T n a -> List n a Source

(!:) :: a -> T n a -> T (Succ n) a infixr 5 Source

end :: T Zero a Source

singleton :: a -> T U1 a Source

viewL :: T (Succ n) a -> (a, T n a) Source

switchL :: (a -> T n a -> b) -> T (Succ n) a -> b Source

head :: Positive n => T n a -> a Source

tail :: T (Succ n) a -> T n a Source

switchEnd :: b -> T Zero a -> b Source

type family Curried n a b Source

Instances

type Curried Zero a b = b Source 
type Curried (Succ n) a b = a -> Curried n a b Source 

uncurry :: Natural n => Curried n a b -> T n a -> b Source

minimum :: (Positive n, Ord a) => T n a -> a Source

maximum :: (Positive n, Ord a) => T n a -> a Source