用于张量索引的Idris非平凡类型计算

Question

我一直在搞乱一个简单的张量库,我在其中定义了以下类型.

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

该类型的矢量参数描述了张量的"尺寸"或"形状".我目前正在尝试定义一个安全索引到a的函数Tensor.我本来打算用Fins 做这个,但我遇到了一个问题.因为Tensor序列未知,我可能需要任意数量的索引,每个索引都需要不同的上限.这意味着一个Vect索引不足,因为每个索引都有不同的类型.这让我开始考虑使用元组(在Idris中称为"对"？).我编写了以下函数来计算必要的类型.

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

... Idris在第二种情况下提出了以下错误(奇怪的是,第一种情况似乎完全没问题).

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

这个错误似乎意味着,不是将其TensorIndex视为一个极其错综复杂的同义词,而是像我希望的那样对其进行评估,而是将其当作一个data声明来定义; 可以说是"黑盒式".伊德里斯在哪里划线？有没有办法让我重写,TensorIndex以便它按照我想要的方式工作？如果没有,你能想到写这个index功能的其他方法吗？

Answer 1

如果您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