Data.FastVect.FastVect

data Vect :: Symbol -> Type -> Typedata Vect len elem

A Vector: A list-like data structure that encodes it's length in the type, backed by an Array.

vect :: Vect "1" String
vect = singleton "a"

Instances

• (IsSymbol len, Show elem) => Show (Vect len elem)
• (Eq elem) => Eq (Vect len elem)
• Functor (Vect len)

replicate :: forall len elem. ToInt len => Proxy len -> elem -> Vect len elem

Create a Vect by replicating len times the given element

vect :: Vect "300" String
vect = replicate (term :: _ "300") "a"

empty :: forall elem. Vect "0" elem

Creates the empty Vect.

vect :: Vect "0" String
vect = empty

singleton :: forall elem. elem -> Vect "1" elem

Create a Vect of one element.

vect :: Vect "1" String
vect = singleton "a"

append :: forall m n elem carry sum m_plus_n_untrimmed m_plus_n m_aligned n_aligned. PadZeroes m n m_aligned n_aligned => Add m_aligned n_aligned carry sum => Cons carry sum m_plus_n_untrimmed => Trim m_plus_n_untrimmed m_plus_n => Vect m elem -> Vect n elem -> Vect m_plus_n elem

Append two Vects.

as :: Vect "300" String
as = replicate (term :: _ "300") "a"

bs :: Vect "200" String
bs = replicate (term :: _ "200") "b"

cs :: Vect "500" String
cs = append as bs

drop :: forall m n elem m_aligned m_plus_n_aligned n_untrimmed m_plus_n. ToInt m => PadZeroes m m_plus_n m_aligned m_plus_n_aligned => Add m_aligned n_untrimmed "0" m_plus_n_aligned => Trim n_untrimmed n => Proxy m -> Vect m_plus_n elem -> Vect n elem

Safely drop m elements from a Vect. Will result in a compile-time error if you are trying to drop more elements than exist in the vector.

vect :: Vect "300" String
vect = replicate (term :: _ "300") "a"

newVect :: Vect "200" String
newVect = drop (term :: _ "100") vect

take :: forall m n elem m_plus_n m_aligned m_aligned_plus_n n_untrimmed. ToInt m => PadZeroes m m_plus_n m_aligned m_aligned_plus_n => Add m_aligned n_untrimmed "0" m_aligned_plus_n => Trim n_untrimmed n => Proxy m -> Vect m_plus_n elem -> Vect m elem

Safely take m elements from a Vect. Will result in a compile-time error if you are trying to take more elements than exist in the vector.

vect :: Vect "300" String
vect = replicate (term :: _ "300") "a"

newVect :: Vect "100" String
newVect = take (term :: _ "100") vect

index :: forall m m_minus_one aligned_one m_aligned m_aligned_minus_one i i_aligned n elem. ToInt i => PadZeroes "1" m aligned_one m_aligned => Add aligned_one m_minus_one "0" m_aligned => PadZeroes i m_minus_one i_aligned m_aligned_minus_one => Add i_aligned n "0" m_aligned_minus_one => Proxy i -> Vect m elem -> elem

Safely access the i-th element of a Vect.

vect :: Vect "300" String
vect = replicate (term :: _ "300") "a"

elem :: String
elem = index (term :: _ "299") vect

head :: forall m m_minus_one aligned_one m_aligned m_aligned_minus_one i_aligned n elem. PadZeroes "1" m aligned_one m_aligned => Add aligned_one m_minus_one "0" m_aligned => PadZeroes "0" m_minus_one i_aligned m_aligned_minus_one => Add i_aligned n "0" m_aligned_minus_one => Vect m elem -> elem

Safely access the head of a Vect.

vect :: Vect "300" String
vect = replicate (term :: _ "300") "a"

elem :: String
elem = head vect

splitAt :: forall m n elem m_aligned m_plus_n_aligned n_untrimmed m_plus_n. ToInt m => PadZeroes m m_plus_n m_aligned m_plus_n_aligned => Add m_aligned n_untrimmed "0" m_plus_n_aligned => Trim n_untrimmed n => Proxy m -> Vect m_plus_n elem -> { after :: Vect n elem, before :: Vect m elem }

Split the Vect into two sub vectors before and after, where before contains up to m elements.

vect ∷ Vect "10" String
vect = replicate (term ∷ _ "10") "a"

split ∷
  { after ∷ Vect "7" String
  , before ∷ Vect "3" String
  }
split = splitAt (term ∷ _ "3") vect

fromArray :: forall len elem. ToInt len => Proxy len -> Array elem -> Maybe (Vect len elem)

Attempt to create a Vect of a given size from an Array.

fromArray (term :: _ "3") ["a", "b", "c"] = Just (Vect (term :: _ "3") ["a", "b", "c"])

fromArray (term :: _ "4") ["a", "b", "c"] = Nothing

toArray :: forall len elem. Vect len elem -> Array elem

Converts the Vect to an Array, effectively dropping the size information.

adjust :: forall len elem. ToInt len => Proxy len -> elem -> Array elem -> Vect len elem

Creates a Vect by adjusting the given Array, padding with the provided element if the array is to small or dropping elements if the array is to big.

toArray $ adjust (term ∷ _ "10") 0 [ 1, 2, 3 ] == [ 0, 0, 0, 0, 0, 0, 0, 1, 2, 3 ]

toArray $ adjust (term ∷ _ "3") 0 [ 0, 0, 0, 0, 1, 2, 3 ] == [ 1, 2, 3 ]

adjustM :: forall len elem. Monoid elem => ToInt len => Proxy len -> Array elem -> Vect len elem

Like adjust but uses the Moinoid instance of elem to create the elements.

cons :: forall len elem one_aligned len_aligned carry sum len_plus_1_untrimmed len_plus_1. PadZeroes "1" len one_aligned len_aligned => Add one_aligned len carry sum => Cons carry sum len_plus_1_untrimmed => Trim len_plus_1_untrimmed len_plus_1 => elem -> Vect len elem -> Vect len_plus_1 elem

Attaches an element to the front of the Vect, creating a new Vect with size incremented.

Note, the running time of this function is O(n).

Operator alias for Data.FastVect.FastVect.cons (right-associative / precedence 6)