CODEWITHSUNDEEP
haskelltype-familiesabstract-algebra
pretzelKn0t
pretzelKn0t

Reputation: 132

How to constrain associated type synonyms?

I'm (relatively) new to Haskell and want to code some math. For example, abelian groups. I would like to write the following code:

{-# 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

Compiling the above gives me the error

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

This makes sense; I haven't ensured that (AbelianGroupElement g1) always has Eq defined for it. However, I'm not sure how I can accomplish that. I can change the above to

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

but this doesn't help. (It's possible that type families are the wrong way to go here; I originally started with MultiParamTypeClasses and FunctionalDependencies, but had other issues with that and got the impression that type families were better).

Thanks for reading this; any help would be appreciated.

Upvotes: 2

Views: 139

Answers (2)

pretzelKn0t
pretzelKn0t

Reputation: 132

I ended up switching to a MultiParamTypeClasses and FunctionalDependencies approach. I'm not sure if this is the best way to do things, but it at least solves this issue. I had tried this previously, but didn't know that I could add both dependencies e -> g and g -> e, which made a difference as far as getting this code to compile.

{-# 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)

Upvotes: 0

DDub
DDub

Reputation: 3924

You can use StandaloneDeriving to get basically what you want, although I admit it's not as pretty as simply writing deriving Eq:

{-# LANGUAGE StandaloneDeriving #-}

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

Upvotes: 2

Related Questions