0 | {--
 1 | Copyright (C) 2021  Joel Berkeley
 2 |
 3 | This program is free software: you can redistribute it and/or modify
 4 | it under the terms of the GNU Affero General Public License as published
 5 | by the Free Software Foundation, either version 3 of the License, or
 6 | (at your option) any later version.
 7 |
 8 | This program is distributed in the hope that it will be useful,
 9 | but WITHOUT ANY WARRANTY; without even the implied warranty of
10 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
11 | GNU Affero General Public License for more details.
12 |
13 | You should have received a copy of the GNU Affero General Public License
14 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
15 | --}
16 | ||| Common library types.
17 | module Types
18 |
19 | import public Data.Nat
20 | import public Data.Vect
21 |
22 | ||| Describes the shape of a `Tensor`. For example, a `Tensor` of `Double`s with contents
23 | ||| `[[0, 1, 2], [3, 4, 5]]` has two elements in its outer-most axis, and each of those elements
24 | ||| has three `Double`s in it, so this has shape [2, 3]. A `Tensor` can have axes of zero length,
25 | ||| though the shape cannot be unambiguously inferred by visualising it. For example, `[[], []]`
26 | ||| can have shape [2, 0], [2, 0, 5] or etc. A scalar `Tensor` has shape `[]`.
27 | public export 0
28 | Shape : Type
29 | Shape = List Nat
30 |
31 | ||| An `Array shape dtype` is either:
32 | ||| 
33 | ||| * a single value of type `dtype` (for `shape` `[]`), or
34 | ||| * an arbitrarily nested array of `Vect`s of such values (for any other `shape`)
35 | |||
36 | ||| @shape The shape of the array.
37 | ||| @dtype The type of elements of the array.
38 | public export 0
39 | Array : (0 shape : Shape) -> (0 dtype : Type) -> Type
40 | Array [] dtype = dtype
41 | Array (d :: ds) dtype = Vect d (Array ds dtype)
42 |