如何约束关联类型同义词？

问题描述

我（相对）是 Haskell 的新手，想编写一些数学代码。例如，阿贝尔群。我想写如下代码：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module Structures where

class Eq g => AbelianGroup g where
    type family AbelianGroupElement g = e | e -> g
    add :: AbelianGroupElement g -> AbelianGroupElement g -> AbelianGroupElement g
    inv :: AbelianGroupElement g -> AbelianGroupElement g
    unit :: g -> AbelianGroupElement g
    parent :: AbelianGroupElement g -> g

data Z = Z deriving Eq
data ZElement = ZElement Z Int deriving Eq

instance AbelianGroup Z where
    type instance AbelianGroupElement Z = ZElement
    add (ZElement z1 x1) (ZElement z2 x2)
        | z1 == z2 = (ZElement z1 (x1+x2))
        | otherwise = error "elements from different groups"
    inv (ZElement z x) = (ZElement z (-x))
    unit z = ZElement z 0
    parent (ZElement z x) = z

data ProductAbGrp g1 g2 = 
    ProductAbGrp g1 g2 deriving Eq
data ProductAbGrpEl g1 g2 = 
    ProductAbGrpEl (ProductAbGrp g1 g2) (AbelianGroupElement g1) (AbelianGroupElement g2) deriving Eq

编译上面给了我错误

No instance for (Eq (AbelianGroupElement g1))
        arising from the second field of `ProductAbGrpEl'
          (type `AbelianGroupElement g1')

这是有道理的；我还没有确保 (AbelianGroupElement g1) 总是为它定义 Eq 。但是，我不确定如何才能做到这一点。我可以把上面的改成

{-# LANGUAGE FlexibleContexts #-} 
...
class (Eq g,Eq (AbelianGroupElement g)) => AbelianGroup g where

但这无济于事。 （类型族可能是错误的方法；我最初从 MultiParamTypeClasses 和 FunctionalDependencies 开始，但遇到了其他问题，并觉得类型族更好。

感谢您阅读本文；任何帮助将不胜感激。

解决方法

您基本上可以使用 StandaloneDeriving 来获得您想要的东西，尽管我承认它并不像简单地编写 deriving Eq 那样漂亮：

{-# LANGUAGE StandaloneDeriving #-}

deriving instance (Eq g1,Eq g2,Eq (AbelianGroupElement g1),Eq (AbelianGroupElement g2)) => Eq (ProductAbGrpEl g1 g2)

,

我最终切换到 MultiParamTypeClasses 和 FunctionalDependencies 方法。我不确定这是否是最好的做事方式，但它至少解决了这个问题。我以前试过这个，但不知道我可以添加两个依赖项 e -> g 和 g -> e，这对编译这段代码产生了影响。

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}    

module Structures where
    
class (Eq g,Show g,Eq e,Show e) => AbelianGroup g e | e -> g,g -> e where
    zero :: g -> e
    add :: e -> e -> e
    neg :: e -> e
    parent :: e -> g

data Z = Z deriving (Eq,Show)
data ZElement = ZElement Z Int deriving (Eq,Show)

instance AbelianGroup Z ZElement where
    zero z = ZElement z 0
    add (ZElement z1 x1) (ZElement z2 x2)
        | z1 == z2 = (ZElement z1 (x1+x2))
        | otherwise = error "elements from different groups"
    neg (ZElement z x) = (ZElement z (-x))
    parent (ZElement z x) = z

data ProductAbelianGroup g1 g2 e1 e2 = ProductAbelianGroup g1 g2 deriving (Eq,Show)
data ProductAbelianGroupElement g1 g2 e1 e2 = ProductAbelianGroupElement g1 g2 e1 e2 deriving (Eq,Show)