Safe Haskell  None 

Language  Haskell2010 
Lazy lengthindexed list: Vec
.
 data Vec (n :: Nat) a where
 empty :: Vec Z a
 singleton :: a > Vec (S Z) a
 withDict :: Vec n a > (InlineInduction n => r) > r
 toPull :: Vec n a > Vec n a
 fromPull :: forall n a. SNatI n => Vec n a > Vec n a
 _Pull :: SNatI n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b)
 toList :: Vec n a > [a]
 fromList :: SNatI n => [a] > Maybe (Vec n a)
 _Vec :: SNatI n => Prism' [a] (Vec n a)
 fromListPrefix :: SNatI n => [a] > Maybe (Vec n a)
 reifyList :: [a] > (forall n. InlineInduction n => Vec n a > r) > r
 (!) :: Vec n a > Fin n > a
 ix :: Fin n > Lens' (Vec n a) a
 _Cons :: Iso (Vec (S n) a) (Vec (S n) b) (a, Vec n a) (b, Vec n b)
 _head :: Lens' (Vec (S n) a) a
 _tail :: Lens' (Vec (S n) a) (Vec n a)
 cons :: a > Vec n a > Vec (S n) a
 head :: Vec (S n) a > a
 tail :: Vec (S n) a > Vec n a
 (++) :: 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 :: (a > Vec m b) > Vec n a > Vec (Mult n m) b
 concat :: 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 => (a > m) > Vec n a > m
 foldMap1 :: Semigroup s => (a > s) > Vec (S n) a > s
 ifoldMap :: Monoid m => (Fin n > a > m) > Vec n a > m
 ifoldMap1 :: Semigroup s => (Fin (S n) > a > s) > Vec (S n) a > s
 foldr :: forall a b n. (a > b > b) > b > Vec n a > b
 ifoldr :: forall a b n. (Fin n > a > b > b) > b > Vec n a > b
 foldl' :: forall a b n. (b > a > b) > b > Vec n a > b
 length :: Vec n a > Int
 null :: Vec n a > Bool
 sum :: Num a => Vec n a > a
 product :: Num a => Vec n a > a
 map :: (a > b) > Vec n a > Vec n b
 imap :: (Fin n > a > b) > Vec n a > Vec n b
 traverse :: forall n f a b. Applicative f => (a > f b) > Vec n a > f (Vec n b)
 traverse1 :: forall n f a b. Apply f => (a > f b) > Vec (S n) a > f (Vec (S n) b)
 itraverse :: Applicative f => (Fin n > a > f b) > Vec n a > f (Vec n b)
 itraverse_ :: Applicative f => (Fin n > a > f b) > Vec n a > f ()
 zipWith :: (a > b > c) > Vec n a > Vec n b > Vec n c
 izipWith :: (Fin n > a > b > c) > Vec n a > Vec n b > Vec n c
 bind :: Vec n a > (a > Vec n b) > Vec n b
 join :: Vec n (Vec n a) > Vec n a
 universe :: SNatI n => Vec n (Fin n)
 class Each s t a b => VecEach s t a b  s > a, t > b, s b > t, t a > s where
Documentation
data Vec (n :: Nat) a where Source #
Vector, i.e. lengthindexed list.
SNatI n => Monad (Vec n) Source #  
Functor (Vec n) Source #  
SNatI n => Applicative (Vec n) Source #  
Foldable (Vec n) Source #  
Traversable (Vec n) Source #  
SNatI n => Distributive (Vec n) Source #  
SNatI n => Representable (Vec n) Source #  
Apply (Vec n) Source #  
(~) Nat n (S m) => Traversable1 (Vec n) Source #  
(~) Nat n (S m) => Foldable1 (Vec n) Source #  
Bind (Vec n) Source #  
FunctorWithIndex (Fin n) (Vec n) Source #  
FoldableWithIndex (Fin n) (Vec n) Source #  
TraversableWithIndex (Fin n) (Vec n) Source #  
Eq a => Eq (Vec n a) Source #  
Ord a => Ord (Vec n a) Source #  
Show a => Show (Vec n a) Source #  
Semigroup a => Semigroup (Vec n a) Source #  
(Monoid a, SNatI n) => Monoid (Vec n a) Source #  
NFData a => NFData (Vec n a) Source #  
Hashable a => Hashable (Vec n a) Source #  
Ixed (Vec n a) Source # 

