A value-level witness for a type-level natural number. This is commonly referred to as a singleton type, as for each n, there is a single value that inhabits the type SNat n (aside from bottom).

The definition of SNat is intentionally left abstract. To obtain an SNat value, use one of the following:

1. The natSing method of KnownNat.
2. The SNat pattern synonym.
3. The withSomeSNat function, which creates an SNat from a Natural number.

Since: base-4.18.0.0

A explicitly bidirectional pattern synonym relating an SNat to a KnownNat constraint.

As an expression: Constructs an explicit SNat n value from an implicit KnownNat n constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNat n value bringing an implicit KnownNat n constraint into scope:

f :: SNat n -> ..
f SNat = {- SNat n in scope -}

Since: base-4.18.0.0

Get the value of a type level Nat. Use with explicit type application

>>> valueOf @42
42

A value-level witness for a type-level list of natural numbers.

Obtain an SNats value using:

• The natsSing method of KnownNats
• The SNats pattern
• The withSomeSNats function

>>> :t SNats @[2,3,4]
SNats @[2,3,4] :: KnownNats [2, 3, 4] => SNats [2, 3, 4]
>>> SNats @[2,3,4]
SNats @[2, 3, 4]

A explicitly bidirectional pattern synonym relating an SNats to a KnownNats constraint.

As an expression: Constructs an explicit SNats ns value from an implicit KnownNats ns constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNats n value bringing an implicit KnownNats n constraint into scope:

f :: SNats ns -> ..
f SNat = {- KnownNats ns in scope -}

or, if you need to both bring the KnownNats into scope and reuse the SNats input:

f (SNats :: SNats s) = g (SNats @s)

Return the value-level list of naturals in an SNats ns value.

>>> fromSNats (SNats @[2,3,4])
[2,3,4]

Reflect a list of naturals.

>>> natsSing @'[2]
SNats @'[2]

Obtain a value-level list of naturals from a type-level proxy

>>> natVals (SNats @[2,3,4])
[2,3,4]

Convert an explicit SNats ns value into an implicit KnownNats ns constraint.

An unknown type-level list of naturals.

Promote a list of naturals to unknown type-level

Convert a list of naturals into an SNats ns value, where ns is a fresh type-level list of naturals.

The value of a KnownNats.

>>> valuesOf @[2,3,4]
[2,3,4]

The rank (or length) of a KnownNats.

>>> rankOf @[2,3,4]
3

The size (or product) of a KnownNats.

>>> sizeOf @[2,3,4]
24

Fin most often represents a (finite) zero-based index for a single dimension (of a multi-dimensioned hyper-rectangular array).

Construct a Fin.

Errors on out-of-bounds

>>> fin @2 1
1

>>> fin @2 2
*** Exception: value outside bounds
...

Construct a Fin safely.

>>> safeFin 1 :: Maybe (Fin 2)
Just 1

>>> safeFin 2 :: Maybe (Fin 2)
Nothing

Fins most often represents (finite) indexes for multiple dimensions (of a multi-dimensioned hyper-rectangular array).

Construct a Fins.

Errors on out-of-bounds

>>> fins @[2,3,4] [1,2,3]
[1,2,3]

>>> fins @[2,3,4] [1,2,5]
*** Exception: value outside bounds
...

Construct a Fins safely.

>>> safeFins [1,2,3] :: Maybe (Fins [2,3,4])
Just [1,2,3]

