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

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)

因为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)

因为此语法中的"modulo"不是变量.

任何人都可以帮助解决这个难题吗？非常感谢!

Answer 1

诀窍是使用类型类将每个自然数类型与单例值相关联.我们通过创建一个用于Zero关联的实例0和一个递归实例来实现此目的Succ x.要访问类型本身,我们需要采用伪代理参数.代理参数的习惯用法是使用一个名为的变量proxy a; 当你打电话给这个时,你最常使用的Proxy是Data.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,以确保nin :: Proxy n与中的相同SingNat (Succ n).

这里一个很好的直觉是两个typelcass实例就像你的decat函数的两个例子,但在类型级别.像这样的函数使用的类型作为一种小型的逻辑编程语言,与迷你Prolog不同.

现在,您可以使用sing在Eq(和其他地方)的定义中获取模数约束:

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.如果您对这种方法感到好奇,请查看我的模块算术包,它实现了您的提醒类型,但使用内置类型级别编号和一些更好的语法.代码很短,所以只需阅读源代码.