Email Gateway (Aug 18 2022 at 19:28): Email Gateway (Aug 18 2022 at 19:28):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Is there currently a theory for multi-dimensional arrays? I have found
something called the Collections framework, but I do not know if this
fits the bill. I am looking to create a theory based on the Mathematics
of Arrays, but if there was already a base for arrays, I would take that
as a starting point.
Email Gateway (Aug 18 2022 at 19:43):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
On Tue, 01 May 2012 08:06:24 +0200, Tobias Nipkow wrote:
The simplest way to model an array
is as a function nat => 'a.
[...]
If you want all arrays in the same type you could use nat list => 'a.
Indeed, this looks like it will do what I want admirably well. Thank you.
Email Gateway (Aug 18 2022 at 20:01):From: Tobias Nipkow <nipkow@in.tum.de>
It depends on what you exactly want. The simplest way to model an array is as a
function nat => 'a. A 2-dim array would have type nat => nat => 'a. If you
want all arrays in the same type you could use nat list => 'a. Of course these
models do not express that arrays have a fixed length. If you model arrays as
lists, that feature is captured as well. But arrays of different dimensions will
have different types, which may or may not bother you. This is the model in the
arrays of the collections framework, except that they wrap it up in a separate type.
Tobias
Last updated: Apr 19 2024 at 16:20 UTC