Haskell - 如何定义依赖类型 Remainder(即 Rmndr 模数)？

Question

我的理解是余数类型是依赖类型(依赖于取模)。我阅读了有关 DataKinds 扩展的信息，并能够像下面这样定义它:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs #-}
data Nat = Zero | Succ Nat

data Rmndr modulo where
    Nil :: Rmndr Zero
    Rmndr :: Integer -> Rmndr modulo

但是当我开始实现 Eq 类时，我陷入了这种情况

Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo)

因为模数不是一个值，而是一种类型。即使我们可以编写如下函数:

decat :: Nat -> Integer
decat Zero = 0
decat (Succ nat) = decat nat + 1

我们不能像下面这样使用它

instance Eq (Rmndr modulo) where
    Nil == Nil = True
    Rmndr x == Rmndr y =
        x `mod` (decat modulo) == y `mod` (decat modulo)

因为此语法中的“模数”不是变量。

谁能帮忙解开这个谜题？非常感谢!

Answer 1

诀窍是使用类型类将每个自然数类型与一个单例 值相关联。为此，我们为 Zero 创建一个与 0 关联的实例，并为 Succ x 创建一个递归实例。要访问类型本身，我们需要采用虚拟代理参数。代理参数的习惯用法是使用一个名为 proxy a 的类型变量；当您调用它时，您最常使用 Data.Proxy 中的 Proxy。

这是相关的类:

class SingNat n where
  sing :: proxy n -> Integer

和实例:

instance SingNat Zero where sing _ = 0

instance SingNat n => SingNat (Succ n) where
  sing _ = 1 + sing (Proxy :: Proxy n)

要完成所有这些工作，您还必须启用 ScopedTypeVariables 以确保 ::Proxy n 中的 n 与SingNat (Succ n) 中的一个。

这里的一个很好的直觉是，两个 typelcass 实例就像 decat 函数的两个 case，但在类型级别。类型类像这样用作一种小型类型级逻辑编程语言，与迷你 Prolog 没有什么不同。

现在您可以使用 sing 来获取 Eq(以及其他地方)定义中的模绑定(bind):

instance SingNat n => Eq (Rmndr n) where
  Rmndr x == Rmndr y = (x `mod` modulo) == (y `mod` modulo)
    where modulo = sing (Proxy :: Proxy n)

这种代码是掌握类型级编程的好方法。但是，在实际代码中，您可能不想使用自己的自然数类型，因为 GHC 有一个内置的 DataKinds。除了标准之外，这还在类型级别为您提供了一些语法糖，让您可以编写类似 Rmndr 10 的类型。如果您对这种方法感到好奇，请查看我的 modular-arithmetic包，它实现了你的提醒类型，但使用了内置的类型级别数字和一些更好的语法。代码很短，所以只需阅读源代码即可。