Currently, the type of vectors related to a function dropping the nat parameter and returning list. The problem is that this encoding makes it impossible to define a partial inverse function going back to vectors without having an inhabitant of the parameter to cover the case where the list is smaller than the expected index n.
Defining a version of vectors and lists taking an inhabited type {A : Type & A} as a parameter would be cumbersome because we would have to redefine all the operations on these custom versions, which brings back the complexity of handling Σ-types we wanted to avoid by relating vectors to lists in the first place (otherwise we would have chosen the following association:
Vector.t A n ~ {l : list A & length l = n}
The problem looks similar in the case of relating matrices to arrays of arrays, as this last container type does not have an index constraining its length.
Currently, the type of vectors related to a function dropping the
nat
parameter and returninglist
. The problem is that this encoding makes it impossible to define a partial inverse function going back to vectors without having an inhabitant of the parameter to cover the case where the list is smaller than the expected indexn
.Defining a version of vectors and lists taking an inhabited type
{A : Type & A}
as a parameter would be cumbersome because we would have to redefine all the operations on these custom versions, which brings back the complexity of handling Σ-types we wanted to avoid by relating vectors to lists in the first place (otherwise we would have chosen the following association:The problem looks similar in the case of relating matrices to arrays of arrays, as this last container type does not have an index constraining its length.