如何定义一个使用列表的函数，该列表中的数字乘积与Haskell中使用GADT的矩阵中的元素数量相同

Question

我有的矩阵表示

data ListN (dim :: Nat) a where
Nil  :: ListN Zero a
Cons :: a -> ListN n a -> ListN (Succ n) a
infixr 5 `Cons`
data Tensor (dims :: [Nat]) a where
Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
Sparse :: Tensor n a

其中Product确保当你取dims的所有元素的乘积时dims等于n。现在我想要一个创建者函数和一个改变张量数据类型维度的函数。

1. 我想要一个改变矩阵维数的函数，但前提是给定[Nat]的乘积等于必须改变的矩阵的dims。我已经想到了类似的东西：reshape :: (Product lm ~ l, Product (ns :: [Nat]) ~ n, l ~ n ) => Tensor ns a -> lm -> Tensor lm a。但这不是类型检查
2. 我也想有一个函数，当给定[Nat]时，可以创建张量，但该列表应该有一个与给定ListN n a的元素数量相同的乘积。我想到了fromList :: (Product lm ~ l, Product (ns :: [Nat]) ~ n, l ~ n ) => ListN n a -> lm -> Tensor lm a。但这也不是类型检查

Answer 1

我猜您遇到的错误是这些类型最明显的问题——lm没有Type类型，这是(->)类型所要求的。这很容易修复。只需删除它。它是一个已经出现在签名中实际需要它的位置的类型。类型推理可以满足您的所有需求。

填写您遗漏的标准内容：

{-# Language DataKinds, TypeFamilies, UndecidableInstances, StandaloneKindSignatures #-}
data Nat = Zero | Succ Nat
type Add :: Nat -> Nat -> Nat
type family Add m n where
Add Zero n = n
Add (Succ m) n = Succ (Add m n)
type Mult :: Nat -> Nat -> Nat
type family Mult m n where
Mult Zero n = Zero
Mult (Succ m) n = Add n (Mult m n)
type Product :: [Nat] -> Nat
type family Product xs where
Product '[] = Succ Zero
Product (x : xs) = Mult x (Product xs)
data ListN (dim :: Nat) a where
Nil  :: ListN Zero a
Cons :: a -> ListN n a -> ListN (Succ n) a
infixr 5 `Cons`
data Tensor (dims :: [Nat]) a where
Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
Sparse :: Tensor n a

然后这些就行了：

reshape :: (Product ns ~ Product lm) => Tensor ns a -> Tensor lm a
reshape (Dense l) = Dense l
reshape Sparse = Sparse
fromList :: (Product lm ~ n) => ListN n a -> Tensor lm a
fromList = Dense

请注意，我也简化了每个签名中的约束。

在reshape中，这只是为了减少冗余。Dense构造函数上的匹配将约束带入范围，这足以允许它合成需要封装在新Dense构造函数中的约束。

对于fromList，我只是将其简化为Dense的类型。毕竟，这是完全相同的功能。(我仍然可以理解为什么你想用一个隐藏内部的名称来导出它，所以我理解它可能存在的原因。(