type-unary-0.3.2: Type-level and typed unary natural numbers, inequality proofs, vectors

Copyright(c) Conal Elliott 2009
LicenseBSD3
Maintainerconal@conal.net
Stabilityexperimental
Safe HaskellSafe
LanguageHaskell98

TypeUnary.Vec

Contents

Description

Experiment in length-typed vectors

Synopsis

Documentation

Vectors

data Vec :: * -> * -> * where Source #

Vectors with type-determined length, having empty vector (ZVec) and vector cons ('(:<)').

Constructors

ZVec :: Vec Z a 
(:<) :: a -> Vec n a -> Vec (S n) a infixr 5 

Instances

IsNat n => Monad (Vec n) Source # 

Methods

(>>=) :: Vec n a -> (a -> Vec n b) -> Vec n b #

(>>) :: Vec n a -> Vec n b -> Vec n b #

return :: a -> Vec n a #

fail :: String -> Vec n a #

Functor (Vec n) Source # 

Methods

fmap :: (a -> b) -> Vec n a -> Vec n b #

(<$) :: a -> Vec n b -> Vec n a #

IsNat n => Applicative (Vec n) Source # 

Methods

pure :: a -> Vec n a #

(<*>) :: Vec n (a -> b) -> Vec n a -> Vec n b #

liftA2 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c #

(*>) :: Vec n a -> Vec n b -> Vec n b #

(<*) :: Vec n a -> Vec n b -> Vec n a #

Foldable (Vec n) Source # 

Methods

fold :: Monoid m => Vec n m -> 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 #

toList :: Vec n a -> [a] #

null :: Vec n a -> Bool #

length :: Vec n a -> Int #

elem :: Eq a => a -> Vec n a -> Bool #

maximum :: Ord a => Vec n a -> a #

minimum :: Ord a => Vec n a -> a #

sum :: Num a => Vec n a -> a #

product :: Num a => Vec n a -> a #

Traversable (Vec n) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) #

sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a) #

mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b) #

sequence :: Monad m => Vec n (m a) -> m (Vec n a) #

(IsNat n, Enum applicative_arg) => Enum (Vec n applicative_arg) # 

Methods

succ :: Vec n applicative_arg -> Vec n applicative_arg #

pred :: Vec n applicative_arg -> Vec n applicative_arg #

toEnum :: Int -> Vec n applicative_arg #

fromEnum :: Vec n applicative_arg -> Int #

enumFrom :: Vec n applicative_arg -> [Vec n applicative_arg] #

enumFromThen :: Vec n applicative_arg -> Vec n applicative_arg -> [Vec n applicative_arg] #

enumFromTo :: Vec n applicative_arg -> Vec n applicative_arg -> [Vec n applicative_arg] #

enumFromThenTo :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg -> [Vec n applicative_arg] #

Eq a => Eq (Vec n a) Source # 

Methods

(==) :: Vec n a -> Vec n a -> Bool #

(/=) :: Vec n a -> Vec n a -> Bool #

(IsNat n, Floating applicative_arg) => Floating (Vec n applicative_arg) # 

Methods

pi :: Vec n applicative_arg #

exp :: Vec n applicative_arg -> Vec n applicative_arg #

log :: Vec n applicative_arg -> Vec n applicative_arg #

sqrt :: Vec n applicative_arg -> Vec n applicative_arg #

(**) :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

logBase :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

sin :: Vec n applicative_arg -> Vec n applicative_arg #

cos :: Vec n applicative_arg -> Vec n applicative_arg #

tan :: Vec n applicative_arg -> Vec n applicative_arg #

asin :: Vec n applicative_arg -> Vec n applicative_arg #

acos :: Vec n applicative_arg -> Vec n applicative_arg #

atan :: Vec n applicative_arg -> Vec n applicative_arg #

sinh :: Vec n applicative_arg -> Vec n applicative_arg #

cosh :: Vec n applicative_arg -> Vec n applicative_arg #

tanh :: Vec n applicative_arg -> Vec n applicative_arg #

asinh :: Vec n applicative_arg -> Vec n applicative_arg #

