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

OAlg.Entity.FinList

Contents

FinList
- Induction
X

Description

finite lists, parameterized by there length.

Synopsis

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

FinList

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

finite lists, parameterized by there length.

Constructors

Nil :: forall a. FinList 'N0 a
(:\|) :: forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 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 #
ApplicativeG (FinList n) (->) (->) Source #
Instance details Defined in OAlg.Entity.FinList Methods amapG :: (x -> y) -> FinList n x -> FinList n y Source #
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 #

toW :: forall (n :: N') a. FinList n a -> W n Source #

the underlying witness.

head :: forall (n :: N') a. FinList (n + 1) a -> a Source #

the head of a non empty finite list.

tail :: forall (n :: N') a. FinList (n + 1) a -> FinList n a Source #

the tail of a non empty finite list.

zip :: forall (n :: N') a b. FinList n a -> FinList n b -> FinList n (a, b) Source #

zips two sequences of the same length.

zip3 :: forall (n :: N') a b c. FinList n a -> FinList n b -> FinList n c -> FinList n (a, b, c) Source #

zips three sequences of the same length.

(|:) :: forall (n :: N') a. FinList n a -> a -> FinList (n + 1) a infixl 5 Source #

appending an element at the end of the finite list.

(++) :: forall (n :: N') a (m :: N'). FinList n a -> FinList m a -> FinList (n + m) a infixr 5 Source #

appending two finite lists.

(**) :: forall (n :: N') a (m :: N') b. FinList n a -> FinList m b -> FinList (n * m) (a, b) Source #

the product of two finite lists.

repeat :: forall (n :: N') a. Any n -> a -> FinList n a Source #

the constant sequence.

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

indexing finite lists, starting at the given natural number.

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

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

iFinList' :: forall (n :: N'). Any n -> FinList n N Source #

the sequence 0,1 .. n-1.

toArray :: forall (n :: N') a. 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).

maybeFinList :: forall (n :: N') a. Any n -> [a] -> Maybe (FinList n a) Source #

list as a finite list according to n.

Property Let xs be in [a] and n in Any n, then holds:

If lengthN n <= length xs then maybeFinList n xs matches Just xs' with toList xs' == xs.

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

the associated finite list.

Note If the input list is infinite then someFinList dose not terminate.

data SomeFinList a Source #

some finite list.

Constructors

SomeFinList (FinList n a)

Instances

Instances details

ApplicativeG SomeFinList (->) (->) Source #
Instance details Defined in OAlg.Entity.FinList Methods amapG :: (x -> y) -> SomeFinList x -> SomeFinList y Source #
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 #
Validable a => Validable (SomeFinList a) Source #
Instance details Defined in OAlg.Entity.FinList Methods valid :: SomeFinList a -> Statement Source #

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

concatenation.

Induction

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

induction for sequences.

newtype FinList' a (n :: N') Source #

Wrapper to switch the parameters.

Constructors

FinList' (FinList n a)

X

xListF :: forall (n :: N') x. FinList n (X x) -> X (FinList n x) Source #

random variable for a finite list of random variables.