Group Theory in Haskell

There are two major motivations for group theory. The first comes from geometry. The geometer Felix Klein tried to find the essence of Euclidean geometry. His answer was that geometry is essentially about transformations of the plane that preserve distance. Another way to express this:

When a geometer makes a proof that triangle \(ABC\) is congruent to triangle \(DEF\) what they are saying is that there exists some transformation of the plane \({\color{red} f : \mathbb{R}^2 \to \mathbb{R}^2}\), so that \(f(ABC) = DEF\). The distance-preserving property could be expressed precisely as \(d(p,q) = d(f(p),f(q))\).

When you consider the set of all such transformations of the plane, you get a structured object called a group. These objects are worthy of study on their own because they show up in many other seemingly unrelated contexts. Like algebra.

Another major motivation for studying groups came from algebra. A young frenchman named Évariste Galois was studying algebra, particularly the existence of solutions to polynomial equations, like:

\[x^3 + 6x^2 + 11x - 20 = 0\]

He developed a theory of how to transform the "zeros" of the polynomial equations, and these also form a group, like Klein's geometric transformations. Galois worked out a theory for why some equations (like quadratics and cubics) have general solutions, and why others don't. The Galois group is central to that theory.

So the idea of a group arises in both algebra and geometry. It shows up in physics too, it's one of those fundamental ideas whose time came in the 19th century. The study of groups is considered the first form of "Modern Algebra". Groups are essential to understanding symmetry, and symmetry is essential to understanding the physical world. The Standard Model of Particle Physics is a glorified study of one particular group: \(U(1) \times U(2) \times SU(3)\), and the application of that one group is… all the forces and fields in the universe except gravity. What's extraordinary is how we can start studying groups here on paper and in a Haskell REPL.

In Haskell, a type g is an instance of a Group if it's a Monoid with an invert function:

class Monoid g => Group g where
  invert :: m -> m

Such that

a <> (invert a) == (invert a) <> a == mempty 

mempty is the Monoid unit, it's the \(e\) in the mathmetical definition above.

The notation used for the inverse of a group element is the superscript -1, so \(a * a^{-1} = e\) means that \(a^{-1}\) is the inverse of \(a\).

Another convention used is to drop the infix \(*\) and just use multiplication notation, so \(aa^{-1}=a^{-1}a=e\)

Function types have an instance of Monoid typeclass which proves that function composition is associative.

instance Monoid m => Monoid (r -> m) where
  mempty _ = mempty
  f `mappend` g = \x -> f x `mappend` g x

Exercise: Check that this Haskell code compiles.

There are two special notations for permutations. We defined \(\text{Sym}(X)\) using functions with inverses, but since we are thinking about these functions as objects in themselves, let's introduce a special syntax.

Since Monoid is so central to Haskell code, it's easy to work with Groups, since they are just Monoids with an inverse function (see 2.1). In Haskell, the analog of a set is a type. So taking our set \(X = \{0,1,2\}\), the statement \(1 \in X\) is expressed as 1 :: X in Haskell. The elements of a set are analogous to the inhabitants of a type. In the example below, we define a type X with three inhabitants.

1. Define the group \(S_3\)
2. Let \(g_1, ..., g_n \in G\) where \(G\) is a group, prove that \[(g_1g_2...g_n)^{-1} = (g_n^{-1}g_{n-1}^{-1}...g_2^{-1}g_1^{-1})\]

I wrote this document in org-mode in Emacs. I export the org file to html to generate the website, and then I run org-babel-tangle to produce the Haskell code. To speed up the workflow I made the function below and then bound it to <F5>

(defun org-babel-tangle-and-compile-perms ()
  "Tangle and compile perms.hs"
  (interactive)
  (progn
    (org-babel-tangle)
    (compile "/opt/homebrew/bin/stack exec -- ghc perms.hs")))

./perms.hs is a literate program that this org-mode document produces. Supporting code to make the file compile and run is defined down here in the appendix.

{-# LANGUAGE FlexibleInstances #-}
module Main where

import Data.Group.Permutation
import Data.List

data X = Zero | One | Two deriving (Enum, Eq, Show)

-- pmatrix notation
pmn :: Permutation X -> String
pmn p = "\\begin{pmatrix}" ++
  (concat $ intersperse " & " $ map show xs) ++ "\\\\" ++
  (concat $ intersperse " & " $ map (show . to) xs) ++ "\\end{pmatrix}"
  where (to, _) = pairwise p
        xs = [Zero, One, Two]

-- show permutations in the notation above
instance Show (Permutation X) where
  show p = pmn p
    where (to, _) = pairwise p

-- Defining the elements of S₃
s0 = permute id id          -- identity permutation
s1 = permute zo zo where  -- transpose Zero/One
  zo = (\x -> case x of
                Zero -> One
                One -> Zero
                Two -> Two)

main :: IO ()
main = do
  print s1