acosh :: Vec n applicative_arg -> Vec n applicative_arg #

atanh :: Vec n applicative_arg -> Vec n applicative_arg #

log1p :: Vec n applicative_arg -> Vec n applicative_arg #

expm1 :: Vec n applicative_arg -> Vec n applicative_arg #

log1pexp :: Vec n applicative_arg -> Vec n applicative_arg #

log1mexp :: Vec n applicative_arg -> Vec n applicative_arg #

(IsNat n, Fractional applicative_arg) => Fractional (Vec n applicative_arg) # 

Methods

(/) :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

recip :: Vec n applicative_arg -> Vec n applicative_arg #

fromRational :: Rational -> Vec n applicative_arg #

(IsNat n, Integral applicative_arg) => Integral (Vec n applicative_arg) # 

Methods

quot :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

rem :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

div :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

mod :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

quotRem :: Vec n applicative_arg -> Vec n applicative_arg -> (Vec n applicative_arg, Vec n applicative_arg) #

divMod :: Vec n applicative_arg -> Vec n applicative_arg -> (Vec n applicative_arg, Vec n applicative_arg) #

toInteger :: Vec n applicative_arg -> Integer #

(IsNat n, Num applicative_arg) => Num (Vec n applicative_arg) # 

Methods

(+) :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

(-) :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

(*) :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

negate :: Vec n applicative_arg -> Vec n applicative_arg #

abs :: Vec n applicative_arg -> Vec n applicative_arg #

signum :: Vec n applicative_arg -> Vec n applicative_arg #

fromInteger :: Integer -> Vec n applicative_arg #

Ord a => Ord (Vec n a) Source # 

Methods

compare :: Vec n a -> Vec n a -> Ordering #

(<) :: Vec n a -> Vec n a -> Bool #

(<=) :: Vec n a -> Vec n a -> Bool #

(>) :: Vec n a -> Vec n a -> Bool #

(>=) :: Vec n a -> Vec n a -> Bool #

max :: Vec n a -> Vec n a -> Vec n a #

min :: Vec n a -> Vec n a -> Vec n a #

(IsNat n, Num applicative_arg, Ord applicative_arg) => Real (Vec n applicative_arg) # 

Methods

toRational :: Vec n applicative_arg -> Rational #

(IsNat n, RealFloat applicative_arg) => RealFloat (Vec n applicative_arg) # 

Methods

floatRadix :: Vec n applicative_arg -> Integer #

floatDigits :: Vec n applicative_arg -> Int #

floatRange :: Vec n applicative_arg -> (Int, Int) #

decodeFloat :: Vec n applicative_arg -> (Integer, Int) #

encodeFloat :: Integer -> Int -> Vec n applicative_arg #

exponent :: Vec n applicative_arg -> Int #

significand :: Vec n applicative_arg -> Vec n applicative_arg #

scaleFloat :: Int -> Vec n applicative_arg -> Vec n applicative_arg #

isNaN :: Vec n applicative_arg -> Bool #

isInfinite :: Vec n applicative_arg -> Bool #

isDenormalized :: Vec n applicative_arg -> Bool #

isNegativeZero :: Vec n applicative_arg -> Bool #

isIEEE :: Vec n applicative_arg -> Bool #

atan2 :: Vec n applicative_arg -> Vec n applicative_arg -> Vec n applicative_arg #

(IsNat n, RealFrac applicative_arg) => RealFrac (Vec n applicative_arg) # 

Methods

properFraction :: Integral b => Vec n applicative_arg -> (b, Vec n applicative_arg) #

truncate :: Integral b => Vec n applicative_arg -> b #

round :: Integral b => Vec n applicative_arg -> b #

ceiling :: Integral b => Vec n applicative_arg -> b #

floor :: Integral b => Vec n applicative_arg -> b #

Show a => Show (Vec n a) Source # 

Methods

showsPrec :: Int -> Vec n a -> ShowS #

show :: Vec n a -> String #

showList :: [Vec n a] -> ShowS #

(IsNat n, Monoid a) => Monoid (Vec n a) Source # 

Methods

mempty :: Vec n a #

