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

问题描述

我正在 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 应该是单射的，所以我想尝试实现它，但是经过大量的反复试验，我不确定如何做到这一点。即使它目前不能解决我的问题，它也可能在未来有用。或者，对于给定的 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 矩阵不是多态的。

将约束调整为以下也不起作用；这是在上述函数的类型中创建注入性的尝试，而不是在定义类型族的地方

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
     )

那么，这个函数是否可以实现注入性，如果可以，我该如何实现？

（要查看更多正在运行的代码，请访问 repository。src 文件夹包含大部分代码源，此问题中涉及的主要区域属于到 Lib.hs 和 Quantum.hs。使用的扩展名（大部分）可以在 package.yaml)

中找到

解决方法

实际上有一种令人惊讶的简单方法可以至少以一种方式使其工作；以下 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，{{ 1}} 是矩阵乘法，(*.*) 是张量积，(.*.) 的类型完全推断）。

这个类型族的工作方式是它有四个参数：基数、目标、累加器和当前指数。如果目标和累加器相等，则“返回”当前指数。如果它们不相等，我们通过将当前累加器乘以基数进行递归，并增加当前指数。

我可以看到这个解决方案有一个问题：如果它不能匹配“基础”，它就会有一个非常长的错误消息，因为它尽可能深入地递归到类型中。这可以通过做一些其他类型的技巧来解决，这超出了这个问题的范围，但可以在我项目存储库的 this commit 中看到。

总而言之：引入一些抽象的注入似乎是行不通的，但是实现指数的某种反转导致了干净、简单且有效的代码——这就是有效的注入，通过证明存在一个可逆函数对于i。

（需要注意的是，这个解决方案需要更多的调整才能完全发挥作用，因为 Exp 对 GetExp n i 并不真正有效；我从来没有 {{1} } 首先）

haskell haskell type-families type-level-computation