haskell - 如何从类实例中抽象数据类型参数？

Question

作为一个玩具项目，我想了解如何在 Haskell 中对数学群进行建模。

首先，我们首先观察要定义的Group只是一个具有反转的Monoid。

class (Monoid m) => Group m where
    minvert :: m -> m

接下来，我们首先将自己限制在循环群上，并从定义 12 阶循环群开始。

data Cyclic12 = Cyclic12 Int deriving (Show, Eq)

最后，我们实例化 Cyclic12 的两个类。

instance Monoid Cyclic12 where
    mempty = Cyclic12 0
    mappend (Cyclic12 x) (Cyclic12 y) = Cyclic12 ((x + y) `mod` 12)

instance Group Cyclic12 where
    minvert (Cyclic12 x) = Cyclic12 ((0 - x) `mod` 12)

如何从 12 的具体值中抽象出先前的定义，以允许对不同的循环群进行更通用的定义？

理想情况下，我想编写如下定义

instance Monoid (Cyclic k) where
    mempty = Cyclic k 0
    mappend (Cyclic k x) (Cyclic k y) = Cyclic k ((x + y) `mod` k)

instance Group (Cyclic k) where
    minvert (Cyclic k x) = Cyclic k ((0 - x) `mod` k)

但是数据定义如下

data Cyclic = Cyclic Int Int deriving (Show, Eq)

我们仍然没有走得太远，因为k“不在范围内”。鉴于其明显的琐碎性，我感觉在这里错过了一些基本概念。在此先感谢您的帮助。

Answer 1

您必须将循环群的顺序作为类型的一部分。一种方法是使用 the builtin type level natural numbers GHC gives us .

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}

import GHC.TypeLits
import Data.Proxy (Proxy(..))

data Cyclic (n :: Nat) = Cyclic Integer deriving (Show, Eq)

这让我们可以很容易地创建两个实例:

instance KnownNat n => Monoid (Cyclic n) where
    mempty = Cyclic 0
    Cyclic x `mappend` Cyclic y = Cyclic $ (x + y) `mod` natVal (Proxy :: Proxy n)

instance KnownNat n => Group (Cyclic n) where
    minvert (Cyclic x) = Cyclic $ negate x `mod` natVal (Proxy :: Proxy n)

签名的 KnownNat 部分基本上表示，无论 n::Nat 最终是什么，我们都应该能够使用 提取其值natVal.

然后，一旦加载到 GHCi 中:

ghci> :set -XDataKinds
ghci> type Z12 = Cyclic 12
ghci> mappend (Cyclic 8 :: Z12) (Cyclic 7 :: Z12)
Cyclic 3
ghci> minvert (Cyclic 4 :: Z12)
Cyclic 8

除了扩展

• DataKinds 让我们拥有一个不是类型的类型参数 n。我们说它的种类不是类型(*)。在本例中，n 具有类型 Nat (n::Nat)。
• KindSignatures 只是让我们写 n::Nat 其中 :: 表示“有种类”(而不是“有类型”)这是有道理的。
• ScopedTypeVariables 使得 Proxy::Proxy n 中的 n 类型变量与实例头中的类型变量相同实例 KnownNat m => Monoid(循环 n)，其中。