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

Question

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

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

Векторный параметр типа описывает «размеры» или «форму» тензора. В настоящее время я пытаюсь определить функцию для безопасного индексирования в Tensor. Я планировал сделать это, используя Fin с, но у меня возникла проблема. Поскольку 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?

Answer 1

Ваша жизнь становится намного проще, если вы позволяете для завершающего () в вашем 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) 

причина это работает, и ваш не потому, что здесь, каждый с ase от index соответствует точно одному корпусу TensorIndex, и поэтому TensorIndex ds может быть уменьшен.

Answer 2

Ваши определения будут более чистыми, если вы определяете 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