Векторы Идриса против связанных списков

Проводит ли Идрис какую-либо оптимизацию под капотом векторов? Потому что, судя по всему, вектор Идриса - это просто связанный список с известным размером (известным во время компиляции). Фактически, в целом кажется, что вы могли бы выразить следующую эквивалентность (я немного догадываюсь о синтаксисе):

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

Так что, хотя это хорошо с точки зрения предотвращения ошибок диапазона, реальное преимущество векторов (в традиционном использовании этого термина) заключается в производительности; в частности, произвольный доступ O (1). Кажется, что вектор idris не поддерживает это (как бы вы написали функцию индексации, чтобы иметь такую ​​производительность?).

  • Если предположить, что под капотом не происходит никакого волшебства (как это происходит с Nat) для перенастройки Vectors, существует ли в Идрисе тип данных с произвольным доступом?
  • Как бы такая вещь была определена в системе алгебраических типов? Конечно, кажется, что невозможно определить его индуктивно.
  • Возможно ли в такой системе типов, как у Идриса, создать тип данных, который поддерживает произвольный доступ O (1), и знает его длину, так что весь доступ доказуемо действителен? (В Haskell есть векторы в стиле массива, но их конкретная реализация непонятна среднему пользователю, включая меня)

vector linked-list algebraic-data-types idris
person limp_chimp    schedule 18.12.2014    source источник

Ответы (2)


arrow_upward
16
arrow_downward

Он ничего не делает для оптимизации поиска векторов (по крайней мере, на момент написания этого ответа).

На самом деле это не из-за каких-либо трудностей, а скорее потому, что я предпочел бы иметь какую-то общую структуру для написания такого рода оптимизации, чем жесткое кодирование многих из них. По общему признанию, у нас уже есть жестко запрограммированные оптимизации для Nat, но я все же предпочел бы не добавлять дополнительные нагрузки специальным образом.

В зависимости от того, для чего вы действительно этого хотите, может оказаться, что вам поможет экспериментальная система типов уникальности, поскольку вы можете иметь под капотом изменяемую вещь низкого уровня и при этом иметь безопасный и эффективный доступ и обновление в чистом стиле на высоком уровне. уровень языка. Посмотрим...

person Edwin Brady    schedule 24.12.2014

arrow_upward
3
arrow_downward

У Эдвина есть исчерпывающие ответы о том, что Идрис делает в настоящее время. Однако, если вы ищете что-то, что может быть естественным для оптимизации поиск в постоянном времени в некоторых случаях, следующее может быть шагом в правильном направлении.

Для векторов фиксированного размера времени компиляции (т. Е. Не под лямбдой, не параметризованной длиной на верхнем уровне) следующая структура дает вам векторы и функции поиска, которые для любой фиксированной конкретной длины могут быть нормализованы во время компиляции до функции, которые должны быть легко оптимизированы в функции с постоянным временем. (Извините, код находится в Coq; у меня на данный момент нет рабочей версии Idris, и я плохо ее знаю. Я буду рад заменить это кодом Idris, если кто-то предложит правильный синтаксис, например, в комментарий.)

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.

Идея состоит в том, что для любого фиксированного n нормальная форма get нерекурсивна, поэтому компилятор может гипотетически скомпилировать его в функцию, время выполнения которой не зависит от того, что n < / em> бывает.

person Jason Gross    schedule 01.01.2015
comment
Первоначальный вопрос касался доступа к элементу в O (1). Очевидно, если вы исправите n, то доступ будет в постоянное время. - person jch; 02.01.2015
comment
Я отредактировал последнее предложение, чтобы прояснить следующий момент, надеюсь: Дело в том, что n должно быть зафиксировано на значении, где бы оно ни использовалось. Он должен быть O (1) в зависимости от значения, которое вы исправили n во время компиляции. То есть в гипотетическом мире, где Идрис может скомпилировать A * B * ... * C в массив, абсолютное время выполнения при подключении n = 5 должно быть таким же, как при подключении n = 100000, но только если вы делаете это во время компиляции. - person Jason Gross; 04.01.2015