Finished the second section of the guide

This commit is contained in:
Kiana Sheibani 2024-04-26 01:53:32 -04:00
parent 2318ee7660
commit 3b361caeb7
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
5 changed files with 108 additions and 14 deletions

View file

@ -28,7 +28,7 @@ combine the most useful features of each library.
## Documentation ## Documentation
Most of the exported utility functions have docstrings. There is also Most of the exported utility functions have docstrings. There is also
a (currently unfinished) tutorial of NumIdr's features [here](docs/Intro.md). a (currently unfinished) guide on how to use NumIdr [here](docs/Intro.md).
## Usage ## Usage

View file

@ -1,6 +1,6 @@
# Fundamental Data Types # Fundamental Data Types
NumIdr exports a number of different datatypes. The most important type to be aware of is the _array_, but there are other useful types as well. NumIdr exports a number of different datatypes. The most important type and the cornerstone of the library is the _array_, but there are other useful types as well.
## Arrays ## Arrays

View file

@ -1,6 +1,6 @@
# NumIdr Tutorial # NumIdr Guide
Welcome to NumIdr's tutorial! Welcome to NumIdr's guide!
If you're familiar with the Python library [NumPy](https://numpy.org/) or anything based on it, then a lot of the early content will be familiar, as NumIdr is based on the same array type. If you're familiar with the Python library [NumPy](https://numpy.org/) or anything based on it, then a lot of the early content will be familiar, as NumIdr is based on the same array type.

View file

@ -8,7 +8,7 @@ The most important array constructor is `array`, which returns an array of the s
array [[1, 2, 3], [4, 5, 6]] array [[1, 2, 3], [4, 5, 6]]
``` ```
Scalars, vectors and matrices have their own constructors, used in exactly the same way (`scalar`, `vector`, and `matrix`). These should be used instead of `array` whenever possible, as they provide more information to the type-checker. Scalars, vectors and matrices have their own constructors, used in exactly the same way (`scalar`, `vector`, and `matrix`). These should be used instead of `array` whereever possible, as they provide more information to the type-checker.
There are also a few other, more basic constructors for convenience. There are also a few other, more basic constructors for convenience.
@ -23,23 +23,36 @@ zeros [2, 2, 3]
ones [2, 2, 3] ones [2, 2, 3]
``` ```
## Accessing Array Properties
There are a few simple functions for accessing basic properties of arrays: `shape` and `rank`, which are self-explanatory, and `size`, which returns the total number of elements in the array.
The `shape` accessor is sufficient for most uses, but it can cause problems with the type-checker, as for an array `arr : Array s a` the type checker does not know that `shape arr` and `s` are equal. To solve this problem, a view for accessing the shape is provided:
```idris
example {s} arr with (viewShape arr)
_ | Shape s = ...
```
This will fully placate the type-checker, as the `s` returned by the view is proven to be equal to the shape of the array.
## Indexing Arrays ## Indexing Arrays
NumIdr provides multiple different indexing functions for different purposes. These functions can be grouped based on these categories: NumIdr provides multiple different indexing functions for different purposes. These functions can be grouped based on these categories:
**Operation** **Operation**
- Access - Accesses and returns elements from the array. - **Access** - Accesses and returns elements from the array.
- Update - Returns a new array with the specified element or range updated by a function. These are indicated by an `Update` suffix. - **Update** - Returns a new array with the specified element or range updated by a function. These are indicated by an `Update` suffix.
- Set - Returns a new array with the specified element or range set to new values. These are indicated by a `Set` suffix. - **Set** - Returns a new array with the specified element or range set to new values. These are indicated by a `Set` suffix.
**Range** **Range**
- Default - Operates on a single array element. - **Default** - Operates on a single array element.
- Range - Operates on multiple elements at once. These are indicated by a `Range` suffix. - **Range** - Operates on multiple elements at once. These are indicated by a `Range` suffix.
**Safety** **Safety**
- Safe - Guarantees through its type that the index is within range by requiring each index to be a `Fin` value. - **Safe** - Guarantees through its type that the index is within range by requiring each index to be a `Fin` value.
- Non-Bounded - Does not guarantee through its type that the index is within range, and returns `Nothing` if the provided index is out of bounds. These are indicated by an `NB` suffix. - **Non-Bounded** - Does not guarantee through its type that the index is within range, and returns `Nothing` if the provided index is out of bounds. These are indicated by an `NB` suffix.
- Unsafe - Does not perform any bounds checks at all. These are indicated by an `Unsafe` suffix. **Only use these if you really know what you are doing!** - **Unsafe** - Does not perform any bounds checks at all. These are indicated by an `Unsafe` suffix. **Only use these if you really know what you are doing!**
Not all combinations of these categories are defined by the library. Here are the currently provided indexing functions: Not all combinations of these categories are defined by the library. Here are the currently provided indexing functions:
@ -49,7 +62,7 @@ Not all combinations of these categories are defined by the library. Here are th
| **Update** | `indexUpdate` | `indexUpdateRange` | `indexUpdateNB` | | | | | **Update** | `indexUpdate` | `indexUpdateRange` | `indexUpdateNB` | | | |
| **Set** | `indexSet` | `indexSetRange` | `indexSetNB` | | | | | **Set** | `indexSet` | `indexSetRange` | `indexSetNB` | | | |
The accessor functions also have operator forms. The accessor functions have operator forms for convenience, also specified within the table.
### Specifying Coordinates ### Specifying Coordinates
@ -78,4 +91,80 @@ matrix [[2, 0], [1, 2]] !!.. [All, One 0]
== vector [2, 1] == vector [2, 1]
``` ```
## Standard Interface Methods
The array type implements a number of standard interfaces. Most of these implementations are unremarkable, but a few have caveats that are worth noting.
### Numeric Operations
Arrays implement the numeric interfaces (`Num`, `Neg`, `Fractional`), as well as `Semigroup` and `Monoid`, if their element type supports those operations. These functions are computed elementwise.
```idris
matrix [[1, 1], [2, 5]] + matrix [[2, 3], [-1, 3]]
== matrix [[3, 4], [1, 8]]
```
This elementwise behavior holds for `(+)`, `(*)`, `(-)`, `(/)`, and `(<+>)`. **`(*)` is not matrix multiplication!** For the generalized multiplication operator, which includes matrix multiplication, see [the next chapter](VectorsMatrices.md).
> [!NOTE]
> Due to unfortunate restrictions in Idris's standard `Num` interface, the addition and multiplication operations can only be used when the array's shape is available at run-time. If this is not the case, you must use `zipwith (+)` or `zipWith (*)` instead.
### `Foldable` and `Traversable`
When folding or traversing the elements of an array, these elements are ordered in row-major or "C-style" order, which corresponds to the order in which elements are written and displayed. This behavior should not be depended on, however, as it can change based on the internal [array representation](Representations.md); use the `elements` function if you specifically want row-major order.
## Other Common Operations
### Concatenation and Stacking
Two arrays can be concatenated along an axis, so long as all other axes have the same dimensions. Two matrices being concatenated along the row axis requires that they must have the same number of columns.
```idris
-- 0 is the first axis i.e. the row axis
concat 0 (matrix [[1, 2], [3, 4]]) (matrix [[5, 6], [7, 8]])
== matrix [[1, 2],
[3, 4],
[5, 6],
[7, 8]]
```
Stacking is similar to concatenation, but slightly different. Stacking combines arrays with the exact same shape into a single array that is one rank higher. For example, vectors can be stacked along the row axis to obtain a matrix whose rows are the original vectors.
```idris
stack 0 [vector [1, 2], vector [3, 4]]
== matrix [[1, 2],
[3, 4]]
```
There are also specialized functions for operating on vectors and matrices: `(++)` for concatenating vectors; `vconcat` and `hconcat` for concatenating two matrices vertically (by row) and horizontally (by column) respectively, and `vstack` and `hstack` for stacking row vectors and column vectors respectively.
### Reshaping and Resizing
An array can be "reshaped" into any other shape, so long as the total number of elements is the same. This reshaping is done by arranging the elements into a linear order before inserting them into the new array. As with folding, the default order is row-major.
```idris
reshape [3, 2] (vector [1, 2, 3, 4, 5, 6])
== matrix [[1, 2],
[3, 4],
[5, 6]]
```
Arrays can also be resized, which changes their shape while keeping every element at the same index. A default element must be provided to fill any indices that did not exist in the original array.
```idris
resize [2, 4] 10 (matrix [[1, 2],
[3, 4],
[5, 6]])
== matrix [[1, 2, 10, 10],
[3, 4, 10, 10]]
```
Instead of the `resize` function, one can also use the `resizeLTE` function, which does not require a default element, but only works if the new array would be provably smaller than the original one.
### Transpose
The `transpose` function reverses the axis order of an array. For matrices, this corresponds to the usual definition of switching rows and columns. There is also a postfix form `(.T)`.
For more fine-grained control when rearranging arrays, there are the `swapAxes` and `permuteAxes` functions, where the first swaps only two axes and the second takes an arbitrary [permutation](DataTypes.md#Permutations). There are also `swapInAxis` and `permuteInAxis`, which permute inside an axis, e.g. swapping rows or columns in a matrix.
[Previous](DataTypes.md) | [Contents](Intro.md) | [Next](VectorsMatrices.md) [Previous](DataTypes.md) | [Contents](Intro.md) | [Next](VectorsMatrices.md)

View file

@ -58,6 +58,11 @@ export
shape : Array {rk} s a -> Vect rk Nat shape : Array {rk} s a -> Vect rk Nat
shape (MkArray _ s _) = s shape (MkArray _ s _) = s
||| The size of the array, i.e. the total number of elements.
export
size : Array s a -> Nat
size = product . shape
||| The rank of the array. ||| The rank of the array.
export export
rank : Array s a -> Nat rank : Array s a -> Nat