时间戳

首页 > 解决方案 > 如何在 Haskell 中实现部分单射类型族？

haskell - 如何在 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 来忽略这个问题，但我不想使用这个扩展，所以所有类型都可以检查函数的定义位置。

我认为Exp n m当 m 是常数时这应该是单射的，所以我想尝试实现它，但我不确定如何在经过大量试验和错误后做到这一点。即使它目前不能解决我的问题，它也可能在将来有用。或者，对于给定的where变化Exp n m是单射的，而不是。nmnOne

在询问其他人后，他们建议使用类似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

可以使用（设置 -XAllowAmbiguousTypes 时）调用此函数tensorPower @Three a，但我希望 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
     )

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

（要查看更多实际代码，请访问存储库。该src文件夹包含大部分代码源，在此问题中涉及的主要区域属于Lib.hs和Quantum.hs。可以（大部分）找到使用的扩展在package.yaml）

标签： haskelltype-familiestype-level-computation

解决方案

实际上有一种非常简单的方法可以让它至少以一种方式工作。以下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)（其中hadamardis Matrix Two Two Double，两者zero和oneare Matrix Two One Double，(*.*)是矩阵乘法，(.*.)是张量积，并且类型i是完全推断的）。

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

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

总而言之：引入一些抽象的注入性似乎是不可行的，但是实现一种指数的反转会产生干净、简单和功能正常的代码——这实际上是注入性，通过证明Exp.

（一个注意事项是，这个解决方案需要更多的摆弄才能充分发挥作用，因为GetExp n i它并不真正适用n=='One；我一开始就没有解决这个GetExp ('One) i问题）

推荐阅读