Safe Haskell	None
Language	Haskell2010

Vector.Lifted

Contents

Primitives
Ranges
Freeze
Copy
Composite
Index
Unsafe
Interop with primitive
Interop with lists
Hide Length
Recover Length

Synopsis

data Vector (a :: Nat) b where
- Vector :: forall (a :: Nat) b. Vector# a b -> Vector a b
data Vector# (a :: Nat) b :: UnliftedType
data MutableVector a (b :: Nat) c where
- MutableVector :: forall a (b :: Nat) c. MutableVector# a b c -> MutableVector a b c
data MutableVector# a (b :: Nat) c :: UnliftedType
data Bounded (a :: Nat) b where
- Bounded :: forall b (a :: Nat) (m :: Nat). Nat# m -> (m <=# a) -> Vector# m b -> Bounded a b
data Vector_ a where
- Vector_ :: forall a (n :: Nat). Nat# n -> Vector# n a -> Vector_ a
type family FromMutability# (m :: Mutability) :: Nat -> TYPE R -> UnliftedType where ...
write# :: forall s (n :: Nat) a. MutableVector# s n a -> Fin# n -> a -> State# s -> State# s
write :: forall s (n :: Nat) a. MutableVector s n a -> Fin# n -> a -> ST s ()
read# :: forall s (n :: Nat) a. MutableVector# s n a -> Fin# n -> State# s -> (# State# s, a #)
read :: forall s (n :: Nat) a. MutableVector s n a -> Fin# n -> ST s a
index# :: forall (n :: Nat) a. Vector# n a -> Fin# n -> a
index :: forall (n :: Nat) a. Vector n a -> Fin# n -> a
unlift :: forall (n :: Nat) a. Vector n a -> Vector# n a
substitute :: forall (m :: Nat) (n :: Nat) a. (m :=:# n) -> Vector m a -> Vector n a
substitute# :: forall (m :: Nat) (n :: Nat) a. (m :=:# n) -> Vector# m a -> Vector# n a
initialized :: forall s (n :: Nat) a. Nat# n -> a -> ST s (MutableVector s n a)
initialized# :: forall s (n :: Nat) a. Nat# n -> a -> State# s -> (# State# s, MutableVector# s n a #)
unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) a. Nat n -> Vector m a -> Vector n a
set :: forall s (n :: Nat) a. MutableVector s n a -> Nat# n -> a -> ST s ()
setSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s a. ((i + n) <=# m) -> MutableVector s n a -> Nat# i -> Nat# m -> a -> ST s ()
unsafeShrinkFreeze :: forall s (n0 :: Nat) (n1 :: Nat) a. (n1 <=# n0) -> MutableVector s n0 a -> Nat# n1 -> ST s (Vector n1 a)
unsafeFreeze :: forall s (n :: Nat) a. MutableVector s n a -> ST s (Vector n a)
freeze :: forall (n :: Nat) s a. Nat# n -> MutableVector s n a -> ST s (Vector n a)
freezeSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s a. ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s (Vector n a)
freeze# :: forall (n :: Nat) s a. Nat# n -> MutableVector# s n a -> State# s -> (# State# s, Vector# n a #)
freezeSlice# :: forall (i :: Natural) (n :: Natural) (m :: Nat) s a. ((i + n) <=# m) -> MutableVector# s m a -> Nat# i -> Nat# n -> State# s -> (# State# s, Vector# n a #)
thaw :: forall (n :: Nat) a s. Nat# n -> Vector n a -> ST s (MutableVector s n a)
tail :: forall (n :: Nat) a. Nat# n -> Vector (n + 1) a -> Vector n a
cons :: forall (n :: Nat) a. Nat# n -> Vector n a -> a -> Vector (n + 1) a
snoc :: forall (n :: Nat) a. Nat# n -> Vector n a -> a -> Vector (n + 1) a
replaceAt :: forall (n :: Nat) a. Nat# n -> Vector n a -> Fin# n -> a -> Vector n a
any :: forall a (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool
all :: forall a (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool
findIndex :: forall (n :: Nat) a. (a -> Bool) -> Nat# n -> Vector n a -> MaybeFin# n
map :: forall a (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a
traverse_ :: forall (n :: Nat) m a b. Monad m => (a -> m b) -> Nat# n -> Vector n a -> m ()
traverseZip_ :: forall (n :: Nat) m a b c. Monad m => (a -> b -> m c) -> Nat# n -> Vector n a -> Vector n b -> m ()
itraverse_ :: forall (n :: Nat) m a b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector n a -> m ()
traverseST# :: forall (n :: Nat) s a b. (a -> State# s -> (# State# s, b #)) -> Nat# n -> Vector# n a -> State# s -> (# State# s, Vector# n b #)
foldlM :: forall (n :: Nat) m a b. Monad m => (b -> a -> m b) -> b -> Nat# n -> Vector n a -> m b
ifoldl' :: forall (n :: Nat) a b. (b -> Fin# n -> a -> b) -> b -> Nat# n -> Vector n a -> b
ifoldlSlice' :: forall (i :: Nat) (m :: Nat) (n :: Nat) a b. ((i + n) <= m) -> (b -> Fin# (i + n) -> a -> b) -> b -> Vector m a -> Nat# i -> Nat# n -> b
ifoldr :: forall (n :: Nat) a b. (Fin# n -> a -> b -> b) -> b -> Nat# n -> Vector n a -> b
foldr :: forall (n :: Nat) a b. (a -> b -> b) -> b -> Nat# n -> Vector n a -> b
foldrZip :: forall (n :: Nat) a b c. (a -> b -> c -> c) -> c -> Nat# n -> Vector n a -> Vector n b -> c
replicate :: forall (n :: Nat) a. Nat# n -> a -> Vector n a
empty :: Vector 0 a
empty# :: (# #) -> Vector# 0 a
equals :: forall a (n :: Nat). Eq a => Nat# n -> Vector n a -> Vector n a -> Bool
construct1 :: a -> Vector 1 a
construct2 :: a -> a -> Vector 2 a
construct3 :: a -> a -> a -> Vector 3 a
construct4 :: a -> a -> a -> a -> Vector 4 a
construct5 :: a -> a -> a -> a -> a -> Vector 5 a
construct1# :: a -> Vector# 1 a
construct2# :: a -> a -> Vector# 2 a
construct3# :: a -> a -> a -> Vector# 3 a
construct4# :: a -> a -> a -> a -> Vector# 4 a
append :: forall (n :: Nat) (m :: Nat) a. Nat# n -> Nat# m -> Vector n a -> Vector m a -> Vector (n + m) a
clone :: forall (n :: Nat) a. Nat# n -> Vector n a -> Vector n a
cloneSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) a. ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a
index0 :: forall (n :: Natural) a. CmpNat 0 n ~ 'LT => Vector n a -> a
index1 :: forall (n :: Natural) a. CmpNat 1 n ~ 'LT => Vector n a -> a
index2 :: forall (n :: Natural) a. CmpNat 2 n ~ 'LT => Vector n a -> a
index3 :: forall (n :: Natural) a. CmpNat 3 n ~ 'LT => Vector n a -> a
index4 :: forall (n :: Natural) a. CmpNat 4 n ~ 'LT => Vector n a -> a
index5 :: forall (n :: Natural) a. CmpNat 5 n ~ 'LT => Vector n a -> a
index6 :: forall (n :: Natural) a. CmpNat 6 n ~ 'LT => Vector n a -> a
index7 :: forall (n :: Natural) a. CmpNat 7 n ~ 'LT => Vector n a -> a
index8 :: forall (n :: Natural) a. CmpNat 8 n ~ 'LT => Vector n a -> a
unsafeCoerceVector :: forall a b (n :: Nat). Vector n a -> Vector n b
with :: SmallArray a -> (forall (n :: Nat). Nat# n -> Vector n a -> b) -> b
toSmallArray :: forall (n :: Nat) a. Vector n a -> SmallArray a
fromList :: [a] -> Vector_ a
fromListN :: forall (n :: Nat) a. Nat# n -> [a] -> Maybe (Vector n a)
toList :: forall (n :: Nat) a. Vector n a -> [a]
vector_ :: forall (n :: Nat) a. Nat# n -> Vector n a -> Vector_ a
length :: forall (n :: Nat) a. Vector n a -> Nat# n

Documentation

data Vector (a :: Nat) b where #

Constructors

Vector :: forall (a :: Nat) b. Vector# a b -> Vector a b

data Vector# (a :: Nat) b :: UnliftedType #

data MutableVector a (b :: Nat) c where #

Constructors

MutableVector :: forall a (b :: Nat) c. MutableVector# a b c -> MutableVector a b c

data MutableVector# a (b :: Nat) c :: UnliftedType #

data Bounded (a :: Nat) b where #

Constructors

Bounded :: forall b (a :: Nat) (m :: Nat). Nat# m -> (m <=# a) -> Vector# m b -> Bounded a b

data Vector_ a where #

Constructors

Vector_ :: forall a (n :: Nat). Nat# n -> Vector# n a -> Vector_ a

type family FromMutability# (m :: Mutability) :: Nat -> TYPE R -> UnliftedType where ... #

Equations

FromMutability# 'Immutable = Vector#
FromMutability# ('Mutable s) = MutableVector# s

Primitives

write# :: forall s (n :: Nat) a. MutableVector# s n a -> Fin# n -> a -> State# s -> State# s #

write :: forall s (n :: Nat) a. MutableVector s n a -> Fin# n -> a -> ST s () #

read# :: forall s (n :: Nat) a. MutableVector# s n a -> Fin# n -> State# s -> (# State# s, a #) #

read :: forall s (n :: Nat) a. MutableVector s n a -> Fin# n -> ST s a Source #

index# :: forall (n :: Nat) a. Vector# n a -> Fin# n -> a #

index :: forall (n :: Nat) a. Vector n a -> Fin# n -> a #

unlift :: forall (n :: Nat) a. Vector n a -> Vector# n a #

substitute :: forall (m :: Nat) (n :: Nat) a. (m :=:# n) -> Vector m a -> Vector n a #

substitute# :: forall (m :: Nat) (n :: Nat) a. (m :=:# n) -> Vector# m a -> Vector# n a #

initialized :: forall s (n :: Nat) a. Nat# n -> a -> ST s (MutableVector s n a) #

initialized# :: forall s (n :: Nat) a. Nat# n -> a -> State# s -> (# State# s, MutableVector# s n a #) #

unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) a. Nat n -> Vector m a -> Vector n a #

Ranges

set :: forall s (n :: Nat) a. MutableVector s n a -> Nat# n -> a -> ST s () #

setSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s a. ((i + n) <=# m) -> MutableVector s n a -> Nat# i -> Nat# m -> a -> ST s () #

Freeze

unsafeShrinkFreeze :: forall s (n0 :: Nat) (n1 :: Nat) a. (n1 <=# n0) -> MutableVector s n0 a -> Nat# n1 -> ST s (Vector n1 a) #

unsafeFreeze :: forall s (n :: Nat) a. MutableVector s n a -> ST s (Vector n a) #

freeze :: forall (n :: Nat) s a. Nat# n -> MutableVector s n a -> ST s (Vector n a) #

freezeSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s a. ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s (Vector n a) #

freeze# :: forall (n :: Nat) s a. Nat# n -> MutableVector# s n a -> State# s -> (# State# s, Vector# n a #) #

freezeSlice# :: forall (i :: Natural) (n :: Natural) (m :: Nat) s a. ((i + n) <=# m) -> MutableVector# s m a -> Nat# i -> Nat# n -> State# s -> (# State# s, Vector# n a #) #

Copy

thaw :: forall (n :: Nat) a s. Nat# n -> Vector n a -> ST s (MutableVector s n a) #

Composite

tail :: forall (n :: Nat) a. Nat# n -> Vector (n + 1) a -> Vector n a #

cons :: forall (n :: Nat) a. Nat# n -> Vector n a -> a -> Vector (n + 1) a #

snoc :: forall (n :: Nat) a. Nat# n -> Vector n a -> a -> Vector (n + 1) a #

replaceAt :: forall (n :: Nat) a. Nat# n -> Vector n a -> Fin# n -> a -> Vector n a #

any :: forall a (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool #

all :: forall a (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool #

findIndex :: forall (n :: Nat) a. (a -> Bool) -> Nat# n -> Vector n a -> MaybeFin# n #

map :: forall a (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a #

traverse_ :: forall (n :: Nat) m a b. Monad m => (a -> m b) -> Nat# n -> Vector n a -> m () #

traverseZip_ :: forall (n :: Nat) m a b c. Monad m => (a -> b -> m c) -> Nat# n -> Vector n a -> Vector n b -> m () #

itraverse_ :: forall (n :: Nat) m a b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector n a -> m () #

traverseST# :: forall (n :: Nat) s a b. (a -> State# s -> (# State# s, b #)) -> Nat# n -> Vector# n a -> State# s -> (# State# s, Vector# n b #) #

foldlM :: forall (n :: Nat) m a b. Monad m => (b -> a -> m b) -> b -> Nat# n -> Vector n a -> m b #

ifoldl' :: forall (n :: Nat) a b. (b -> Fin# n -> a -> b) -> b -> Nat# n -> Vector n a -> b #

ifoldlSlice' :: forall (i :: Nat) (m :: Nat) (n :: Nat) a b. ((i + n) <= m) -> (b -> Fin# (i + n) -> a -> b) -> b -> Vector m a -> Nat# i -> Nat# n -> b #

ifoldr :: forall (n :: Nat) a b. (Fin# n -> a -> b -> b) -> b -> Nat# n -> Vector n a -> b #

foldr :: forall (n :: Nat) a b. (a -> b -> b) -> b -> Nat# n -> Vector n a -> b #

foldrZip :: forall (n :: Nat) a b c. (a -> b -> c -> c) -> c -> Nat# n -> Vector n a -> Vector n b -> c #

replicate :: forall (n :: Nat) a. Nat# n -> a -> Vector n a #

empty :: Vector 0 a #

empty# :: (# #) -> Vector# 0 a #

equals :: forall a (n :: Nat). Eq a => Nat# n -> Vector n a -> Vector n a -> Bool Source #

construct1 :: a -> Vector 1 a #

construct2 :: a -> a -> Vector 2 a #

construct3 :: a -> a -> a -> Vector 3 a #

construct4 :: a -> a -> a -> a -> Vector 4 a #

construct5 :: a -> a -> a -> a -> a -> Vector 5 a #

construct1# :: a -> Vector# 1 a #

construct2# :: a -> a -> Vector# 2 a #

construct3# :: a -> a -> a -> Vector# 3 a #

construct4# :: a -> a -> a -> a -> Vector# 4 a #

append :: forall (n :: Nat) (m :: Nat) a. Nat# n -> Nat# m -> Vector n a -> Vector m a -> Vector (n + m) a #

clone :: forall (n :: Nat) a. Nat# n -> Vector n a -> Vector n a #

cloneSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) a. ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a #

Index

index0 :: forall (n :: Natural) a. CmpNat 0 n ~ 'LT => Vector n a -> a #

index1 :: forall (n :: Natural) a. CmpNat 1 n ~ 'LT => Vector n a -> a #

index2 :: forall (n :: Natural) a. CmpNat 2 n ~ 'LT => Vector n a -> a #

index3 :: forall (n :: Natural) a. CmpNat 3 n ~ 'LT => Vector n a -> a #

index4 :: forall (n :: Natural) a. CmpNat 4 n ~ 'LT => Vector n a -> a #

index5 :: forall (n :: Natural) a. CmpNat 5 n ~ 'LT => Vector n a -> a #

index6 :: forall (n :: Natural) a. CmpNat 6 n ~ 'LT => Vector n a -> a #

index7 :: forall (n :: Natural) a. CmpNat 7 n ~ 'LT => Vector n a -> a #

index8 :: forall (n :: Natural) a. CmpNat 8 n ~ 'LT => Vector n a -> a #

Unsafe

unsafeCoerceVector :: forall a b (n :: Nat). Vector n a -> Vector n b #

Interop with primitive

with :: SmallArray a -> (forall (n :: Nat). Nat# n -> Vector n a -> b) -> b Source #

toSmallArray :: forall (n :: Nat) a. Vector n a -> SmallArray a Source #

Interop with lists

fromList :: [a] -> Vector_ a Source #

fromListN :: forall (n :: Nat) a. Nat# n -> [a] -> Maybe (Vector n a) Source #

toList :: forall (n :: Nat) a. Vector n a -> [a] Source #

Hide Length

vector_ :: forall (n :: Nat) a. Nat# n -> Vector n a -> Vector_ a #

Recover Length

length :: forall (n :: Nat) a. Vector n a -> Nat# n Source #