In this article, I'll cover one approach to model an algebraic structure in F#. I'll make heavy use of features like generics and function types, which are distinctive features of F#. The specific example I'll focus on is how to model structures called groups. This will pave the way to do some even more impressive examples in subsequent articles, including sybolic programming in abstract groups, and generic computations in finite groups. I'll start by reviewing some of the math terminology and then walk through the F# implementation.
In abstract algebra, a group is a set equipped with an operation that satisfies certain properties. So before I can say what a group is, I want to define the words "set" and "operation."
A mathematical set is a collection of distinct entities called elements, where the order of the elements doesn't matter. That is, $\{1,2,3\}$ is a set of three elements. This is a nice order for the elements, but $\{3,1,2\}$ represents the same set. It's unusual to write a set with repeated elements, like $\{1,2,2,3\}$, but in this case we would still say it is equivalent to $\{1,2,3\}$ because we only care about distinct elements.
An operation on a set $S$ is a way of combining an ordered pair of elements of $S$ to produce a new element of $S$. I wrote a quick overview of some sets and operations in another article, and I've listed some of them in a table below for reference.
| Set | Symbol | # of elements | Operation | Example |
|---|---|---|---|---|
| Integers | $\mathbb{Z}$ | $\infty$ | Addition | 2+2=4 |
| $\{0,1,2,3,4,5,6\}$ | $\mathbb{Z}/7\mathbb{Z}$ | $7$ | Multiplication mod 7 | $6\cdot 6 \equiv 1 \pmod{7}$ |
| Real functions | $\mathbb{R}\rightarrow \mathbb{R}$ or $\mathbb{R}^\mathbb{R}$ | $\infty$ | Composition of functions | $\frac{1}{x} \circ \sin(x) = \frac{1}{\sin(x)}$ |
| Permutations of 3 objects | $S_3$ | $3! = 6$ | Composition of permutations | $[213]\circ[132] = [312]$ |
Of course, some of these sets have other operations as well.
In F#, you can think of a type 'T as a set, whose elements are all of the values of type 'T. An operation on the type 'T as a function of signature 'T * 'T -> 'T or equivalently 'T -> 'T -> 'T. For instance, the type int corresponds to the set of all int values in F#, and the (+) operation corresponds to the mathematical operation of addition on this set.
We'll often use a subset of the values of a given type, for instance the values 0, 1, 2, 3, and 4 with addition mod 5. In that particular example, the type system only guarantees that the result is an int, not that it is one of these five numbers, so we have to rely on our knowledge of how modular arithmetic works to know this is a valid operation.
Roughly speaking, a group is a set $G$ equipped with an operation that "behaves like" composition of invertible functions. Depending on the context, the operation on two elements $g$ and $h$ in $G$ is written $g\cdot h$, $gh$, $g\circ h$, or $g+h$. In general, I'll default to the notation $gh$ when making general statements about group operations, and sometimes I'll call it the "product of $g$ and $h$". Here are the specific rules the operation has to obey to turn the set $G$ into a group.
As examples, the first, second, and fourth rows in the table above are sets with operations that define groups. The third row is not, because not every real function $f(x)$ has an inverse $f^{-1}(x)$.
We can write an F# type to represent a finite group, meaning a group with finitely many elements. It's generic because a group could be a set of numbers, permuations, functions, matrices, or any other kind of object we want. The properties of the generic record list the things that we can do with any group.
type FiniteGroup<'T> =
{
// the elements of the set
Elements : 'T list
// the operation
Operation : 'T -> 'T -> 'T
// the special identity element
Identity : 'T
// for any element, identify its inverse
Invert : 'T -> 'T
}
Here's how to make a group out of the set $\{0;1;2\}$ with addition mod 3. The list of elements will be [0;1;2], which are the distinct integers mod 3. The operation will be addition mod 3, which I showed how to implement in an earlier article. Here I've included it as the Modular.add function. The identity element for addition mod 3 is zero, because $0 + n \equiv n \pmod{3}$. The inverse of an element $n$ is $-n$, since $n+(-n) \equiv 0 \pmod{3}$, but we need to find a representative for $-n$ among $0$, $1$, and $2$. For instance the inverse of $2$ is $-2$, and $1\equiv -2 \pmod{3}$, so we want our inverse function to return 1 as the inverse of 2. We can achieve that via Modular.subtract 3 0 n, which does $0-n$ in mod 3.
let integersMod3 : FiniteGroup = {
Elements = [0;1;2]
Operation = Modular.add 3
Identity = 0
Invert = Modular.subtract 3 0
}
As another example, we can build the group of permutations on 5 objects with the operation of composition of permutations (see here for some background). That group is called the symmetric group on 5 objects, and denoted $S_5$. Running the function Permutation.all 5 function in the source code, you can get all $5! = 120$ possible permutations of the array [|1;2;3;4;5|], which become our elements. The list of all arrays begins:
[[|1; 2; 3; 4; 5|]; [|1; 2; 3; 5; 4|]; [|1; 2; 4; 3; 5|];
[|1; 2; 4; 5; 3|]; [|1; 2; 5; 3; 4|]; [|1; 2; 5; 4; 3|];
[|1; 3; 2; 4; 5|]; [|1; 3; 2; 5; 4|]; [|1; 3; 4; 2; 5|];
[|1; 3; 4; 5; 2|]; [|1; 3; 5; 2; 4|]; [|1; 3; 5; 4; 2|];
...
The operation is composition of permutations, as computed by the Permutation.compose function. The identity element is the permutation [|1;2;3;4;5|] which represents keeping the five elements in their original order. We can find the inverse of any given permutation by searching for it, composing it with all of the permutations until we get the identity permutation back.
let invertPermutation (n:int) (p:Permutation) =
Permutation.all n
|> List.find (fun q -> Permutation.compose p q = [|1..n|])
More efficiently, we can get the inverse by finding the rearrangement of the given permutation to get back to [|1..n|]. This is the version of the function I named Permutation.invert
let invert n (p:Permutation) =
let indexOf p i = Array.findIndex ((=) i) p
[|1..n|]
|> Array.map (indexOf p >> (+) 1)With all of these functions implemented, we're ready to write down the definition of $S_5$.
let s5 = {
Elements = Permutation.all 5
Operation = Permutation.compose
Identity = [|1..5|]
Invert = Permutation.invert 5
}The integers with mod 3, denoted $\mathbb{Z}/3\mathbb{Z}$ as well as the permutations on five elements, $S_5$ are members of families of groups, indexed by whole numbers. Rather than hard-coding the numbers 3 and 5, we can make functions that generate $\mathbb{Z}/n\mathbb{Z}$ and $S_n$ for any value of $n$.
let integersModN n = {
Elements = [0..n-1]
Operation = Modular.add n
Identity = 0
Invert = Modular.subtract n 0
}
let symmetricGroup n = {
Elements = Permutation.all n
Operation = Permutation.compose
Identity = [|1..n|]
Invert = Permutation.invert n
}In the next articles, I'll show you many other groups that can be represented with the FiniteGroup type, but these two families of finite groups give some of the most important examples.
In F#, it's often our goal to design and name our types so that they can't represent invalid data. Unfortunately, the FiniteGroup type can represent a structure which is not a group. Here are some of the ways that it can fail:
Elements may not be closed under the Operation. That means that group.Operation g h isn't guaranteed by the type system to return a value in group.Elements.group.Operation (group.Operation g h) k may not agree with group.Operation g (group.Operation h k).group.Operation (group.Identity g) g may not return g.group.Operation (group.Invert g) g may not return the identity element.
My philosophy is to model the domain as closely as possible with types, and to use unit tests to cover cases where illegal states may still be representable. The specific kind of unit tests I'm talking about are property-based tests, which take some or all of the possible values and confirm that they obey certain properties. It turns out that each of the four above shortcomings can be checked with a property-based test. The nice thing about our FiniteGroup type is that we can write one set of generic tests, and they can be used to validate any group. Here are the tests:
// For all g,h test that gh is in grp.Elements
let testClosure<'T when 'T:equality> (grp:FiniteGroup<'T>) =
grp.Elements
|> List.forall (fun g ->
grp.Elements
|> List.forall (fun h ->
List.contains (grp.Operation g h) grp.Elements))
// for all g,h,k, test g(hk) = (gh)k
let testAssociative<'T when 'T:equality> (grp:FiniteGroup<'T>) =
grp.Elements |> List.forall (fun g ->
grp.Elements |> List.forall (fun h ->
grp.Elements |> List.forall (fun k ->
grp.Operation g (grp.Operation h k)
= grp.Operation (grp.Operation g h) k)))
// with identity e, test for all g that eg = ge = g
let testIdentity<'T when 'T:equality> (grp:FiniteGroup<'T>) =
grp.Elements
|> List.forall (fun g ->
grp.Operation grp.Identity g = g
&& grp.Operation g grp.Identity = g
)
// for any g, if h is the inverse of g then gh = hg = e
let testInvert<'T when 'T:equality> (grp:FiniteGroup<'T>) =
grp.Elements
|> List.forall (fun g ->
grp.Operation grp.Identity g = g
&& grp.Operation g grp.Identity = g
)This function runs all the tests at once:
let testGroup grp =
[testClosure; testAssociative; testIdentity; testInvert]
|> List.map (fun test -> test grp)Using these tests we can verify, for instance, that the group of permutations on four elements is indeed a group:
> testGroup (symmetricGroup 4);;
val it : bool list = [true; true; true; true]
I want to include a few more comments for readers that know a bit about category theory. We can think of the F# type system as a category $\textbf{Type}$ whose objects are F# types and whose morphisms are F# functions, i.e. $\hom(\texttt{'T},\texttt{'U})$ consists of functions of type 'T -> 'U. This category has finite products, where the product of type 'T and type 'U is 'T * 'U, and it has an terminal object unit.
From this perspective, our FiniteGroup type holds the data of a group object in the category $\textbf{Type}$. In a category with finite products and a terminal object, written "$1$"", a group object is an object $G$ with morphisms $\mu : G\times G \rightarrow G$, $\eta: 1 \rightarrow G$, and $\iota: G \rightarrow G$. These morphisms respectively represent the group operation, selecting an identity, and inverting an element, and they must make the following diagrams commute.
Our FiniteGroup type specifies an object 'T of $\textbf{Type}$, as well as morphisms Operation : 'T -> 'T -> 'T (for $\mu$), Invert : 'T -> 'T (for $\iota$), and Identity : 'T (for $\eta$). To more strictly adhere to the definition of group object, we could have given Identity the signature unit -> 'T, but that wouldn't have changed the implementation. Redrawn in $\textbf{Type}$, the diagrams look like this:
Our property-based tests were equivalent to checking the commutativity of these diagrams. When the elements coincide with all the values of the given type, closure of the operation is guaranteed, and the FiniteGroup value specifies a group object in $\textbf{type}$. For instance:
type Two = A | B
let twoGroup = {
Elements = [A;B]
Operation = fun x y ->
match x,y with
| A,A | B,B -> A
| A,B | B,A -> B
Identity = A
Invert = function A -> A | B -> B
}or as a "trivial" example:
let oneGroup : FiniteGroup = {
Elements = [()]
Operation = fun _ _ -> ()
Identity = ()
Invert = fun _ -> ()
}