Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

OAlg.Entity.FinList

Contents

FinList
- Induction

Description

finite lists, parameterized by there length.

Synopsis

data FinList (n :: N') a where
- Nil :: FinList N0 a
- (:|) :: a -> FinList n a -> FinList (n + 1) a
toW :: FinList n a -> W n
head :: FinList (n + 1) a -> a
tail :: FinList (n + 1) a -> FinList n a
zip :: FinList n a -> FinList n b -> FinList n (a, b)
zip3 :: FinList n a -> FinList n b -> FinList n c -> FinList n (a, b, c)
(|:) :: FinList n a -> a -> FinList (n + 1) a
(++) :: FinList n a -> FinList m a -> FinList (n + m) a
(**) :: FinList n a -> FinList m b -> FinList (n * m) (a, b)
repeat :: Any n -> a -> FinList n a
iFinList :: N -> FinList n a -> FinList n (a, N)
iFinList0 :: FinList n a -> FinList n (a, N)
iFinList' :: Any n -> FinList n N
toArray :: FinList n a -> Array N a
someFinList :: [a] -> SomeFinList a
data SomeFinList a = forall n. SomeFinList (FinList n a)
(<++>) :: SomeFinList x -> SomeFinList x -> SomeFinList x
inductionS :: Any n -> FinList N0 a -> (forall i. FinList i a -> FinList (i + 1) a) -> FinList n a
newtype FinList' a n = FinList' (FinList n a)

FinList

data FinList (n :: N') a where Source #

finite lists, parameterized by there length.

Constructors

Nil :: FinList N0 a
(:\|) :: a -> FinList n a -> FinList (n + 1) a infixr 5

Instances

Instances details

Foldable (FinList n) Source #
Instance details Defined in OAlg.Entity.FinList Methods fold :: Monoid m => FinList n m -> m # foldMap :: Monoid m => (a -> m) -> FinList n a -> m # foldMap' :: Monoid m => (a -> m) -> FinList n a -> m # foldr :: (a -> b -> b) -> b -> FinList n a -> b # foldr' :: (a -> b -> b) -> b -> FinList n a -> b # foldl :: (b -> a -> b) -> b -> FinList n a -> b # foldl' :: (b -> a -> b) -> b -> FinList n a -> b # foldr1 :: (a -> a -> a) -> FinList n a -> a # foldl1 :: (a -> a -> a) -> FinList n a -> a # toList :: FinList n a -> [a] # null :: FinList n a -> Bool # length :: FinList n a -> Int # elem :: Eq a => a -> FinList n a -> Bool # maximum :: Ord a => FinList n a -> a # minimum :: Ord a => FinList n a -> a # sum :: Num a => FinList n a -> a # product :: Num a => FinList n a -> a #
Functor (FinList n) Source #
Instance details Defined in OAlg.Entity.FinList Methods fmap :: (a -> b) -> FinList n a -> FinList n b # (<$) :: a -> FinList n b -> FinList n a #
Show a => Show (FinList n a) Source #
Instance details Defined in OAlg.Entity.FinList Methods showsPrec :: Int -> FinList n a -> ShowS # show :: FinList n a -> String # showList :: [FinList n a] -> ShowS #
Eq a => Eq (FinList n a) Source #
Instance details Defined in OAlg.Entity.FinList Methods (==) :: FinList n a -> FinList n a -> Bool # (/=) :: FinList n a -> FinList n a -> Bool #
Ord x => Ord (FinList n x) Source #
Instance details Defined in OAlg.Entity.FinList Methods compare :: FinList n x -> FinList n x -> Ordering # (<) :: FinList n x -> FinList n x -> Bool # (<=) :: FinList n x -> FinList n x -> Bool # (>) :: FinList n x -> FinList n x -> Bool # (>=) :: FinList n x -> FinList n x -> Bool # max :: FinList n x -> FinList n x -> FinList n x # min :: FinList n x -> FinList n x -> FinList n x #
Validable a => Validable (FinList n a) Source #
Instance details Defined in OAlg.Entity.FinList Methods valid :: FinList n a -> Statement Source #
(Typeable n, Entity a) => Entity (FinList n a) Source #
Instance details Defined in OAlg.Entity.FinList

toW :: FinList n a -> W n Source #

the underlying witness.

head :: FinList (n + 1) a -> a Source #

the head of a non empty finite list.

tail :: FinList (n + 1) a -> FinList n a Source #

the tail of a non empty finite list.

zip :: FinList n a -> FinList n b -> FinList n (a, b) Source #

zips two sequences of the same length.

zip3 :: FinList n a -> FinList n b -> FinList n c -> FinList n (a, b, c) Source #

zips three sequences of the same length.

(|:) :: FinList n a -> a -> FinList (n + 1) a infixl 5 Source #

appending an element at the end of the finite list.

(++) :: FinList n a -> FinList m a -> FinList (n + m) a infixr 5 Source #

appending two finite lists.

(**) :: FinList n a -> FinList m b -> FinList (n * m) (a, b) Source #

the product of two finite lists.

repeat :: Any n -> a -> FinList n a Source #

the constant sequence.

iFinList :: N -> FinList n a -> FinList n (a, N) Source #

indexing finite lists, starting at the given natural number.

iFinList0 :: FinList n a -> FinList n (a, N) Source #

adjoins to each element its index, starting from '0'.

iFinList' :: Any n -> FinList n N Source #

the sequence 0,1 .. n-1.

toArray :: FinList n a -> Array N a Source #

maps a sequnece as = a0..a(n-1) of length n to the corresponding array a with ai == a$i for i = 0..(n-1).

someFinList :: [a] -> SomeFinList a Source #

the associated finite list.

data SomeFinList a Source #

some finite list.

Constructors

forall n. SomeFinList (FinList n a)

Instances

Instances details

Functor SomeFinList Source #
Instance details Defined in OAlg.Entity.FinList Methods fmap :: (a -> b) -> SomeFinList a -> SomeFinList b # (<$) :: a -> SomeFinList b -> SomeFinList a #
Show a => Show (SomeFinList a) Source #
Instance details Defined in OAlg.Entity.FinList Methods showsPrec :: Int -> SomeFinList a -> ShowS # show :: SomeFinList a -> String # showList :: [SomeFinList a] -> ShowS #

(<++>) :: SomeFinList x -> SomeFinList x -> SomeFinList x infixr 5 Source #

concatenation.

Induction

inductionS :: Any n -> FinList N0 a -> (forall i. FinList i a -> FinList (i + 1) a) -> FinList n a Source #

induction for sequences.

newtype FinList' a n Source #

Wrapper to switch the parameters.

Constructors

FinList' (FinList n a)