I am currently working in Agda on defining data types and implementing functions to operate on them. The purpose of this is to compile the code into JavaScript for verifying the logic of an application's state. One crucial requirement for this project is a data type that can be translated into a JavaScript array. Apart from filtering elements, I also need to determine the maximum value in the array.
On the Agda side, I aim to establish certain properties related to this data type (which will ultimately translate into a JavaScript array). Within the standard library, I am considering using Vec to represent a JavaScript array. Are there any other alternatives available, such as Vec.Bounded, that could serve this purpose effectively?
Initially, I attempted to utilize Data.List. However, due to a proof requiring retrieval of the last element, I decided to switch to Data.Vec to avoid working with Data.Maybe.
Subsequently, when I needed to perform some filtering operations, I discovered that Data.Vec.filter has the following signature:
filter : ∀ {n} → Vec A n → Vec≤ A n
Following the filtration process, it becomes necessary to convert the filtered Vec≤ back to a regular Vec.
At this stage, I started contemplating whether transitioning to Vec≤ might be advantageous to eliminate the need for conversions between Vec≤ and Vec.
What are the implications and trade-offs associated with these different data types during compilation to JavaScript? Do List, Vec, and Vec≤ all essentially translate into a JavaScript array? Furthermore, does Vec≤ encompass the functionalities of both List and Vec as a superset?
Thank you!