mappend :: Vec n a -> Vec n a -> Vec n a #

mconcat :: [Vec n a] -> Vec n a #

(IsNat n, Storable a) => Storable (Vec n a) Source # 

Methods

sizeOf :: Vec n a -> Int #

alignment :: Vec n a -> Int #

peekElemOff :: Ptr (Vec n a) -> Int -> IO (Vec n a) #

pokeElemOff :: Ptr (Vec n a) -> Int -> Vec n a -> IO () #

peekByteOff :: Ptr b -> Int -> IO (Vec n a) #

pokeByteOff :: Ptr b -> Int -> Vec n a -> IO () #

peek :: Ptr (Vec n a) -> IO (Vec n a) #

poke :: Ptr (Vec n a) -> Vec n a -> IO () #

Newtype (Vec (S n) a) Source # 

Associated Types

type O (Vec (S n) a) :: * #

Methods

pack :: O (Vec (S n) a) -> Vec (S n) a #

unpack :: Vec (S n) a -> O (Vec (S n) a) #

Newtype (Vec Z a) Source # 

Associated Types

type O (Vec Z a) :: * #

Methods

pack :: O (Vec Z a) -> Vec Z a #

unpack :: Vec Z a -> O (Vec Z a) #

(IsNat n, Num a) => VectorSpace (Vec n a) Source # 

Associated Types

type Scalar (Vec n a) :: * #

Methods

(*^) :: Scalar (Vec n a) -> Vec n a -> Vec n a #

(IsNat n, Num a) => InnerSpace (Vec n a) Source # 

Methods

(<.>) :: Vec n a -> Vec n a -> Scalar (Vec n a) #

(IsNat n, Num a) => AdditiveGroup (Vec n a) Source # 

Methods

zeroV :: Vec n a #

(^+^) :: Vec n a -> Vec n a -> Vec n a #

negateV :: Vec n a -> Vec n a #

(^-^) :: Vec n a -> Vec n a -> Vec n a #

ToVec (Vec n a) n a Source # 

Methods

toVec :: Vec n a -> Vec n a Source #

type O (Vec (S n) a) Source # 
type O (Vec (S n) a) = (a, Vec n a)
type O (Vec Z a) Source # 
type O (Vec Z a) = ()
type Scalar (Vec n a) Source # 
type Scalar (Vec n a) = Vec1 a

unConsV :: Vec (S n) a -> (a, Vec n a) Source #

Type-safe un-cons for vectors

headV :: Vec (S n) a -> a Source #

Type-safe head for vectors

tailV :: Vec (S n) a -> Vec n a Source #

Type-safe tail for vectors

joinV :: Vec n (Vec n a) -> Vec n a Source #

Equivalent to monad join for vectors

(<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) a infixl 1 Source #

Concatenation of vectors

indices :: IsNat n => Vec n (Index n) Source #

Indices under n: index0 :< index1 :< ...

iota :: (IsNat n, Num a) => Vec n a Source #

Vector of ints from 0 to n-1. Named for APL iota operation (but 0 based).

type Vec0 = Vec N0 Source #

type Vec1 = Vec N1 Source #

type Vec2 = Vec N2 Source #

type Vec3 = Vec N3 Source #

type Vec4 = Vec N4 Source #

type Vec5 = Vec N5 Source #

type Vec6 = Vec N6 Source #

type Vec7 = Vec N7 Source #

type Vec8 = Vec N8 Source #

type Vec9 = Vec N9 Source #

vec1 :: a -> Vec1 a Source #

vec2 :: a -> a -> Vec2 a Source #

vec3 :: a -> a -> a -> Vec3 a Source #

vec4 :: a -> a -> a -> a -> Vec4 a Source #

vec5 :: a -> a -> a -> a -> a -> Vec5 a Source #

vec6 :: a -> a -> a -> a -> a -> a -> Vec6 a Source #

vec7 :: a -> a -> a -> a -> a -> a -> a -> Vec7 a Source #

vec8 :: a -> a -> a -> a -> a -> a -> a -> a -> Vec8 a Source #

un1 :: Vec1 a -> a Source #

