haskell - 如何在 Haskell 中实现部分内射类型系列？

Question

我在 Haskell 中实现了各种需要类型安全自然数的函数，最近需要一个指数类型来表示一个新类型。
为便于引用，以下是我到目前为止编写的三个类型系列。

type family Add n m where
  Add 'One n = 'Succ n
  Add ('Succ n) m = 'Succ (Add n m)

-- Multiplication, allowing ever more powerful operators
type family Mul n m where
  Mul 'One m = m
  Mul ('Succ n) m = Add m (Mul n m)

-- Exponentiation, allowing even even more powerful operators
type family Exp n m where
  Exp n 'One = n
  Exp n ('Succ m) = Mul n (Exp n m)

但是，在使用这种类型时，我遇到了它不是单射的问题；这意味着我想要的一些类型推断并不存在。 (错误是 NB: ‘Exp’ is a non-injective type family )。我可以通过使用 -XAllowAmbiguousTypes 来忽略这个问题，但我不想使用这个扩展，所以所有类型都可以检查函数的定义位置。
我认为当 m 是常数时 Exp n m 应该是单射的，所以我想尝试实现它，但是经过大量的反复试验，我不确定如何做到这一点。即使它目前不能解决我的问题，它也可能在 future 有用。或者， Exp n m 对于给定的 n 是单射的，其中 m 发生变化，而 n 不是 One 。
在询问其他人后，他们建议使用 type family Exp n m = inj | inj, n -> m where 之类的东西，但这不起作用，如果逗号存在，则会在逗号上出现语法错误，如果不存在，则会在最终的 n 上出现解析错误。这旨在允许 inj 和 n 唯一标识给定的 m 。
我正在尝试实现但遇到问题的函数当前具有如下签名。 tensorPower :: forall i a n m . (Num a, KnownNat i) => Matrix n m a -> Matrix (Exp n i) (Exp m i) a可以使用 tensorPower @Three a(设置 -XAllowAmbiguousTypes 时)调用此函数，但如果可能，我希望 GHC 能够自行确定 i 值。对于这个问题，可以假设给定的 a 矩阵不是多态的。
将约束调整为以下也不起作用；这是在上述函数的类型中创建注入(inject)性的尝试，而不是在定义类型族的地方

forall i a n m
   . ( Num a
     , KnownNat i
     , Exp n ( 'Succ i) ~ Mul n (Exp n i)
     , Exp m ( 'Succ i) ~ Mul m (Exp m i)
     , Exp n One ~ n
     , Exp m One ~ m
     )

那么，是否可以为这个函数实现注入(inject)性，如果是，我该如何实现呢？
(要查看更多正在运行的代码，请访问 repository 。 src 文件夹包含大部分代码源，此问题中涉及的主要区域属于 Lib.hs 和 Quantum.hs (大多数使用的扩展可以) 在 package.yaml 中找到)

Answer 1

实际上有一种令人惊讶的简单方法可以至少以一种方式使其工作；以下 type family 在约束中适当使用时，允许在没有注释的情况下使用 tensorPower。

-- Reverse the exponent - if it can't match then it goes infinitely
type family RLog n m x c where
  RLog m n n i = i
  RLog m n x i = RLog m n (Mul m x) ('Succ i)

type ReverseLog n m = RLog n m n 'One
type GetExp n i = ReverseLog n (Exp n i)
----------------
-- adjusted constraint for tensorPower
forall i a n m . (Num a, KnownNat i, i ~ GetExp n i, i ~ GetExp m i)

例如，现在可以输入 (tensorPower hadamard) *.* (zero .*. zero .*. one) (其中 hadamard 是 Matrix Two Two Double ， zero 和 one 都是 Matrix Two One Double ， (*.*) 是矩阵乘法， (.*.) 是张量积， i 的类型是完全推断出来的)。
这个类型族的工作方式是它有四个参数:基数、目标、累加器和当前指数。如果目标和累加器相等，则“返回”当前指数。如果它们不相等，我们通过将当前累加器乘以基数进行递归，并增加当前指数。
我可以看到这个解决方案有一个问题:如果它不能匹配“基础”，它就会有一个非常长的错误消息，因为它尽可能深入地递归到类型中。这可以通过做一些其他类型的技巧来解决，这超出了这个问题的范围，但可以在我的项目存储库的 this commit 中看到。
总而言之:引入一些抽象的注入(inject)似乎是行不通的，但是实现指数的某种反转会产生干净、简单且功能强大的代码——这就是有效的注入(inject)，通过证明 Exp 有一个可逆函数.
(一个注意事项是，这个解决方案需要更多的摆弄才能完全工作，因为 GetExp n i 对 n=='One 并不真正起作用；我已经解决了这个问题，因为从来没有 GetExp ('One) i 放在首位)