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

Question

作为一个玩具项目，我想了解如何建模的数学小组在哈斯克尔在总体上。

首先，我们从观察待定义的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

必须确定类型的循环组部分的顺序。这样做的一种方法是使用内置型水平自然数GHC给出了我们。

{-# 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，其中::的意思是“有种类”(而不是"has“)。
• ScopedTypeVariables使其能够使Proxy :: Proxy n中的n类型变量与实例头instance KnownNat m => Monoid (Cyclic n) where中的变量相同。