What is the relation between type classes, laws that they should follow and mathematical properties?

Learn
#1

I’ve been trying for a while to write a Haskell library for set/semigroup/monoid/group actions (I know some already exist). One design I’ve been wanting to use is to define the class

class LAct s x where
  lact :: s -> x -> x
  infixr 5 `lact`

and then add different properties this action might satisfy like the following ones :

-- (s <> t) <>$ x === s <>$ t <>$ x
class (LAct s x, Semigroup s) => LActSg s x

-- mempty <>$ x === x
class (LActSg s x, Monoid s) => LActMn s x

-- s <>$ (x <> y) === (s <>$ x) <> (s <>$ y)
class (LActSg s x, Semigroup x) => LActSgMorph s x

-- s <>$ mempty === mempty
class (LActMn s x, LActSgMorph s x, Monoid x) => LActMnMorph s x
Now in terms of instances, I would like to be able to write both instances of the form
-- driven by second parameter
instance LAct s x => LAct s [x] where
   lact s l = map (s <>$) l


-- driven by first parameter
instance LAct s x => LAct [s] x where
  lact l x = foldr lact x l

Now this absolutely cannot work and will always overlap. Worse, no instance would be a specialisation of the other one.

There is a trick though. It looks pretty nasty but it does work : I can decide that instances of LAct
are always driven by the first parameter, and declare another type class LAct’ that is driven by the second parameter along with a lifting of all instances of LAct’ into instances of LAct

class LAct' s x where
  lact' :: s -> x -> x