Extract element

un2 :: Vec2 a -> (a, a) Source #

Extract elements

un3 :: Vec3 a -> (a, a, a) Source #

Extract elements

un4 :: Vec4 a -> (a, a, a, a) Source #

Extract elements

get :: Index n -> Vec n a -> a Source #

Extract a vector element, taking a proof that the index is within bounds.

get0 Source #

Arguments

:: Vec (N1 :+: n) a 
-> a

Get first element

get1 Source #

Arguments

:: Vec (N2 :+: n) a 
-> a

Get second element

get2 Source #

Arguments

:: Vec (N3 :+: n) a 
-> a

Get third element

get3 Source #

Arguments

:: Vec (N4 :+: n) a 
-> a

Get fourth element

update :: Index n -> (a -> a) -> Vec n a -> Vec n a Source #

Update a vector element, taking a proof that the index is within bounds.

set :: Index n -> a -> Vec n a -> Vec n a Source #

Replace a vector element, taking a proof that the index is within bounds.

set0 Source #

Arguments

:: a 
-> Vec (N1 :+: n) a 
-> Vec (N1 :+: n) a

Set first element

set1 Source #

Arguments

:: a 
-> Vec (N2 :+: n) a 
-> Vec (N2 :+: n) a

Set second element

set2 Source #

Arguments

:: a 
-> Vec (N3 :+: n) a 
-> Vec (N3 :+: n) a

Set third element

set3 Source #

Arguments

:: a 
-> Vec (N4 :+: n) a 
-> Vec (N4 :+: n) a

Set fourth element

getI :: (IsNat n, Show i, Integral i) => i -> Vec n a -> a Source #

Variant of get in which the index size is checked at run-time instead of compile-time.

setI :: (IsNat n, Show i, Integral i) => i -> a -> Vec n a -> Vec n a Source #

Variant of set in which the index size is checked at run-time instead of compile-time.

flattenV :: IsNat n => Vec n (Vec m a) -> Vec (n :*: m) a Source #

Flatten a vector of vectors (a 2D array) into a vector

chunkV :: (IsNat n, IsNat m) => Vec (n :*: m) a -> Vec n (Vec m a) Source #

Chunk a vector into a vector of vectors (a 2D array)

swizzle :: Vec n (Index m) -> Vec m a -> Vec n a Source #

Swizzling. Extract multiple elements simultaneously.

split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a) Source #

Split a vector

deleteV :: Eq a => a -> Vec (S n) a -> Vec n a Source #

Delete exactly one occurrence of an element from a vector, raising an error if the element isn't present.

elemsV :: IsNat n => [a] -> Vec n a Source #

Convert a list into a vector. Error if the list is too short or too long

zipV :: Vec n a -> Vec n b -> Vec n (a, b) Source #

Zip two vectors into one. Like liftA2 '(,)', but the former requires IsNat n.

zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

Unzip one vector into two. Like liftA2, but the former requires IsNat n.

unzipV :: Vec n (a, b) -> (Vec n a, Vec n b) Source #

Unzip a vector of pairs into a pair of vectors

zipV3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c) Source #

Zip three vectors into one. Like liftA3 '(,)', but the former requires IsNat n.

zipWithV3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d Source #

Unzip one vector into two. Like liftA2, but the former requires IsNat n.

unzipV3 :: Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c) Source #

Unzip a vector of pairs into a pair of vectors

transpose :: IsNat n => Vec m (Vec n a) -> Vec n (Vec m a) Source #

Matrix transposition. Specialization of sequenceA.

cross :: Vec m a -> Vec n b -> Vec m (Vec n (a, b)) Source #

Cross-product of two vectors, in the set-theory sense, not the geometric sense. You can flattenV the resulting vector of vectors.

class ToVec c n a where Source #

Minimal complete definition

toVec

Methods

toVec :: c -> Vec n a Source #

Instances

IsNat n => ToVec [a] n a Source # 

Methods

toVec :: [a] -> Vec n a Source #

ToVec (Vec n a) n a Source # 

Methods

toVec :: Vec n a -> Vec n a Source #