Safe Haskell	None
Language	GHC2021

NumHask.Array.Shape

Description

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

Synopsis

newtype Shape (s :: [Nat]) = Shape {
- shapeVal :: [Int]
}
class HasShape (s :: [Nat]) where
- toShape :: Shape s
type family (a :: [k]) ++ (b :: [k]) :: [k] where ...
type family (a :: [k]) !! (b :: Nat) :: k where ...
type family Take (n :: Nat) (a :: [k]) :: [k] where ...
type family Drop (n :: Nat) (a :: [k]) :: [k] where ...
type Reverse (a :: [k]) = ReverseGo a ('[] :: [k])
type family ReverseGo (a :: [k]) (b :: [k]) :: [k] where ...
type family Filter (r :: [Nat]) (xs :: [Nat]) (i :: Nat) :: [Nat] where ...
rank :: [a] -> Int
type family Rank (s :: [a]) :: Nat where ...
ranks :: [[a]] -> [Int]
type family Ranks (s :: [[a]]) :: [Nat] where ...
size :: [Int] -> Int
type family Size (s :: [Nat]) :: Nat where ...
dimension :: [Int] -> Int -> Int
type family Dimension (s :: [Nat]) (i :: Nat) :: Nat where ...
flatten :: [Int] -> [Int] -> Int
shapen :: [Int] -> Int -> [Int]
minimum :: [Int] -> Int
type family Minimum (s :: [Nat]) :: Nat where ...
checkIndex :: Int -> Int -> Bool
type family CheckIndex (i :: Nat) (n :: Nat) :: Bool where ...
checkIndexes :: [Int] -> Int -> Bool
type family CheckIndexes (i :: [Nat]) (n :: Nat) :: Bool where ...
addIndex :: [Int] -> Int -> Int -> [Int]
type AddIndex (s :: [a]) (i :: Nat) (d :: a) = Take i s ++ (d ': Drop i s)
dropIndex :: [Int] -> Int -> [Int]
type DropIndex (s :: [k]) (i :: Nat) = Take i s ++ Drop (i + 1) s
posRelative :: [Int] -> [Int]
type family PosRelative (s :: [Nat]) :: [Nat] where ...
type family PosRelativeGo (r :: [Nat]) (s :: [Nat]) :: [Nat] where ...
type family DecMap (x :: Nat) (ys :: [Nat]) :: [Nat] where ...
addIndexes :: [Int] -> [Int] -> [Int] -> [Int]
type family AddIndexes (as :: [Nat]) (xs :: [Nat]) (ys :: [Nat]) :: [Nat] where ...
type family AddIndexesGo (as :: [Nat]) (xs :: [Nat]) (ys :: [Nat]) :: [Nat] where ...
dropIndexes :: [Int] -> [Int] -> [Int]
type family DropIndexes (s :: [Nat]) (i :: [Nat]) :: [Nat] where ...
type family DropIndexesGo (s :: [Nat]) (i :: [Nat]) :: [Nat] where ...
takeIndexes :: [Int] -> [Int] -> [Int]
type family TakeIndexes (s :: [Nat]) (i :: [Nat]) :: [Nat] where ...
exclude :: Int -> [Int] -> [Int]
type family Exclude (r :: Nat) (i :: [Nat]) :: [Nat] where ...
type family Enumerate (n :: Nat) :: [Natural] where ...
type family EnumerateGo (n :: Nat) :: [Natural] where ...
concatenate' :: Int -> [Int] -> [Int] -> [Int]
type Concatenate (i :: Nat) (s0 :: [Nat]) (s1 :: [Nat]) = Take i s0 ++ ((Dimension s0 i + Dimension s1 i) ': Drop (i + 1) s0)
type CheckConcatenate (i :: Nat) (s0 :: [a]) (s1 :: [a]) (s :: k) = (CheckIndex i (Rank s0) && ((DropIndex s0 i == DropIndex s1 i) && (Rank s0 == Rank s1))) ~ 'True
type Insert (d :: Nat) (s :: [Nat]) = Take d s ++ ((Dimension s d + 1) ': Drop (d + 1) s)
type CheckInsert (d :: Nat) (i :: Nat) (s :: [Nat]) = (CheckIndex d (Rank s) && CheckIndex i (Dimension s d)) ~ 'True
reorder' :: [Int] -> [Int] -> [Int]
type family Reorder (s :: [Nat]) (ds :: [Nat]) :: [Nat] where ...
type family CheckReorder (ds :: [Nat]) (s :: [Nat]) where ...
squeeze' :: (Eq a, Multiplicative a) => [a] -> [a]
type family Squeeze (a :: [Nat]) :: [Nat] where ...
incAt :: Int -> [Int] -> [Int]
decAt :: Int -> [Int] -> [Int]
class KnownNats (ns :: [Nat]) where
- natVals :: Proxy ns -> [Int]
class KnownNatss (ns :: [[Nat]]) where
- natValss :: Proxy ns -> [[Int]]

Documentation

newtype Shape (s :: [Nat]) Source #

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

Instances details

Show (Shape s) Source #
Instance details Defined in NumHask.Array.Shape Methods showsPrec :: Int -> Shape s -> ShowS # show :: Shape s -> String # showList :: [Shape s] -> ShowS #

class HasShape (s :: [Nat]) where Source #

Methods

toShape :: Shape s Source #

Instances

Instances details

HasShape ('[] :: [Nat]) Source #
Instance details Defined in NumHask.Array.Shape Methods toShape :: Shape ('[] :: [Nat]) Source #
(KnownNat n, HasShape s) => HasShape (n ': s) Source #
Instance details Defined in NumHask.Array.Shape Methods toShape :: Shape (n ': s) Source #

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

Equations

('[] :: [k]) ++ (b :: [k]) = b
(a ': as :: [k]) ++ (b :: [k]) = a ': (as ++ b)

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

Equations

('[] :: [k]) !! _1 = TypeError ('Text "Index Underflow") :: k
(x ': _1 :: [k]) !! 0 = x
(_1 ': xs :: [k]) !! i = xs !! (i - 1)

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

Equations

Take 0 (_1 :: [k]) = '[] :: [k]
Take n (x ': xs :: [k]) = x ': Take (n - 1) xs

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

Equations

Drop 0 (xs :: [k]) = xs
Drop n (_1 ': xs :: [k]) = Drop (n - 1) xs

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

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

Equations

ReverseGo ('[] :: [k]) (b :: [k]) = b
ReverseGo (a2 ': as :: [a1]) (b :: [a1]) = ReverseGo as (a2 ': b)

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

Equations

Filter r ('[] :: [Nat]) _1 = Reverse r
Filter r (x ': xs) i = Filter (If (x == i) r (x ': r)) xs i

rank :: [a] -> Int Source #

Number of dimensions

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

Equations

Rank ('[] :: [a]) = 0
Rank (_1 ': s :: [a]) = Rank s + 1

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

The shape of a list of element indexes

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

Equations

Ranks ('[] :: [[a]]) = '[] :: [Nat]
Ranks (x ': xs :: [[a]]) = Rank x ': Ranks xs

size :: [Int] -> Int Source #

Number of elements

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

Equations

Size ('[] :: [Nat]) = 1
Size (n ': s) = n * Size s

dimension :: [Int] -> Int -> Int Source #

dimension i is the i'th dimension of a Shape

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

Equations

Dimension (s ': _1) 0 = s
Dimension (_1 ': s) n = Dimension s (n - 1)
Dimension _1 _2 = TypeError ('Text "dimension overflow") :: Nat

flatten :: [Int] -> [Int] -> Int Source #

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

convert from a flat index to a shape index

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

minimum :: [Int] -> Int Source #

minimum value in a list

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

Equations

Minimum ('[] :: [Nat]) = TypeError ('Text "zero dimension") :: Nat
Minimum '[x] = x
Minimum (x ': xs) = If (x <=? Minimum xs) x (Minimum xs)

checkIndex :: Int -> Int -> Bool Source #

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 ... Source #

Equations

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

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

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

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

Equations

CheckIndexes ('[] :: [Nat]) _1 = 'True
CheckIndexes (i ': is) n = CheckIndex i n && CheckIndexes is n

addIndex :: [Int] -> Int -> Int -> [Int] Source #

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 :: [a]) (i :: Nat) (d :: a) = Take i s ++ (d ': Drop i s) Source #

dropIndex :: [Int] -> Int -> [Int] Source #

drop the i'th dimension from a shape

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

type DropIndex (s :: [k]) (i :: Nat) = Take i s ++ Drop (i + 1) s Source #

posRelative :: [Int] -> [Int] Source #

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]) :: [Nat] where ... Source #

Equations

PosRelative s = PosRelativeGo s ('[] :: [Nat])

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

Equations

PosRelativeGo ('[] :: [Nat]) r = Reverse r
PosRelativeGo (x ': xs) r = PosRelativeGo (DecMap x xs) (x ': r)

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

Equations

DecMap _1 ('[] :: [Nat]) = '[] :: [Nat]
DecMap x (y ': ys) = If ((y + 1) <=? x) y (y - 1) ': DecMap x ys

addIndexes :: [Int] -> [Int] -> [Int] -> [Int] Source #

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]) :: [Nat] where ... Source #

Equations

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

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

Equations

AddIndexesGo as' ('[] :: [Nat]) _1 = as'
AddIndexesGo as' (x ': xs') (y ': ys') = AddIndexesGo (AddIndex as' x y) xs' ys'
AddIndexesGo _1 _2 _3 = TypeError ('Text "mismatched ranks") :: [Nat]

dropIndexes :: [Int] -> [Int] -> [Int] Source #

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]) :: [Nat] where ... Source #

Equations

DropIndexes s i = DropIndexesGo s (PosRelative i)

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

Equations

DropIndexesGo s ('[] :: [Nat]) = s
DropIndexesGo s (i ': is) = DropIndexesGo (DropIndex s i) is

takeIndexes :: [Int] -> [Int] -> [Int] Source #

take list of dimensions according to position lists.

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

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

Equations

TakeIndexes ('[] :: [Nat]) _1 = '[] :: [Nat]
TakeIndexes _1 ('[] :: [Nat]) = '[] :: [Nat]
TakeIndexes s (i ': is) = (s !! i) ': TakeIndexes s is

exclude :: Int -> [Int] -> [Int] Source #

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]) :: [Nat] where ... Source #

Equations

Exclude r i = DropIndexes (EnumerateGo r) i

type family Enumerate (n :: Nat) :: [Natural] where ... Source #

Equations

Enumerate n = Reverse (EnumerateGo n)

type family EnumerateGo (n :: Nat) :: [Natural] where ... Source #

Equations

EnumerateGo 0 = '[] :: [Natural]
EnumerateGo n = (n - 1) ': EnumerateGo (n - 1)

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

concatenate

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

type Concatenate (i :: Nat) (s0 :: [Nat]) (s1 :: [Nat]) = Take i s0 ++ ((Dimension s0 i + Dimension s1 i) ': Drop (i + 1) s0) Source #

type CheckConcatenate (i :: Nat) (s0 :: [a]) (s1 :: [a]) (s :: k) = (CheckIndex i (Rank s0) && ((DropIndex s0 i == DropIndex s1 i) && (Rank s0 == Rank s1))) ~ 'True Source #

type Insert (d :: Nat) (s :: [Nat]) = Take d s ++ ((Dimension s d + 1) ': Drop (d + 1) s) Source #

type CheckInsert (d :: Nat) (i :: Nat) (s :: [Nat]) = (CheckIndex d (Rank s) && CheckIndex i (Dimension s d)) ~ 'True Source #

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

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 ... Source #

Equations

Reorder ('[] :: [Nat]) _1 = '[] :: [Nat]
Reorder _1 ('[] :: [Nat]) = '[] :: [Nat]
Reorder s (d ': ds) = Dimension s d ': Reorder s ds

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

Equations

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

squeeze' :: (Eq a, Multiplicative a) => [a] -> [a] Source #

remove 1's from a list

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

Equations

Squeeze ('[] :: [Nat]) = '[] :: [Nat]
Squeeze a = Filter ('[] :: [Nat]) a 1

incAt :: Int -> [Int] -> [Int] Source #

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

decAt :: Int -> [Int] -> [Int] Source #

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

class KnownNats (ns :: [Nat]) where Source #

Reflect a list of Nats

Methods

natVals :: Proxy ns -> [Int] Source #

Instances

Instances details

KnownNats ('[] :: [Nat]) Source #
Instance details Defined in NumHask.Array.Shape Methods natVals :: Proxy ('[] :: [Nat]) -> [Int] Source #
(KnownNat n, KnownNats ns) => KnownNats (n ': ns) Source #
Instance details Defined in NumHask.Array.Shape Methods natVals :: Proxy (n ': ns) -> [Int] Source #

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

Reflect a list of list of Nats

Methods

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

Instances

Instances details

KnownNatss ('[] :: [[Nat]]) Source #
Instance details Defined in NumHask.Array.Shape Methods natValss :: Proxy ('[] :: [[Nat]]) -> [[Int]] Source #
(KnownNats n, KnownNatss ns) => KnownNatss (n ': ns) Source #
Instance details Defined in NumHask.Array.Shape Methods natValss :: Proxy (n ': ns) -> [[Int]] Source #