{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.TypeMap.Internal.Vector where
import Data.Vector (Vector)
import qualified Data.Vector as Vector
import Data.TypeMap.Internal.Unsafe
newtype TypeVector d = TypeVector (Vector Any)
type role TypeVector nominal
empty :: TypeVector '[]
empty :: TypeVector '[]
empty = Vector Any -> TypeVector '[]
forall k (d :: k). Vector Any -> TypeVector d
TypeVector Vector Any
forall a. Vector a
Vector.empty
index
:: forall a d
. KnownNat (Index a d)
=> TypeVector d -> Lookup a d
index :: TypeVector d -> Lookup a d
index = (forall c. Vector c -> Int -> c) -> TypeVector d -> Lookup a d
forall k (a :: k) (d :: [(k, *)]) (f :: * -> *)
(m :: [(k, *)] -> *).
(KnownNat (Index a d), Coercible (f Any) (m d)) =>
(forall c. f c -> Int -> c) -> m d -> Lookup a d
unsafeIndex @a forall c. Vector c -> Int -> c
(Vector.!)
cons
:: forall a d b
. b -> TypeVector d -> TypeVector ('(a, b) ': d)
cons :: b -> TypeVector d -> TypeVector ('(a, b) : d)
cons = (forall c. c -> Vector c -> Vector c)
-> b -> TypeVector d -> TypeVector ('(a, b) : d)
forall k (a :: k) (d :: [(k, *)]) b (f :: * -> *)
(m :: [(k, *)] -> *).
(Coercible (f Any) (m d), Coercible (f Any) (m ('(a, b) : d))) =>
(forall c. c -> f c -> f c) -> b -> m d -> m ('(a, b) : d)
unsafeCons forall c. c -> Vector c -> Vector c
Vector.cons
(<|)
:: forall a d b
. b -> TypeVector d -> TypeVector ('(a, b) ': d)
<| :: b -> TypeVector d -> TypeVector ('(a, b) : d)
(<|) = b -> TypeVector d -> TypeVector ('(a, b) : d)
forall k (a :: k) (d :: [(k, *)]) b.
b -> TypeVector d -> TypeVector ('(a, b) : d)
cons
infixr 5 <|, `cons`
snoc
:: forall a d b
. (Last d ~ '(a, b))
=> TypeVector (Init d) -> b -> TypeVector d
snoc :: TypeVector (Init d) -> b -> TypeVector d
snoc = (forall c. Vector c -> c -> Vector c)
-> TypeVector (Init d) -> b -> TypeVector d
forall k (a :: k) (d :: [(k, *)]) b (f :: * -> *)
(m :: [(k, *)] -> *).
(Last d ~ '(a, b), Coercible (f Any) (m (Init d)),
Coercible (f Any) (m d)) =>
(forall c. f c -> c -> f c) -> m (Init d) -> b -> m d
unsafeSnoc @a forall c. Vector c -> c -> Vector c
Vector.snoc
(|>)
:: forall a d b
. (Last d ~ '(a, b))
=> TypeVector (Init d) -> b -> TypeVector d
|> :: TypeVector (Init d) -> b -> TypeVector d
(|>) = TypeVector (Init d) -> b -> TypeVector d
forall k (a :: k) (d :: [(k, *)]) b.
(Last d ~ '(a, b)) =>
TypeVector (Init d) -> b -> TypeVector d
snoc
infixr 5 |>, `snoc`