>>> safeFins [2] :: Maybe (Fins '[2])
Nothing

Number of dimensions

>>> rank @Int [2,3,4]
3

Number of dimensions

>>> :k! Eval (Rank [2,3,4])
...
= 3

Enumerate a range of rank n

>>> range 0
[]

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

Enumerate a range of rank n

>>> :k! Eval (Range 0)
...
= '[]

>>> :k! Eval (Range 3)
...
= [0, 1, 2]

Create a new rank by adding ones to the left, if the new rank is greater, or combining dimensions (from left to right) into rows, if the new rank is lower.

>>> rerank 4 [2,3,4]
[1,2,3,4]
>>> rerank 2 [2,3,4]
[6,4]

Create a new rank by adding ones to the left, if the new rank is greater, or combining dimensions (from left to right) into rows, if the new rank is lower.

>>> :k! Eval (Rerank 4 [2,3,4])
...
= [1, 2, 3, 4]
>>> :k! Eval (Rerank 2 [2,3,4])
...
= [6, 4]

Enumerate the dimensions of a shape.

dimsOf [2,3,4] [0,1,2]

Enumerate the dimensions of a shape.

>>> :k! Eval (DimsOf [2,3,4])
...
= [0, 1, 2]

Enumerate the final dimensions of a shape.

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

Enumerate the final dimensions of a shape.

>>> :k! Eval (EndDimsOf [1,0] [2,3,4])
...
= [2, 1]

Total number of elements (if the list is the shape of a hyper-rectangular array).

>>> size [2,3,4]
24

Total number of elements (if the list is the shape of a hyper-rectangular array).

>>> :k! (Eval (Size [2,3,4]))
...
= 24

Convert from a n-dimensional shape list index to a flat index, which, technically is the lexicographic position of the position in a row-major array.

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

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

Convert from a flat index to a shape index.

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

Convert a scalar to a dimensioned shape

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

Convert a scalar to a dimensioned shape >>> :k! Eval (AsSingleton '[]) ... = '[1] >>> :k! Eval (AsSingleton [2,3,4]) ... = [2, 3, 4]

Convert a (potentially) [1] dimensioned shape to a scalar shape

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

Convert a (potentially) [1] dimensioned shape to a scalar shape >>> :k! Eval (AsScalar '[1]) ... = '[] >>> :k! Eval (AsScalar [2,3,4]) ... = [2, 3, 4]

Check if a shape is a subset (<=) another shape after reranking.

>>> isSubset [2,3,4] [2,3,4]
True

>>> isSubset [1,2] [2,3,4]
True

>>> isSubset [2,1] [1]
False

Check if a shape is a subset (<=) another shape after reranking.

>>> :k! Eval (IsSubset [2,3,4] [2,3,4])
...
= True

>>> :k! Eval (IsSubset [1,2] [2,3,4])
...
= True

>>> :k! Eval (IsSubset [2,1] '[1])
...
= False

Compute dimensions for a shape other than the supplied dimensions.

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

Compute dimensions for a shape other than the supplied dimensions.

>>> :k! Eval (ExceptDims [1,2] [2,3,4])
...
= '[0]

Reorder the dimensions of shape according to a list of positions.

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

Reorder the dimensions of shape according to a list of positions.

>>> :k! Eval (Reorder [2,3,4] [2,0,1])
...
= [4, 2, 3]

Test if a Reorder is valid.

>>> :k! Eval (ReorderOk [2,3,4] [0,1])
...
= False

remove 1's from a list

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

Remove 1's from a list.

>>> :k! (Eval (Squeeze [0,1,2,3]))
...
= [0, 2, 3]

Minimum of two type values.

>>> :k! Eval (Min 0 1)
...
= 0

Maximum of two type values.

>>> :k! Eval (Max 0 1)
...
= 1

minimum of a list

>>> S.minimum []
*** Exception: zero-ranked
...
>>> S.minimum [2,3,4]
2

minimum of a list

>>> :k! Eval (Minimum '[])
...
= (TypeError ...)

>>> :k! Eval (Minimum [2,3,4])
...
= 2

Check if i is a valid Fin (aka in-bounds index of a dimension)

>>> isFin 0 2
True
>>> isFin 2 2
False

Check if i is a valid Fin (aka in-bounds index of a dimension)

>>> :k! Eval (IsFin 0 2)
...
= True
>>> :k! Eval (IsFin 2 2)
...
= False

Check if i is a valid Fins (aka in-bounds index of a Shape)

>>> isFins [0,1] [2,2]
True
>>> isFins [0,1] [2,1]
False

Check if i is a valid Fins (aka in-bounds index of a Shape)

>>> :k! Eval (IsFins [0,1] [2,2])
...
= True
>>> :k! Eval (IsFins [0,1] [2,1])
...
= False

Is a value a valid dimension of a shape.

>>> isDim 2 [2,3,4]
True
>>> isDim 0 []
True

Is a value a valid dimension of a shape.

>>> :k! Eval (IsDim 2 [2,3,4])
...
= True
>>> :k! Eval (IsDim 0 '[])
...
= True

Are values valid dimensions of a shape.

>>> isDims [2,1] [2,3,4]
True
>>> isDims [0] []
True

Are values valid dimensions of a shape.

>>> :k! Eval (IsDims [2,1] [2,3,4])
...
= True
>>> :k! Eval (IsDims '[0] '[])
...
= True

Get the last position of a dimension of a shape.

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

Get the last position of a dimension of a shape.

>>> :k! Eval (LastPos 2 [2,3,4])
...
= 3
>>> :k! Eval (LastPos 0 '[])
...
= 0

Get the minimum dimension as a singleton dimension.

>>> minDim [2,3,4]
[2]
>>> minDim []
[]

Get the minimum dimension as a singleton dimension.

>>> :k! Eval (MinDim [2,3,4])
...
= '[2]
>>> :k! Eval (MinDim '[])
...
= '[]

Enumerate between two Nats

>>> :k! Eval (EnumFromTo 0 3)
...
= [0, 1, 2, 3]

Left fold.

>>> :k! Eval (Foldl' (Fcf.+) 0 [1,2,3])
...
= 6

Get an element at a given index.

>>> :kind! Eval (GetIndex 2 [2,3,4])
...
= Just 4

Modify an element at a given index.

The list is unchanged if the index is out of bounds.

Example

>>> :kind! Eval (SetIndex 2 7 [1,2,3])
Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
= [1, 2, 7]

Get the dimension of a shape at the supplied index. Error if out-of-bounds.

>>> getDim 1 [2,3,4]
3
>>> getDim 3 [2,3,4]
*** Exception: getDim outside bounds
...
>>> getDim 0 []
1

Get the dimension of a shape at the supplied index. Error if out-of-bounds or non-computable (usually unknown to the compiler).

>>> :k! Eval (GetDim 1 [2,3,4])
...
= 3
>>> :k! Eval (GetDim 3 [2,3,4])
...
= (TypeError ...)
>>> :k! Eval (GetDim 0 '[])
...
= 1

modify an index at a specific dimension. Errors if out of bounds.

>>> modifyDim 0 (+1) [0,1,2]
[1,1,2]
>>> modifyDim 0 (+1) []
[2]

modify an index at a specific dimension. Errors if out of bounds.

>>> :k! Eval (ModifyDim 0 ((Fcf.+) 1) [0,1,2])
...
= [1, 1, 2]

Increment the index at a dimension of a shape by 1. Scalars turn into singletons.

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

Increment the index at a dimension of a shape by 1. Scalars turn into singletons.

>>> :k! Eval (IncAt 1 [2,3,4])
...
= [2, 4, 4]
>>> :k! Eval (IncAt 0 '[])
...
= '[2]

Decrement the index at a dimension os a shape by 1.

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

Decrement the index at a dimension of a shape by 1.

>>> :k! Eval (DecAt 1 [2,3,4])
...
= [2, 2, 4]

replace an index at a specific dimension, or transform a scalar into being 1-dimensional.

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

replace an index at a specific dimension.

>>> :k! Eval (SetDim 0 1 [2,3,4])
...
= [1, 3, 4]

Take along a dimension.

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

Take along a dimension.

>>> :k! Eval (TakeDim 0 1 [2,3,4])
...
= [1, 3, 4]

Drop along a dimension.

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

Drop along a dimension.

>>> :k! Eval (DropDim 2 1 [2,3,4])
...
= [2, 3, 3]

delete the i'th dimension. No effect on a scalar.

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

delete the i'th dimension

>>> :k! Eval (DeleteDim 1 [2, 3, 4])
...
= [2, 4]
>>> :k! Eval (DeleteDim 1 '[])
...
= '[]

Insert a new dimension at a position (or at the end if > rank).

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

Insert a new dimension at a position (or at the end if > rank).

>>> :k! Eval (InsertDim 1 3 [2,4])
...
= [2, 3, 4]
>>> :k! Eval (InsertDim 0 4 '[])
...
= '[4]

Is a slice ok constraint.

>>> :k! Eval (InsertOk 2 [2,3,4] [2,3])
...
= True
>>> :k! Eval (InsertOk 0 '[] '[])
...
= True

Is a slice ok?

>>> :k! Eval (SliceOk 1 1 2 [2,3,4])
...
= True

Are slices ok?

>>> :k! Eval (SlicesOk '[1] '[1] '[2] [2,3,4])
...
= True

concatenate two arrays at dimension i

Bespoke logic for scalars.

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

concatenate two arrays at dimension i

Bespoke logic for scalars.

>>> :k! Eval (Concatenate 1 [2,3,4] [2,3,4])
...
= [2, 6, 4]
>>> :k! Eval (Concatenate 0 '[3] '[])
...
= '[4]
>>> :k! Eval (Concatenate 0 '[] '[3])
...
= '[4]
>>> :k! Eval (Concatenate 0 '[] '[])
...
= '[2]

Concatenate is Ok if ranks are the same and the non-indexed portion of the shapes are the same.

Get dimensions of a shape.

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

Get dimensions of a shape.

>>> :k! Eval (GetDims [2,0] [2,3,4])
...
= [4, 2]
>>> :k! Eval (GetDims '[2] '[])
...
= '[(TypeError ...)]

Get the index of the last position in the selected dimensions of a shape. Errors on a 0-dimension.

>>> getLastPositions [2,0] [2,3,4]
[3,1]
>>> getLastPositions [0] [0]
[-1]

Get the index of the last position in the selected dimensions of a shape. Errors on a 0-dimension.

>>> :k! Eval (GetLastPositions [2,0] [2,3,4])
...
= [3, 1]

modify dimensions of a shape with (separate) functions.

>>> modifyDims [0,1] [(+1), (+5)] [2,3,4]
[3,8,4]

Insert a list of dimensions according to dimensions and positions. Note that the list of positions references the final shape and not the initial shape.

>>> insertDims [0] [5] []
[5]
>>> insertDims [1,0] [3,2] [4]
[2,3,4]

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

>>> :k! Eval (InsertDims '[0] '[5] '[])
...
= '[5]
>>> :k! Eval (InsertDims [1,0] [3,2] '[4])
...
= [2, 3, 4]

Convert a list of positions that reference deletions according to a final shape to 1 that references deletions relative to an initial shape.

To delete the positions [1,2,5] from a list, for example, you need to delete position 1, (arriving at a 4 element list), then position 1, arriving at a 3 element list, and finally position 3.

>>> preDeletePositions [1,2,5]
[1,1,3]

>>> preDeletePositions [1,2,0]
[1,1,0]

Convert a list of positions that reference deletions according to a final shape to 1 that references deletions relative to an initial shape.

To delete the positions [1,2,5] from a list, for example, you need to delete position 1, (arriving at a 4 element list), then position 1, arriving at a 3 element list, and finally position 3.

>>> :k! Eval (PreDeletePositions [1,2,5])
...
= [1, 1, 3]

>>> :k! Eval (PreDeletePositions [1,2,0])
...
= [1, 1, 0]

Convert a list of position that reference insertions according to a final shape to 1 that references list insertions relative to an initial shape.

To insert into positions [1,2,0] from a list, starting from a 2 element list, for example, you need to insert at position 0, (arriving at a 3 element list), then position 1, arriving at a 4 element list, and finally position 0.

 preInsertPositions == reverse . preDeletePositions . reverse
>> preInsertPositions [1,2,5]

1,2,5

>>> preInsertPositions [1,2,0]
[0,1,0]

Convert a list of position that reference insertions according to a final shape to 1 that references list insertions relative to an initial shape.

To insert into positions [1,2,0] from a list, starting from a 2 element list, for example, you need to insert at position 0, (arriving at a 3 element list), then position 1, arriving at a 4 element list, and finally position 0.

 preInsertPositions == reverse . preDeletePositions . reverse
>> :k! Eval (PreInsertPositions [1,2,5])

... = [1, 2, 5]

>>> :k! Eval (PreInsertPositions [1,2,0])
...
= [0, 1, 0]

Set dimensions of a shape.

>>> setDims [0,1] [1,5] [2,3,4]
[1,5,4]

>>> setDims [0] [3] []
[3]

Set dimensions of a shape.

>>> :k! Eval (SetDims [0,1] [1,5] [2,3,4])
...
= [1, 5, 4]

>>> :k! Eval (SetDims '[0] '[3] '[])
...
= '[3]

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

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

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

>>> :k! Eval (DeleteDims [1,0] [2, 3, 4])
...
= '[4]

Drop a number of elements of a shape along the supplied dimensions.

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

Drop a number of elements of a shape along the supplied dimensions.

>>> :k! Eval (DropDims [0,2] [1,3] [2,3,4])
...
= [1, 3, 1]

Concatenate and replace dimensions, creating a new dimension at the supplied postion.

>>> concatDims [0,1] 1 [2,3,4]
[4,6]

Drop a number of elements of a shape along the supplied dimensions.

>>> :k! Eval (ConcatDims [0,1] 1 [2,3,4])
...
= [4, 6]

Unconcatenate and reinsert dimensions for an index.

>>> unconcatDimsIndex [0,1] 1 [4,6] [2,3]
[0,3,2]

reverse an index along specific dimensions.

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

rotate a list

>>> rotate 1 [0..3]
[1,2,3,0]
>>> rotate (-1) [0..3]
[3,0,1,2]

rotate an index along a specific dimension.

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

rotate an index along specific dimensions.

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

Test whether an index is a diagonal one.

>>> isDiag [2,2,2]
True
>>> isDiag [1,2]
False

Expanded shape of a windowed array

>>> expandWindows [2,2] [4,3,2]
[3,2,2,2,2]

Expanded shape of a windowed array

>>> :k! Eval (ExpandWindows [2,2] [4,3,2])
...
= [3, 2, 2, 2, 2]

Index into windows of an expanded windowed array, given a rank of the windows.

>>> indexWindows 2 [0,1,2,1,1]
[2,2,1]

Dimensions of a windowed array.

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

Dimensions of a windowed array.

>>> :k! Eval (DimWindows [2,2] [4,3,2])
...
= [0, 1, 2]

Expression evaluator.