NumHask.Array.Shape

Functions for manipulating shape. The module tends to supply equivalent functionality at type-level and value-level with functions of the same name (except for capitalization).

Documentation

newtype Shape (s :: [Nat])

The Shape type holds a [Nat] at type level and the equivalent [Int] at value level.

Constructors

Shape

Fields

• shapeVal :: [Int]

Instances

Show (Shape s)

Defined in NumHask.Array.Shape

Methods

showsPrec :: Int -> Shape s -> ShowS

show :: Shape s -> String

showList :: [Shape s] -> ShowS

class HasShape s where

Methods

toShape :: Shape s

Instances

HasShape ([] :: [Nat])

Defined in NumHask.Array.Shape

Methods

toShape :: Shape []

(KnownNat n, HasShape s) => HasShape (n ': s)

Defined in NumHask.Array.Shape

Methods

toShape :: Shape (n ': s)

rank :: [a] -> Int

Number of dimensions

type family Rank (s :: [a]) :: Nat where ...

Equations

Rank '[] = 0

Rank (_ ': s) = Rank s + 1

ranks :: [[a]] -> [Int]

The shape of a list of element indexes

type family Ranks (s :: [[a]]) :: [Nat] where ...

Equations

Ranks '[] = '[]

Ranks (x ': xs) = Rank x ': Ranks xs

size :: [Int] -> Int

Number of elements

type family Size (s :: [Nat]) :: Nat where ...

Equations

Size '[] = 1

Size (n ': s) = n * Size s

flatten :: [Int] -> [Int] -> Int

convert from n-dim shape index to a flat index

>>> flatten [2,3,4] [1,1,1]
17

>>> flatten [] [1,1,1]
0

shapen :: [Int] -> Int -> [Int]

convert from a flat index to a shape index

>>> shapen [2,3,4] 17
[1,1,1]

checkIndex :: Int -> Int -> Bool

checkIndex i n checks if i is a valid index of a list of length n

type family CheckIndex (i :: Nat) (n :: Nat) :: Bool where ...

Equations

CheckIndex i n = If ((0 <=? i) && ((i + 1) <=? n)) True (TypeError (Text "index outside range"))

checkIndexes :: [Int] -> Int -> Bool

checkIndexes is n check if is are valid indexes of a list of length n

type family CheckIndexes (i :: [Nat]) (n :: Nat) :: Bool where ...

Equations

CheckIndexes '[] n = True

CheckIndexes (i ': is) n = CheckIndex i n && CheckIndexes is n

dimension :: [Int] -> Int -> Int

dimension i is the i'th dimension of a Shape

type family Dimension (s :: [Nat]) (i :: Nat) :: Nat where ...

Equations

Dimension (s ': _) 0 = s

Dimension (_ ': s) n = Dimension s (n - 1)

Dimension _ _ = TypeError (Text "dimension overflow")

minimum :: [Int] -> Int

minimum value in a list

type family Minimum (s :: [Nat]) :: Nat where ...

Equations

Minimum '[] = TypeError (Text "zero dimension")

Minimum '[x] = x

Minimum (x ': xs) = If (x <=? Minimum xs) x (Minimum xs)

type family Take (n :: Nat) (a :: [k]) :: [k] where ...

Equations

Take 0 _ = '[]

Take n (x ': xs) = x ': Take (n - 1) xs

type family Drop (n :: Nat) (a :: [k]) :: [k] where ...

Equations

Drop 0 xs = xs

Drop n (_ ': xs) = Drop (n - 1) xs

type family Tail (a :: [k]) :: [k] where ...

Equations

Tail '[] = TypeError (Text "No tail")

Tail (_ ': xs) = xs

type family Init (a :: [k]) :: [k] where ...

Equations

Init '[] = TypeError (Text "No init")

Init '[_] = '[]

Init (x ': xs) = x ': Init xs

type family Head (a :: [k]) :: k where ...

Equations

Head '[] = TypeError (Text "No head")

Head (x ': _) = x

type family Last (a :: [k]) :: k where ...

Equations

Last '[] = TypeError (Text "No last")

Last '[x] = x

Last (_ ': xs) = Last xs

type family (a :: [k]) ++ (b :: [k]) :: [k] where ...

Equations

'[] ++ b = b

(a ': as) ++ b = a ': (as ++ b)

dropIndex :: [Int] -> Int -> [Int]

drop the i'th dimension from a shape

>>> dropIndex [2, 3, 4] 1
[2,4]

type DropIndex s i = Take i s ++ Drop (i + 1) s

addIndex :: [Int] -> Int -> Int -> [Int]

addIndex s i d adds a new dimension to shape s at position i

>>> addIndex [2,4] 1 3
[2,3,4]

type AddIndex s i d = Take i s ++ (d ': Drop i s)

type Reverse (a :: [k]) = ReverseGo a '[]

type family ReverseGo (a :: [k]) (b :: [k]) :: [k] where ...

Equations

ReverseGo '[] b = b

ReverseGo (a ': as) b = ReverseGo as (a ': b)

posRelative :: [Int] -> [Int]

convert a list of position that references a final shape to one that references positions relative to an accumulator. Deletions are from the left and additions are from the right.

deletions

>>> posRelative [0,1]
[0,0]

additions

>>> reverse (posRelative (reverse [1,0]))
[0,0]

type family PosRelative (s :: [Nat]) where ...

Equations

PosRelative s = PosRelativeGo s '[]

type family PosRelativeGo (r :: [Nat]) (s :: [Nat]) where ...

Equations

PosRelativeGo '[] r = Reverse r

PosRelativeGo (x ': xs) r = PosRelativeGo (DecMap x xs) (x ': r)

type family DecMap (x :: Nat) (ys :: [Nat]) :: [Nat] where ...

Equations

DecMap _ '[] = '[]

DecMap x (y ': ys) = If ((y + 1) <=? x) y (y - 1) ': DecMap x ys

dropIndexes :: [Int] -> [Int] -> [Int]

drop dimensions of a shape according to a list of positions (where position refers to the initial shape)

>>> dropIndexes [2, 3, 4] [1, 0]
[4]

type family DropIndexes (s :: [Nat]) (i :: [Nat]) where ...

Equations

DropIndexes s i = DropIndexesGo s (PosRelative i)

type family DropIndexesGo (s :: [Nat]) (i :: [Nat]) where ...

Equations

DropIndexesGo s '[] = s

DropIndexesGo s (i ': is) = DropIndexesGo (DropIndex s i) is

addIndexes :: [Int] -> [Int] -> [Int] -> [Int]

insert a list of dimensions according to position and dimension lists. Note that the list of positions references the final shape and not the initial shape.

>>> addIndexes [4] [1,0] [3,2]
[2,3,4]

type family AddIndexes (as :: [Nat]) (xs :: [Nat]) (ys :: [Nat]) where ...

Equations

AddIndexes as xs ys = AddIndexesGo as (Reverse (PosRelative (Reverse xs))) ys

type family AddIndexesGo (as :: [Nat]) (xs :: [Nat]) (ys :: [Nat]) where ...

Equations

AddIndexesGo as' '[] _ = as'

AddIndexesGo as' (x ': xs') (y ': ys') = AddIndexesGo (AddIndex as' x y) xs' ys'

AddIndexesGo _ _ _ = TypeError (Text "mismatched ranks")

takeIndexes :: [Int] -> [Int] -> [Int]

take list of dimensions according to position lists.

>>> takeIndexes [2,3,4] [2,0]
[4,2]

type family TakeIndexes (s :: [Nat]) (i :: [Nat]) where ...

Equations

TakeIndexes '[] _ = '[]

TakeIndexes _ '[] = '[]

TakeIndexes s (i ': is) = (s !! i) ': TakeIndexes s is

type family (a :: [k]) !! (b :: Nat) :: k where ...

Equations

'[] !! i = TypeError (Text "Index Underflow")

(x ': _) !! 0 = x

(_ ': xs) !! i = (!!) xs (i - 1)

type family Enumerate (n :: Nat) where ...

Equations

Enumerate n = Reverse (EnumerateGo n)

type family EnumerateGo (n :: Nat) where ...

Equations

EnumerateGo 0 = '[]

EnumerateGo n = (n - 1) ': EnumerateGo (n - 1)

exclude :: Int -> [Int] -> [Int]

turn a list of included positions for a given rank into a list of excluded positions

>>> exclude 3 [1,2]
[0]

type family Exclude (r :: Nat) (i :: [Nat]) where ...

Equations

Exclude r i = DropIndexes (EnumerateGo r) i

concatenate' :: Int -> [Int] -> [Int] -> [Int]

type Concatenate i s0 s1 = Take i s0 ++ ((Dimension s0 i + Dimension s1 i) ': Drop (i + 1) s0)

type CheckConcatenate i s0 s1 s = (CheckIndex i (Rank s0) && ((DropIndex s0 i == DropIndex s1 i) && (Rank s0 == Rank s1))) ~ True

type CheckInsert d i s = (CheckIndex d (Rank s) && CheckIndex i (Dimension s d)) ~ True

type Insert d s = Take d s ++ ((Dimension s d + 1) ': Drop (d + 1) s)

incAt :: Int -> [Int] -> [Int]

incAt d s increments the index at d of shape s by one.

decAt :: Int -> [Int] -> [Int]

decAt d s decrements the index at d of shape s by one.

reorder' :: [Int] -> [Int] -> [Int]

type family Reorder (s :: [Nat]) (ds :: [Nat]) :: [Nat] where ...

Equations

Reorder '[] _ = '[]

Reorder _ '[] = '[]

Reorder s (d ': ds) = Dimension s d ': Reorder s ds

type family CheckReorder (ds :: [Nat]) (s :: [Nat]) where ...

Equations

CheckReorder ds s = If ((Rank ds == Rank s) && CheckIndexes ds (Rank s)) True (TypeError (Text "bad dimensions")) ~ True

squeeze' :: (Eq a, Num a) => [a] -> [a]

type family Squeeze (a :: [Nat]) where ...

Equations

Squeeze '[] = '[]

Squeeze a = Filter '[] a 1

type family Filter (r :: [Nat]) (xs :: [Nat]) (i :: Nat) where ...

Equations

Filter r '[] _ = Reverse r

Filter r (x ': xs) i = Filter (If (x == i) r (x ': r)) xs i

type family Sort (xs :: [k]) :: [k] where ...

Equations

Sort '[] = '[]

Sort (x ': xs) = (Sort (SFilter FMin x xs) ++ '[x]) ++ Sort (SFilter FMax x xs)

data Flag

Constructors

FMin

FMax

type family Cmp (a :: k) (b :: k) :: Ordering

type family SFilter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where ...

Equations

SFilter f p '[] = '[]

SFilter FMin p (x ': xs) = If (Cmp x p == LT) (x ': SFilter FMin p xs) (SFilter FMin p xs)

SFilter FMax p (x ': xs) = If ((Cmp x p == GT) || (Cmp x p == EQ)) (x ': SFilter FMax p xs) (SFilter FMax p xs)

type family Zip lst lst' where ...

Equations

Zip lst lst' = ZipWith (,) lst lst'

type family ZipWith f lst lst' where ...

Equations

ZipWith f '[] lst = '[]

ZipWith f lst '[] = '[]

ZipWith f (l ': ls) (n ': ns) = f l n ': ZipWith f ls ns

type family Fst a where ...

Equations

Fst '(a, _) = a

type family Snd a where ...

Equations

Snd '(_, a) = a

type family FMap f lst where ...

Equations

FMap f '[] = '[]

FMap f (l ': ls) = f l ': FMap f ls

class KnownNats (ns :: [Nat]) where

Reflect a list of Nats

Methods

natVals :: Proxy ns -> [Int]

Instances

KnownNats ([] :: [Nat])

Defined in NumHask.Array.Shape

Methods

natVals :: Proxy [] -> [Int]

(KnownNat n, KnownNats ns) => KnownNats (n ': ns)

Defined in NumHask.Array.Shape

Methods

natVals :: Proxy (n ': ns) -> [Int]

class KnownNatss (ns :: [[Nat]]) where

Reflect a list of list of Nats

Methods

natValss :: Proxy ns -> [[Int]]

Instances

KnownNatss ([] :: [[Nat]])

Defined in NumHask.Array.Shape

Methods

natValss :: Proxy [] -> [[Int]]

(KnownNats n, KnownNatss ns) => KnownNatss (n ': ns)

Defined in NumHask.Array.Shape

Methods

natValss :: Proxy (n ': ns) -> [[Int]]