tag - Idris vectores vs listas enlazadas

tag free traduccion

Question

¿Idris hace algún tipo de optimización bajo el capó de vectores? Debido a su aspecto, un vector Idris es solo una lista enlazada con un tamaño conocido (conocido en tiempo de compilación). De hecho, en general parece que podrías expresar la siguiente equivalencia (supongo un poco en la sintaxis):

Vector : Nat -> Type -> Type
Vector n t = (l: List t ** length l = n)

Entonces, aunque esto es bueno en el sentido de prevenir errores de rango, la ventaja real de los vectores (en el uso tradicional del término) es en términos de rendimiento; en particular, O (1) acceso aleatorio. Parece que el vector idris no lo admitiría (¿cómo escribiría la función de indexación para tener este rendimiento?).

• Suponiendo que no haya ninguna magia bajo el capó (como ocurre con Nat ) para reconfigurar Vector s, ¿hay un tipo de datos de acceso aleatorio en Idris?
• ¿Cómo se define / define una cosa así en un sistema de tipo algebraico? Ciertamente, parece que sería imposible definirlo inductivamente.
• ¿Es posible, dentro de un sistema de tipos como el de Idris, crear un tipo de datos que admita el acceso aleatorio O (1), y sea ​​consciente de su longitud de tal manera que todos los accesos sean demostrablemente válidos? (Haskell tiene vectores de estilo de matriz, pero su implementación concreta es opaca para el usuario promedio, incluyéndome a mí)

Answer 1

No hace nada para optimizar las búsquedas de vectores (al momento de escribir esta respuesta, al menos).

Esto no se debe a ninguna dificultad para hacerlo, en realidad, sino más bien porque preferiría tener algún tipo de marco general para escribir este tipo de optimización en lugar de codificarlo en muchos. Es cierto que ya tenemos optimizaciones codificadas para Nat , pero aún así preferiría no agregar más cargas de manera ad hoc.

Dependiendo de lo que realmente lo desee, puede ser que el sistema experimental de tipo de singularidad lo ayude, ya que podría tener un nivel bajo mutable bajo el capó y aún así tener un acceso y actualización seguros y eficientes en un estilo puro en el más alto nivel. lenguaje de nivel Ya veremos...

Answer 2

Edwin tiene las respuestas definitivas sobre lo que hace actualmente Idris. Sin embargo, si está buscando algo que podría ser natural para optimizar la búsqueda en tiempo constante en algunos casos, lo siguiente podría ser un paso en la dirección correcta.

Para vectores de tamaño fijo en tiempo de compilación (es decir, no bajo un lambda, no parametrizado por longitud en el nivel superior), la siguiente estructura le proporciona vectores y funciones de búsqueda que, para cualquier longitud de hormigón fija, se pueden normalizar en tiempo de compilación a Funciones que deberían ser optimizables hasta cierto punto en funciones de tiempo constante. (Lo siento, el código está en Coq; no tengo una versión funcional de Idris en este momento, y no lo sé bien. Estoy feliz de reemplazarlo con el código de Idris si alguien sugiere la sintaxis correcta, por ejemplo, en un comentario.)

Fixpoint vector (n : nat) (A : Type) :=
  match n return Type with
    | 0 => unit
    | S n'' => (A * vector n'' A)%type
  end.
Definition nil {A} : vector 0 A := tt.
Definition cons {n} {A : Prop} (x : A) (xs : vector n A) : vector (S n) A
  := (x, xs).
Fixpoint get {n} {A : Prop} (m : nat) (default : A) (v : vector n A) {struct n} : A
  := match n as n return vector n A -> A with
       | 0 => fun _ => default
       | S n'' => match m with
                   | 0 => fun v => fst v
                   | S m'' => fun v => @get n'' A m'' default (snd v)
                 end
     end v.

La idea es que, para cualquier n fija, la forma normal de get no es recursiva, por lo que el compilador podría, hipotéticamente, compilarla en una función cuyo tiempo de ejecución sea independiente de lo que n sea.