我的理解是余数类型是依赖类型(依赖于取模)。我阅读了有关 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)
因为此语法中的“模数”不是变量。
谁能帮忙解开这个谜题?非常感谢!
最佳答案
诀窍是使用类型类将每个自然数类型与一个单例 值相关联。为此,我们为 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包,它实现了你的提醒类型,但使用了内置的类型级别数字和一些更好的语法。代码很短,所以只需阅读源代码即可。
关于Haskell - 如何定义依赖类型 Remainder(即 Rmndr 模数)?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/28181234/