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

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

您必须使该类型的循环组部分的顺序.这样做的一种方法是使用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不是类型的类型参数.我们说它的类型不是type(*).在这种情况下,n有kind Nat(n :: Nat).
• KindSignatures只是让我们n :: Nat在::有意义的时候写出"有种类"(而不是"有类型")的地方.
• ScopedTypeVariables使得n类型变量Proxy :: Proxy nin与实例头中的变量相同instance KnownNat m => Monoid (Cyclic n) where.