haskell - 定义访问多维数组的运算符

Question

我想到了定义一个运算符，它接受(可能)多维列表和索引列表，并返回元素。我的原型(prototype)尝试是:

(!!!) xs [i]            = xs !! i
(!!!) xs (cI : restI)   = (xs !! cI) !!! restI

现在回想起来，这显然存在很多问题。我首先无法找出类型签名，然后我意识到在第 2 行中， (xs !! cI) 的返回类型会不断变化，甚至可能并不总是列表(在最后一个“迭代”中)

我意识到要使用标准下标运算符访问多维数组，您可以简单地将其链接起来，如下所示:

[[1,2,3],[4,5,6],[7,8,9]] !! 1 !! 1 = 5

并意识到这看起来很像折叠，所以我尝试了:

(!!!) xxs inds = foldl (!!) xxs inds
or simply (!!!) = foldl (!!) 

但是我遇到了与第一次尝试相同的错误；我正在尝试构造一个无限类型。

这种类型的功能是否可能(通过黑客或其他方式)？我开始认为它的类型太悬而未决了。

举个例子，我的目标如下:

[[1,2,3],[4,5,6],[7,8,9]] !!! [1,1] = 5

Answer 1

只要您不必须使用列表来存储索引，您就可以毫不费力地做到这一点。索引必须作为数据类型传递，该数据类型对类型中有多少个索引进行编码。规范长度索引列表类型如下所示:

data Nat = Z | S Nat

infixr 5 :>
data Vector (n :: Nat) a where 
  Nil :: Vector Z a 
  (:>) :: a -> Vector n a -> Vector (S n) a 

那么你的函数是

(!!!) a Nil = a 
(!!!) a (i :> is) = (a !! i) !!! is 

您会注意到这无法编译。这是因为第一行和第二行中a的类型不同。 a 的类型必须取决于索引的类型，并且您必须准确地告诉编译器它们如何依赖它。这种依赖性非常简单；当有n个索引时，必须有一个n维的列表:

type family Dimension (n :: Nat) (v :: * -> *) (x :: *) :: * where 
  Dimension     Z v x = x 
  Dimension (S n) v x = v (Dimension n v x)

那么上面的类型就很简单了

(!!!) :: Dimension n [] a -> Vector n Int -> a

我不知道你对 Haskell 类型系统的更高级功能有多熟悉，但是上面需要type families和 data kinds .