Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Spine-strict length-indexed list defined as data-family: Vec
.
Data family variant allows lazy pattern matching.
On the other hand, the Vec
value doesn't "know" its length (i.e. there isn't withDict
).
Agda
If you happen to familiar with Agda, then the difference between GADT and data-family version is maybe clearer:
module Vec where open import Data.Nat open import Relation.Binary.PropositionalEquality using (_≡_; refl) -- "GADT" data Vec (A : Set) : ℕ → Set where [] : Vec A 0 _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) infixr 50 _∷_ exVec : Vec ℕ 2 exVec = 13 ∷ 37 ∷ [] -- "data family" data Unit : Set where [] : Unit data _×_ (A B : Set) : Set where _∷_ : A → B → A × B infixr 50 _×_ VecF : Set → ℕ → Set VecF A zero = Unit VecF A (suc n) = A × VecF A n exVecF : VecF ℕ 2 exVecF = 13 ∷ 37 ∷ [] reduction : VecF ℕ 2 ≡ ℕ × ℕ × Unit reduction = refl
Synopsis
- data family Vec (n :: Nat) a
- empty :: Vec 'Z a
- singleton :: a -> Vec ('S 'Z) a
- toPull :: forall n a. SNatI n => Vec n a -> Vec n a
- fromPull :: forall n a. SNatI n => Vec n a -> Vec n a
- toList :: forall n a. SNatI n => Vec n a -> [a]
- toNonEmpty :: forall n a. SNatI n => Vec ('S n) a -> NonEmpty a
- fromList :: SNatI n => [a] -> Maybe (Vec n a)
- fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a)
- reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r
- (!) :: SNatI n => Vec n a -> Fin n -> a
- tabulate :: SNatI n => (Fin n -> a) -> Vec n a
- cons :: a -> Vec n a -> Vec ('S n) a
- snoc :: forall n a. SNatI n => Vec n a -> a -> Vec ('S n) a
- head :: Vec ('S n) a -> a
- last :: forall n a. SNatI n => Vec ('S n) a -> a
- tail :: Vec ('S n) a -> Vec n a
- init :: forall n a. SNatI n => Vec ('S n) a -> Vec n a
- reverse :: forall n a. SNatI n => Vec n a -> Vec n a
- (++) :: forall n m a. SNatI n => Vec n a -> Vec m a -> Vec (Plus n m) a
- split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a)
- concatMap :: forall a b n m. (SNatI m, SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
- concat :: (SNatI m, SNatI n) => Vec n (Vec m a) -> Vec (Mult n m) a
- chunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a)
- foldMap :: (Monoid m, SNatI n) => (a -> m) -> Vec n a -> m
- foldMap1 :: forall s a n. (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s
- ifoldMap :: forall a n m. (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
- ifoldMap1 :: forall a n s. (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
- foldr :: forall a b n. SNatI n => (a -> b -> b) -> b -> Vec n a -> b
- ifoldr :: forall a b n. SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
- length :: forall n a. SNatI n => Vec n a -> Int
- null :: forall n a. SNatI n => Vec n a -> Bool
- sum :: (Num a, SNatI n) => Vec n a -> a
- product :: (Num a, SNatI n) => Vec n a -> a
- map :: forall a b n. SNatI n => (a -> b) -> Vec n a -> Vec n b
- imap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b
- traverse :: forall n f a b. (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)
- traverse1 :: forall n f a b. (Apply f, SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
- itraverse :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
- itraverse_ :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()
- zipWith :: forall a b c n. SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- izipWith :: SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- repeat :: SNatI n => x -> Vec n x
- bind :: SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b
- join :: SNatI n => Vec n (Vec n a) -> Vec n a
- universe :: SNatI n => Vec n (Fin n)
- ensureSpine :: SNatI n => Vec n a -> Vec n a
Documentation
data family Vec (n :: Nat) a infixr 5 Source #
Vector, i.e. length-indexed list.
Instances
SNatI n => Arbitrary1 (Vec n) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict liftArbitrary :: Gen a -> Gen (Vec n a) # liftShrink :: (a -> [a]) -> Vec n a -> [Vec n a] # | |
SNatI n => Representable (Vec n) Source # | |
SNatI n => Foldable (Vec n) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict fold :: Monoid m => Vec n m -> m # foldMap :: Monoid m => (a -> m) -> Vec n a -> m # foldMap' :: Monoid m => (a -> m) -> Vec n a -> m # foldr :: (a -> b -> b) -> b -> Vec n a -> b # foldr' :: (a -> b -> b) -> b -> Vec n a -> b # foldl :: (b -> a -> b) -> b -> Vec n a -> b # foldl' :: (b -> a -> b) -> b -> Vec n a -> b # foldr1 :: (a -> a -> a) -> Vec n a -> a # foldl1 :: (a -> a -> a) -> Vec n a -> a # elem :: Eq a => a -> Vec n a -> Bool # maximum :: Ord a => Vec n a -> a # minimum :: Ord a => Vec n a -> a # | |
(SNatI m, n ~ 'S m) => Foldable1 (Vec n) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict fold1 :: Semigroup m => Vec n m -> m # foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m # foldMap1' :: Semigroup m => (a -> m) -> Vec n a -> m # toNonEmpty :: Vec n a -> NonEmpty a # maximum :: Ord a => Vec n a -> a # minimum :: Ord a => Vec n a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> Vec n a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> Vec n a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> Vec n a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> Vec n a -> b # | |
SNatI n => Eq1 (Vec n) Source # | Since: 0.4 |
SNatI n => Ord1 (Vec n) Source # | Since: 0.4 |
Defined in Data.Vec.DataFamily.SpineStrict | |
SNatI n => Show1 (Vec n) Source # | Since: 0.4 |
SNatI n => Traversable (Vec n) Source # | |
SNatI n => Applicative (Vec n) Source # | |
SNatI n => Functor (Vec n) Source # | |
SNatI n => Monad (Vec n) Source # | |
SNatI n => Distributive (Vec n) Source # | |
SNatI n => Apply (Vec n) Source # | |
SNatI n => Bind (Vec n) Source # | |
(SNatI m, n ~ 'S m) => Traversable1 (Vec n) Source # | |
SNatI n => FoldableWithIndex (Fin n) (Vec n) Source # | Since: 0.4 |
Defined in Data.Vec.DataFamily.SpineStrict | |
SNatI n => FunctorWithIndex (Fin n) (Vec n) Source # | Since: 0.4 |
SNatI n => TraversableWithIndex (Fin n) (Vec n) Source # | Since: 0.4 |
Defined in Data.Vec.DataFamily.SpineStrict | |
(SNatI n, Arbitrary a) => Arbitrary (Vec n a) Source # | |
(SNatI n, CoArbitrary a) => CoArbitrary (Vec n a) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict coarbitrary :: Vec n a -> Gen b -> Gen b # | |
(SNatI n, Function a) => Function (Vec n a) Source # | |
(Monoid a, SNatI n) => Monoid (Vec n a) Source # | |
(Semigroup a, SNatI n) => Semigroup (Vec n a) Source # | |
(Show a, SNatI n) => Show (Vec n a) Source # | |
(NFData a, SNatI n) => NFData (Vec n a) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict | |
(Eq a, SNatI n) => Eq (Vec n a) Source # |
|
(Ord a, SNatI n) => Ord (Vec n a) Source # |
|
Defined in Data.Vec.DataFamily.SpineStrict | |
(Hashable a, SNatI n) => Hashable (Vec n a) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict | |
data Vec 'Z a Source # | |
Defined in Data.Vec.DataFamily.SpineStrict | |
type Rep (Vec n) Source # | |
Defined in Data.Vec.DataFamily.SpineStrict | |
data Vec ('S n) a Source # | |
Defined in Data.Vec.DataFamily.SpineStrict |
Construction
singleton :: a -> Vec ('S 'Z) a Source #
Vec
with exactly one element.
>>>
singleton True
True ::: VNil
Conversions
toList :: forall n a. SNatI n => Vec n a -> [a] Source #
Convert Vec
to list.
>>>
toList $ 'f' ::: 'o' ::: 'o' ::: VNil
"foo"
toNonEmpty :: forall n a. SNatI n => Vec ('S n) a -> NonEmpty a Source #
>>>
toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
1 :| [2,3]
Since: 0.4
fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a) Source #
Convert list [a]
to
.
Returns Vec
n aNothing
if input list is too short.
>>>
fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)
Just ('f' ::: 'o' ::: 'o' ::: VNil)
>>>
fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)
Just ('q' ::: 'u' ::: 'u' ::: VNil)
>>>
fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)
Nothing
reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r Source #
Reify any list [a]
to
.Vec
n a
>>>
reifyList "foo" length
3
Indexing
(!) :: SNatI n => Vec n a -> Fin n -> a Source #
Indexing.
>>>
('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
'b'
tabulate :: SNatI n => (Fin n -> a) -> Vec n a Source #
Tabulating, inverse of !
.
>>>
tabulate id :: Vec N.Nat3 (Fin N.Nat3)
0 ::: 1 ::: 2 ::: VNil
snoc :: forall n a. SNatI n => Vec n a -> a -> Vec ('S n) a Source #
Add a single element at the end of a Vec
.
Reverse
Concatenation and splitting
(++) :: forall n m a. SNatI n => Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5 Source #
Append two Vec
.
>>>
('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a) Source #
Split vector into two parts. Inverse of ++
.
>>>
split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)
('a' ::: VNil,'b' ::: 'c' ::: VNil)
>>>
uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))
'a' ::: 'b' ::: 'c' ::: VNil
concatMap :: forall a b n m. (SNatI m, SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b Source #
chunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a) Source #
Inverse of concat
.
>>>
chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))
Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)
>>>
let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)
>>>
concat . idVec . chunks <$> fromListPrefix [1..]
Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)
Folds
foldMap1 :: forall s a n. (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s Source #
See Foldable1
.
ifoldMap :: forall a n m. (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m Source #
See FoldableWithIndex
.
ifoldMap1 :: forall a n s. (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s Source #
There is no type-class for this :(
ifoldr :: forall a b n. SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b Source #
Right fold with an index.
Special folds
Mapping
map :: forall a b n. SNatI n => (a -> b) -> Vec n a -> Vec n b Source #
>>>
map not $ True ::: False ::: VNil
False ::: True ::: VNil
imap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b Source #
>>>
imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
(0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
traverse :: forall n f a b. (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b) Source #
traverse1 :: forall n f a b. (Apply f, SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b) Source #
itraverse :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) Source #
itraverse_ :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f () Source #
Apply an action to every element of a Vec
and its index, ignoring the results.
Zipping
zipWith :: forall a b c n. SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #
Zip two Vec
s with a function.
izipWith :: SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #
Zip two Vec
s. with a function that also takes the elements' indices.
repeat :: SNatI n => x -> Vec n x Source #
Repeat value
>>>
repeat 'x' :: Vec N.Nat3 Char
'x' ::: 'x' ::: 'x' ::: VNil
Since: 0.2.1
Monadic
join :: SNatI n => Vec n (Vec n a) -> Vec n a Source #
Monadic join.
>>>
join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
'a' ::: 'd' ::: VNil
Universe
Extras
ensureSpine :: SNatI n => Vec n a -> Vec n a Source #
Ensure spine.
If we have an undefined Vec
,
>>>
let v = error "err" :: Vec N.Nat3 Char
And insert data into it later:
>>>
let setHead :: a -> Vec ('S n) a -> Vec ('S n) a; setHead x (_ ::: xs) = x ::: xs
Then without a spine, it will fail:
>>>
head $ setHead 'x' v
*** Exception: err ...
But with the spine, it won't:
>>>
head $ setHead 'x' $ ensureSpine v
'x'