Stability | experimental |
---|---|
Maintainer | conal@conal.net |
Experiment in length-typed vectors
- data Z
- data S n
- type family a :+: b
- type ZeroT = Z
- type OneT = S ZeroT
- type TwoT = S OneT
- type ThreeT = S TwoT
- type FourT = S ThreeT
- data Nat where
- zero :: Nat ZeroT
- one :: Nat OneT
- two :: Nat TwoT
- three :: Nat ThreeT
- four :: Nat FourT
- withIsNat :: (IsNat n => Nat n -> a) -> Nat n -> a
- natSucc :: Nat n -> Nat (S n)
- natIsNat :: Nat n -> IsNat n => Nat n
- natToZ :: Nat n -> Integer
- natEq :: Nat m -> Nat n -> Maybe (m :=: n)
- natAdd :: Nat m -> Nat n -> Nat (m :+: n)
- data m :<: n
- data Index lim = forall n . IsNat n => Index (n :<: lim) (Nat n)
- succI :: Index m -> Index (S m)
- index0 :: Index (S n)
- index1 :: Index (S (S n))
- index2 :: Index (S (S (S n)))
- index3 :: Index (S (S (S (S n))))
- data Vec where
- class IsNat n where
- (<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) a
- indices :: Nat n -> Vec n (Index n)
- type Zero = Vec ZeroT
- type One = Vec OneT
- type Two = Vec TwoT
- type Three = Vec ThreeT
- type Four = Vec FourT
- vElems :: Vec n a -> [a]
- vec1 :: a -> One a
- vec2 :: a -> a -> Two a
- vec3 :: a -> a -> a -> Three a
- vec4 :: a -> a -> a -> a -> Four a
- un1 :: One a -> a
- un2 :: Two a -> (a, a)
- un3 :: Three a -> (a, a, a)
- un4 :: Four a -> (a, a, a, a)
- get0 :: Vec (S n) a -> One a
- get1 :: Vec (S (S n)) a -> One a
- get2 :: Vec (S (S (S n))) a -> One a
- get3 :: Vec (S (S (S (S n)))) a -> One a
- get :: Index n -> Vec n a -> One a
- swizzle :: Vec n (Index m) -> Vec m a -> Vec n a
Type-level numbers
Type-level representation of zero
Type-level representation of successor
Typed natural numbers
A number under the given limit, with proof
Vectors
Vectors with type-determined length, having empty vector (ZVec
) and
vector cons ('(:<)').
(IsNat n, IsScalar a, Show a) => IfB BoolE (VecE n a) | |
(IsNat n, IsScalar b, Floating b) => Floating (E (Vec n b)) | |
(IsNat n, IsScalar b, Fractional b) => Fractional (E (Vec n b)) | |
(IsNat n, IsScalar b, Integral b) => Integral (E (Vec n b)) | |
Functor (Vec n) | |
(IsNat n, IsScalar a, Num a) => Num (E (Vec n a)) | |
(IsNat n, IsScalar a, Ord a, Show a) => Ord (E (Vec n a)) | |
(IsNat n, IsScalar a, Ord a, Num a) => Real (E (Vec n a)) | |
(IsNat n, IsScalar b, RealFrac b) => RealFrac (E (Vec n b)) | |
IsNat n => Applicative (Vec n) | |
Foldable (Vec n) | |
(IsNat n, IsScalar a, Num a) => VectorSpace (E (Vec n a)) | |
IsNat n => InnerSpace (E (Vec n R)) | |
(IsNat n, IsScalar a, Num a) => AdditiveGroup (E (Vec n a)) | |
(IsNat n, IsScalar a, FMod a) => FMod (E (Vec n a)) | |
(IsNat n, IsScalar a, FMod a, RealFrac a) => Frac (E (Vec n a)) | |
(Show a, IsScalar a) => FromE (ComplexE a) | |
(Show a, IsScalar a) => ToE (ComplexE a) | |
(IsNat n, IsScalar applicative_arg, Enum applicative_arg) => Enum (Vec n applicative_arg) | |
Eq a => Eq (Vec n a) | |
(IsNat n, IsScalar applicative_arg, Floating applicative_arg) => Floating (Vec n applicative_arg) | |
(IsNat n, IsScalar applicative_arg, Fractional applicative_arg) => Fractional (Vec n applicative_arg) | |
(IsNat n, IsScalar applicative_arg, Integral applicative_arg) => Integral (Vec n applicative_arg) | |
(IsNat n, IsScalar applicative_arg, Num applicative_arg) => Num (Vec n applicative_arg) | |
Ord a => Ord (Vec n a) | |
(IsNat n, IsScalar applicative_arg, Num applicative_arg, Ord applicative_arg) => Real (Vec n applicative_arg) | |
(IsNat n, IsScalar applicative_arg, RealFloat applicative_arg) => RealFloat (Vec n applicative_arg) | |
(IsNat n, IsScalar applicative_arg, RealFrac applicative_arg) => RealFrac (Vec n applicative_arg) | |
(IsNat n, IsScalar a, Show a) => Show (Vec n a) | |
IsNat n => Boolean (VecE n Bool) | |
(IsNat n, Storable a) => Storable (Vec n a) | |
(IsNat n, Num a) => VectorSpace (Vec n a) | |
(IsNat n, Num a) => InnerSpace (Vec n a) | |
(IsNat n, Num a) => AdditiveGroup (Vec n a) | |
(IsNat n, IsScalar a, Pretty a) => Pretty (Vec n a) | |
(IsNat n, IsScalar a, FMod a) => FMod (Vec n a) | |
(IsNat n, IsScalar a, Pretty a) => PrettyPrec (Vec n a) | |
(IsNat n, IsScalar a, Show a) => HasExpr (Vec n a) | |
(IsNat n, IsScalar a) => HasType (Vec n a) | |
(IsNat n, IsScalar a, Eq a, Show a) => EqB (VecE n Bool) (VecE n a) | |
(IsNat n, IsScalar a, Ord a, Show a) => OrdB (VecE n Bool) (VecE n a) |
vElems :: Vec n a -> [a]Source
Enumerate the elements of a vector. See also elemsV
vElems :: Vec n a -> [a]
vElems ZVec = []
vElems (a :< as) = a : vElems as