Вычисление нетривиального типа Идриса для тензорной индексации

Я возился с простой тензорной библиотекой, в которой я определил следующий тип.

data Tensor : Vect n Nat -> Type -> Type where
  Scalar : a -> Tensor [] a
  Dimension : Vect n (Tensor d a) -> Tensor (n :: d) a

Векторный параметр типа описывает «размеры» или «форму» тензора. В настоящее время я пытаюсь определить функцию для безопасного индексирования в Tensor. Я планировал сделать это с помощью Fins, но столкнулся с проблемой. Поскольку Tensor имеет неизвестный порядок, мне может понадобиться любое количество индексов, для каждого из которых требуется своя верхняя граница. Это означает, что Vect индексов будет недостаточно, потому что каждый индекс будет иметь свой тип. Это побудило меня вместо этого взглянуть на использование кортежей (называемых «парами» в Идрисе?). Я написал следующую функцию для вычисления необходимого типа.

TensorIndex : Vect n Nat -> Type
TensorIndex []      = ()
TensorIndex (d::[]) = Fin d
TensorIndex (d::ds) = (Fin d, TensorIndex ds)

Эта функция работала так, как я ожидал, вычисляя соответствующий тип индекса из вектора размерности.

> TensorIndex [4,4,3] -- (Fin 4, Fin 4, Fin 3)
> TensorIndex [2] -- Fin 2
> TensorIndex [] -- ()

Но когда я попытался определить настоящую index функцию ...

index : {d : Vect n Nat} -> TensorIndex d -> Tensor d a -> a
index () (Scalar x) = x
index (a,as) (Dimension xs) = index as $ index a xs
index a (Dimension xs) with (index a xs) | Tensor x = x

... Идрис выдвинул следующую ошибку во втором случае (как ни странно, в первом случае все было в порядке).

Type mismatch between
         (A, B) (Type of (a,as))
and
         TensorIndex (n :: d) (Expected type)

Ошибка, по-видимому, подразумевает, что вместо того, чтобы рассматривать TensorIndex как чрезвычайно запутанный синоним типа и оценивать его так, как я надеялся, он рассматривал его так, как если бы он был определен с помощью объявления data; так сказать "типа черного ящика". Где Идрис подводит черту? Есть ли способ переписать TensorIndex, чтобы он работал так, как я хочу? Если нет, можете ли вы придумать другой способ написать функцию index?


dependent-type idris
person Kwarrtz    schedule 23.05.2016    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Ваша жизнь станет намного проще, если вы допустите конечный () в своем TensorIndex, с тех пор вы можете просто делать

TensorIndex : Vect n Nat -> Type
TensorIndex []      = ()
TensorIndex (d::ds) = (Fin d, TensorIndex ds)

index : {ds : Vect n Nat} -> TensorIndex ds -> Tensor ds a -> a
index {ds = []} () (Scalar x) = x
index {ds = _ :: ds} (i, is) (Dimension xs) = index is (index i xs)

Если вы хотите сохранить свое определение TensorIndex, вам понадобятся отдельные регистры для ds = [_] и ds = _::_::_, чтобы соответствовать структуре TensorIndex:

TensorIndex : Vect n Nat -> Type
TensorIndex []      = ()
TensorIndex (d::[]) = Fin d
TensorIndex (d::ds) = (Fin d, TensorIndex ds)

index : {ds : Vect n Nat} -> TensorIndex ds -> Tensor ds a -> a
index {ds = []} () (Scalar x) = x
index {ds = _ :: []} i (Dimension xs) with (index i xs) | (Scalar x) = x
index {ds = _ :: _ :: _} (i, is) (Dimension xs) = index is (index i xs)

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

person Cactus    schedule 24.05.2016
comment
@Kwarrtz: ответ обновлен, чтобы использовать ваше TensorIndex представление + объяснение. - person Cactus; 24.05.2016
comment
Спасибо за обновления. Итак, чтобы прояснить, часть, которую мне не хватало, на самом деле была неявным соответствием на ds? - person Kwarrtz; 24.05.2016
comment
Если вы не соответствуете ds, вы все равно можете узнать что-то об этом, сопоставив Scalar vs Dimension. Но просто Dimension не говорит вам, нужно ли сокращать TensorIndex ds для второго или третьего случая. - person Cactus; 24.05.2016

arrow_upward
9
arrow_downward

Ваши определения будут более ясными, если вы определите Tensor индукцией по списку измерений, в то время как Index определен как тип данных.

Действительно, в настоящий момент вы вынуждены сопоставлять шаблон для неявного аргумента типа Vect n Nat, чтобы увидеть, какую форму имеет индекс. Но если индекс определяется непосредственно как часть данных, тогда он ограничивает форму структуры, в которую он индексирует, и все становится на свои места: нужная информация поступает в нужное время для проверки типов быть счастливым.

module Tensor

import Data.Fin
import Data.Vect

tensor : Vect n Nat -> Type -> Type
tensor []        a = a
tensor (m :: ms) a = Vect m (tensor ms a)

data Index : Vect n Nat -> Type where
  Here : Index []
  At   : Fin m -> Index ms -> Index (m :: ms)

index : Index ms -> tensor ms a -> a
index Here     a = a
index (At k i) v = index i $ index k v
person gallais    schedule 26.05.2016
comment
Ваше предложение очень полезно. Я даже не рассматривал эту возможность, но это значительно упростило бы ситуацию. Я собираюсь оставить ответ Кактуса принятым, потому что он ответил первым и ответил на мой вопрос более прямо, но я ценю дополнительную информацию. - person Kwarrtz; 27.05.2016
comment
Это приятно, но кажется, что отсутствие конструктора типа проблематично для определения интерфейсов функторов для тензора и т. Д. ... - person shevket; 30.04.2021