instance {-# OVERLAPPABLE #-} LAct' s x => LAct s x where
  (<>$) = lact'

Now I wan define the following instance that will always be chosen by the type checker only if it doesn’t find any first driven parameter instance

instance LAct s x => LAct' s [x] where
  lact' s l = map (s <>$) l

This is more comfortable to code with as it seems, and one do not have to bother about overlapping instances, just use LAct’ when one need an instance driven by the second parameter.

But there is a huge problem when I start to combine this trick with action properties like LActSg, LActMn…
I could declare second paramater driven versions of this properties, by writing something like

class (LAct' s x, Semigroup s) => LActSg' s x
instance LActSg [s] x where
  lact l x = foldr lact x l
instance {-# OVERLAPPABLE #-}LActSg' s x => LActSg s x

But this is wrong because of the overlappings. There might be cases where the instance above is not opverlapped (because the overlapping action does NOT have the semigroup action property) but the type system will still think that this action has the property.

So here is my questions :

  • How common is the practice of using type classes as some mathematical properties ?
    (There are some packages like commutative-semigroups that relies only on this trick)
  • Is it considered good practice ?
  • It feels fundamentally not compatible with overlapping instances, how bad is it ? Is this something you’ve already experienced ?

I’d like to finish this post with an idea. One way to solve some of those questions would be to have some kind of Haskell extension that I would call something like “ExplicitLaws”
It would allow to write something like the following

{-# LANGUAGE ExplicitLaws #-}

class LAct s x where
  law LActSg s x
  law LActMn s x
  law LActSgMorph s x
  law LActMnMorph s x

  implies LActMn s x => LActSg s x
  implies LActSgMorph s x => LActSg s x
  implies LActMnMorph s x => (LActSg s x, LActSgMorph s x)

  (<>$) :: s -> x -> x

instance LAct s x => LAct [s] x where
  abides LActMn s x
  lact l x = foldr lact x l

-- We could use such explicit laws in a lot of cases, for instance for defining Semigroup in terms of Magma

class Magma s where
  law Associative s
  law Commutative s
  (<>) :: s -> s -> s

type Semigroup s = (Associative s, Magma s)

instance Semigroup (Sum Int) where
  -- somehow the compiler adds the "abides" declaration itself since it is an instance of Semigroup
  (<>) = (+)
#2

Other, more experienced minds may correct me, but:

How common is the practice of using type classes as some mathematical properties ?

It depends on what you mean by that - as you observed, Haskell uses typeclasses extensively to represent mathematical and algebraic constructs such as monoids and groups and rings. However, the lawfulness of typeclasses is merely strongly suggested by convention, and is not enforced by the compiler - it is still up to the programmer to ensure that their instances are lawful.

Is it considered good practice ?

It is certainly good practice to make your instances lawful. Actually proving it is unfortunately moreso left to documentation and unit tests.

If you need to enforce lawful behavior with your typeclasses at compile-time, you may want to look into something like LiquidHaskell which allows you to enforce laws through proofs. Otherwise, you are left to a more proof-oriented language like Coq.

It feels fundamentally not compatible with overlapping instances, how bad is it ? Is this something you’ve already experienced ?

I think overlapping instances is just a bandaid hiding your real problem, which you may have already observed - the need to create new typeclasses for each new combination of laws. It creates a combinatorial explosion of typeclass hierarchies, and it really isn’t sustainable. Plus, there still is the classic issue of multiple conformance, eg an Integer is a Monoid in more than one way.

In my own experimentation I have found the following method satisfactory for enforcing algebraic laws as constraints with a minimal amount of boilerplate, although it still does not go as far as to require proof.

I believe I have posted this elsewhere but cannot find it to link, so here is an example using binary operation:

{-# LANGUAGE
    AllowAmbiguousTypes
,   FlexibleContexts
,   FlexibleInstances
,   KindSignatures
,   MultiParamTypeClasses
,   OverloadedStrings
,   ScopedTypeVariables
,   TypeApplications
,   UndecidableSuperClasses
#-}

module AlgebraicConstraints where

import Prelude

import GHC.Exts (Constraint)

{-
AllowAmbiguousTypes is needed for defining a constraint typeclass
-}

class Binop (r :: * -> Constraint) where
    binop :: (r a) => a -> a -> a

{-
AllowAmbiguousTypes, UndecidableSuperClasses is needed for defining laws
-}

class (Binop r, r a) => Associative r a where
    associate :: (r a) => a -> a -> a
    associate = binop @r

class (Binop r, r a) => Commutative r a where
    commutate :: (r a) => a -> a -> a
    commutate = binop @r

{-
Neither AllowAmbiguousTypes nor UndecidableSuperClasses are needed for defining
instances
-}

class Addition a where
    plus :: a -> a -> a

instance Binop Addition where
    binop = plus

instance Addition Integer where
    plus = (+)
instance Associative Addition Integer where
instance Commutative Addition Integer where

instance Addition String where
    plus = (++)
instance Associative Addition String where
-- NOTE: Addition String is not Commutative

{-
Using it is fairly simple
-}

-- We can be very general with binop:
fifteen :: Integer
fifteen = binop @Addition 5 10

-- Or more specific with associate:
foobar :: String
foobar = associate @Addition "foo" "bar"

-- We can define functions with lawful constraints:
commutativeAddition :: (Commutative Addition a) => a -> a -> a
commutativeAddition = commutate @Addition

-- We can even throw an error if the relation does not satisfy our properties
-- This compiles:
two :: Integer
two = commutate @Addition 1 1
-- This doesn't compile:
-- Error: No instance for (Commutative Addition String) arising from a use of ‘commutate’
-- rejected :: String
-- rejected = commutate @Addition "first" "second"

AllowAmbiguousTypes and UndecidableSuperClasses can be scary, but I believe they are appropriately used here, especially if you split off the constraints and laws into their own modules and only enable AllowAmbiguousTypes and UndecidableSuperClasses there.

1 Like
#3

Classes are not always used for laws. In this instance it is actually better not to, and to rely on the properties of the thing you want as an action and the thing you want to be acted on. Here’s my Data.Action:

module Data.Action
  ( Action (action)
  , actions
  ) where

import Data.Foldable
import Data.List.NonEmpty (NonEmpty, (<|))
import Data.Semigroup

-- | One type can affect, or perform an 'action', on another in some way.
class Action g x where
  action :: g -> (x -> x)

-- | Semigroups act on themselves.
instance (Semigroup g) => Action g g where
  action :: g -> (g -> g)
  action = (<>)

-- | Elements act on linked lists by prepending.
instance Action x [x] where
  action :: x -> ([x] -> [x])
  action = (:)

-- | Elements act on linked lists by prepending.
instance Action x (NonEmpty x) where
  action :: x -> (NonEmpty x -> NonEmpty x)
  action = (<|)

-- | All of the actions in a 'Foldable' container can constitute one action.
actions :: (Foldable t, Action g x) => t g -> (x -> x)
actions = foldl' (\a -> (.) a . action) id

-- | Input-valued functions act on their inputs.
instance Action (x -> x) x where
  action :: (x -> x) -> (x -> x)
  action = ($)

-- | Endomorphisms act on their inputs.
instance Action (Endo x) x where
  action :: Endo x -> (x -> x)
  action = appEndo

-- | Actions act on functions via precomposition.
instance (Action h x) => Action h (x -> a) where
  action :: (Action h x) => h -> ((x -> a) -> (x -> a))
  action h = (. action h)

-- Actions of various semigroups on their base type.

instance Action (First x) x where
  action :: First x -> x -> x
  action (First f) = const f

instance Action (Last x) x where
  action :: Last x -> x -> x
  action (Last _) = id

instance (Ord x) => Action (Min x) x where
  action :: Min x -> x -> x
  action (Min x) = min x

instance (Ord x) => Action (Max x) x where
  action :: Max x -> x -> x
  action (Max x) = max x

instance (Num n) => Action (Sum n) n where
  action :: Sum n -> n -> n
  action (Sum x) y = x + y

instance (Num n) => Action (Product n) n where
  action :: Product n -> n -> n
  action (Product x) y = x * y

The last section shows how the action doesn’t depend on the structure of the type as much as which types it’s applied to. I believe you’re looking for type synonyms in the wrong place.

#4

Weeell … You can get this ‘diamond overlap’ to work. Make sure there’s a most specific instance to catch the overlap:

instance {-# OVERLAPPING #-} LAct s x => LAct [s] [x] where
   lact s l = ...

And make sure all three instances (or four if you want LAct s x) are declared in the same module, so there’s no risk of the compiler picking a less-specific one because it can’t see the most-specific.

OTOH this is all pretty fragile, especially if you’re including instances for other constructors. And yes smells of a bandaid to what is not really the underlying requirement.

#5

An old C++ idea that used to be called “fat interfaces” (that term apparently means something different now) is to have abstract base classes (algebras) include optional operations, to limit the combinatorial explosion, and to reduce run-time conversions between nearly identical algebras. So for computer algebra, in my work in progress I define Group operations (==, op, ident, inv, etc.) in a single algebra type that can be used for a group, an abelian group, a monoid, or even a semigroup. There’s also a word of bit flags that say which operations/axioms are present/satisfied. I do the same thing for Ring operations (Abelian Group with times, one, division, etc.) in an algebra that can be used for a field, integral domain, commutative ring, noncommutative ring, etc., again with flags saying which axioms are satisfied. The flags are useful also for things like property-based testing, sometimes choosing a better algorithm (e.g. no zero-divisors lets one speed up multiplication of a scalar times a sparse vector or polynomial), etc. Also Pattern synonyms for the different kinds of algebras can help make this usable.

Note that I also generally use “explicit dictionary [algebra] passing”, because I believe that type classes are too rigid for complicated algebras that often need to be computed at run-time, especially in computer algebra. Also this handles the “multiple conformance” problem mentioned by @ApothecaLabs. GHC 9.4 added a withDict function to maybe help with explicit dictionary passing using type classes, but there are some issues. There’s also a shorter related discussion about the multiple conformance problem.

Type classes are great when you clearly don’t want to have to specify the dictionary/algebra at every call site, like + for various built-in number types, or a “programmable semicolon” for do blocks in a Monad. It’s harder to make them work for more complicated algebras, like polynomial rings modulo an ideal, or algebraic number fields, especially when the ideal or field extension is computed at run time.

2 Likes
#6

This is very interesting, thank you ! Somehow your calculi library manages to make work something pretty similar to the imaginary extension I suggested. Somehow I feel like the whole tag system you are using could be part of the language in order to enforce laws or properties without actually having to prove them like in LiquidHaskell.

What would be great is to be able to specify some laws, ask the programmer to ensure that the law holds (just like for the Monad type class), without having to prove it. But instead of having to use type classes, these laws could be linked to instances or even to variables.

#7

Your actions function is pretty neat !

The thing is, I’m using the LAct class in order to create semi direct products. And if I don’t enforce any laws, then the Semigroup and Monoid instances for the Semidirect product may not be associative. I just feel this would be wrong, even though it is pretty artificial to add “useless” type classes

#8

so here is an example using binary operation:

I really love your code. I feel it would be great if the Base library was constructed like this.

#9

Creating values of a type, that are part of some larger type but must fit some criteria, is best done through the use of smart constructors. For example, if you were modelling permutation groups as vectors of indices, you’d want to first make sure that your vector has all the right entries before calling it a permutation, so you’d write a newtype Permute n = MkPermute (Vector n Int) and a smart constructor permute :: Vector n Int -> Maybe (Permute n), that checks the law for the type. That’s why the commutative-groups package doesn’t really make sense: it’s a property of the types, not a property of the type class!

#10

it’s a property of the types, not a property of the type class!

That’s a good remark. I’ve been thinking of using types instead of type classes, with something like

newtype LActSg s x = MkSgLAct (Semigroup s => s -> x -> x)

newtype LActMnMorph s x = MkLActMnMorph ((Monoid s, Monoid x) => s -> x -> x)

But obviously the problem is that I lose polymorphism and this is not really usable in practice. I do believe the commutative-groups package exists exactly because of this.

#11

Recall that the word “is” is deceptively generic. In particular, it can mean either “is-really-a-kind-of” or “can-be-used-as-a-kind-of”. The former case is single inheritance, the latter is an interface. Interfaces are much more common than inheritance.

An an extreme example, a Victorinox Swiss Army knife “is-really-a-kind-of” knife which “can-be-used-as-a-kind-of” saw or tweezers or… if need be.

If I remember correctly, it was Aristotle who defined “man” as a “featherless biped”. Upon hearing this piece a wisdom, a sophist went to the market square, bought a chicken, plucked it bare of feathers, and proclaimed that to be a man…

1 Like