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. Using [Int] as the index for an array nicely represents the practical interests and constraints downstream of this high-level API: densely-packed numbers (reals or integrals), indexed and layered.

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)

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

Equations

'[] ++ b = b

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

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

Equations

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

(x ': _) !! 0 = x

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

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 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)

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

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

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")

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]

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)

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 '[] _ = 'True

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

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)

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

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

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")

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

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

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

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)

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

concatenate

>>> concatenate' 1 [2,3,4] [2,3,4]
[2,6,4]

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 Insert d s = Take d s ++ ((Dimension s d + 1) ': Drop (d + 1) s)

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

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

reorder' s i reorders the dimensions of shape s according to a list of positions i

>>> reorder' [2,3,4] [2,0,1]
[4,2,3]

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, Multiplicative a) => [a] -> [a]

remove 1's from a list

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

Equations

Squeeze '[] = '[]

Squeeze a = Filter '[] a 1

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.

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]]