Each (Vec n a) (Vec n b) a b Source #  
Field1 (Vec (S n) a) (Vec (S n) a) a a Source #  
Field2 (Vec (S (S n)) a) (Vec (S (S n)) a) a a Source #  
Field3 (Vec (S (S (S n))) a) (Vec (S (S (S n))) a) a a Source #  
Field4 (Vec (S (S (S (S n)))) a) (Vec (S (S (S (S n)))) a) a a Source #  
Field5 (Vec (S (S (S (S (S n))))) a) (Vec (S (S (S (S (S n))))) a) a a Source #  
Field6 (Vec (S (S (S (S (S (S n)))))) a) (Vec (S (S (S (S (S (S n)))))) a) a a Source #  
Field7 (Vec (S (S (S (S (S (S (S n))))))) a) (Vec (S (S (S (S (S (S (S n))))))) a) a a Source #  
Field8 (Vec (S (S (S (S (S (S (S (S n)))))))) a) (Vec (S (S (S (S (S (S (S (S n)))))))) a) a a Source #  
Field9 (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) a a Source #  
type Rep (Vec n) Source #  
type Index (Vec n a) Source #  
type IxValue (Vec n a) Source #  
Construction
withDict :: Vec n a > (InlineInduction n => r) > r Source #
O(n). Recover InlineInduction
(and SNatI
) dictionary from a Vec
value.
Example: reflect
is constrained with
, but if we have a
SNatI
n
, we can recover that dictionary:Vec
n a
>>>
let f :: forall n a. Vec n a > N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)
1
Note: using InlineInduction
will be suboptimal, as if GHC has no
opportunity to optimise the code, the recusion won't be unfold.
How bad such code will perform? I don't know, we'll need benchmarks.
Conversions
toList :: Vec n a > [a] Source #
Convert Vec
to list.
>>>
toList $ 'f' ::: 'o' ::: 'o' ::: VNil
"foo"
_Vec :: SNatI n => Prism' [a] (Vec n a) Source #
Prism from list.
>>>
"foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
Just ('f' ::: 'o' ::: 'o' ::: VNil)
>>>
"foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
Nothing
>>>
_Vec # (True ::: False ::: VNil)
[True,False]
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. InlineInduction n => Vec n a > r) > r Source #
Reify any list [a]
to
.Vec
n a
>>>
reifyList "foo" length
3
Indexing
ix :: Fin n > Lens' (Vec n a) a Source #
Index lens.
>>>
('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)
'b'
>>>
('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'
'a' ::: 'x' ::: 'c' ::: VNil
_head :: Lens' (Vec (S n) a) a Source #
Head lens. Note: lens
_head
is a Traversal'
.
>>>
('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
'a'
>>>
('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
'x' ::: 'b' ::: 'c' ::: VNil
Concatenation and splitting
(++) :: 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
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
ifoldMap1 :: Semigroup s => (Fin (S n) > a > s) > Vec (S n) a > s Source #
There is no typeclass for this :(
ifoldr :: forall a b n. (Fin n > a > b > b) > b > Vec n a > b Source #
Right fold with an index.
Special folds
Mapping
map :: (a > b) > Vec n a > Vec n b Source #
>>>
map not $ True ::: False ::: VNil
False ::: True ::: VNil
imap :: (Fin n > a > b) > Vec n a > Vec n b Source #
>>>
imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
(0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
itraverse_ :: Applicative f => (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
izipWith :: (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.
Monadic
join :: Vec n (Vec n a) > Vec n a Source #
Monadic join.
>>>
join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
'a' ::: 'd' ::: VNil
Universe
VecEach
class Each s t a b => VecEach s t a b  s > a, t > b, s b > t, t a > s where Source #
Write functions on Vec
. Use them with tuples.
VecEach
can be used to avoid "this function won't change the length of the
list" in DSLs.
bad: Instead of
[x, y] < badDslMagic ["foo", "bar"]  list!
good: we can write
(x, y) < betterDslMagic ("foo", "bar")  homogenic tuple!
where betterDslMagic
can be defined using traverseWithVec
.
mapWithVec :: (forall n. InlineInduction n => Vec n a > Vec n b) > s > t Source #
traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a > f (Vec n b)) > s > f t Source #