Monoids and Groups in F*

monoid.fst

// Andrew Miller - monoid.fst
// compiles under the school14.1 release of F* 
// https://github.com/FStarLang/FStar/releases/tag/school14.1

// This is an example of constructive algebra in F*. We're going to define the 
// class of mathematical objects called "monoids", and give several constructions,
// using F* to prove the constructions are sound.

// For similar developments in other languages, see:
// [Agda] http://people.inf.elte.hu/divip/AgdaTutorial/Application.Algebra.html
// [Coq] http://mattam.org/repos/coq/prelude/Monoid.v
// [OCaml] https://github.com/ghulette/ocaml-basics/blob/master/monoid.ml
// [Haskell] http://hackage.haskell.org/package/base-4.7.0.2/docs/Data-Monoid.html
// Note that in Agda and Coq, the laws are proven 

// Here's the mathematical definition of a monoid:
//  A "monoid" is an object consisting of a set of elements (called
//  its "carrier set") along with a binary operation defined over these elements.
//  The binary operation must be 'closed' over this set. Furthermore, the operation
//  must be associative. Finally, there must also be a distinguished element
//  that behaves like an identity.
//
// See https://en.wikipedia.org/wiki/Monoid for more!

module MonoidRaw
open List

// First, we'll just look at the "programming", leaving the laws implicit, as is done
// in languages without dependent types (e.g., Haskell). 

// This says that a monoid (over the carrier set 'a) consists of a binary operation
// 'mappend', as well as a distinguished element 'mempty'. The "laws" (which are part
// of the mathematical definition, but here are left as comments) state that the
// mempty element must behave like an 'identity', and mappend is associative.

type monoid_raw 'a =
  | MkMonoidRaw :
  mempty : 'a ->
  mappend : ('a -> 'a -> 'a)
  -> monoid_raw 'a
// -- Laws:
// identity: mappend mempty a == mappend a mempty == a
// associative: mappend a (mappend b c) == mappend (mappend a b) c

// abbreviations...
let mempty = MkMonoidRaw.mempty
let mappend = MkMonoidRaw.mappend


// In Haskell, this would be (and is) written as:
// class Monoid a where
//    mempty :: a
//    mappend :: a -> a -> a
//    -- Laws ....


// Here are some concrete examples of monoids, formed by familiar objects

// Example: the integers under addition form a monoid
val monoid_raw_int_plus : monoid_raw int
let monoid_raw_int_plus = MkMonoidRaw 0 (fun a b -> a + b)

// Example: the integers under multiplication *also* form a monoid
val monoid_raw_int_mul : monoid_raw int
let monoid_raw_int_mul = MkMonoidRaw 1 (fun a b -> a * b)

// Example: lists under concatenation form a monoid
// FIXME: this surprisingly fails with "List.append" not found
//val monoid_raw_list : monoid_raw (list 'a)
//let monoid_raw_list 'a = MkMonoidRaw [] (List.append)


// Here's the first "abstract construction", that builds a monoid from parts

// Example: given two monoids, their product (as a tuple) is a monoid
val monoid_raw_product : monoid_raw 'a -> monoid_raw 'b -> monoid_raw (Tuple2 'a 'b)
let monoid_raw_product a b =
  let bimap2 f g (a,b) (a',b') = (f a a', g b b') in
  MkMonoidRaw (mempty a, mempty b) (bimap2 (mappend a) (mappend b))


end // module MonoidRaw




module Monoid

// Now lets make a more thorough version of this interface, with laws included. This shows
// off the dependent types in F*, as well as the automated theorem proving.

// In this definition, monoid must be constructed from the identity element and binary
// operation, but must also carry around proofs that the laws are satisfied for the operation

type monoid 'a =
  | MkMonoid :
  mempty : 'a ->
  mappend : ('a -> 'a -> Tot 'a) ->
  monoid_id_left  : (a:'a -> Lemma (mappend mempty a == a)) ->
  monoid_id_right : (a:'a -> Lemma (mappend a mempty == a)) ->
  monoid_assoc : (a:'a -> b:'a -> c:'a -> Lemma (mappend a (mappend b c) == mappend (mappend a b) c)) ->
  monoid 'a

// abbreviations
let mempty = MkMonoid.mempty
let mappend = MkMonoid.mappend
let monoid_id_left = MkMonoid.monoid_id_left
let monoid_id_right = MkMonoid.monoid_id_right
let monoid_assoc = MkMonoid.monoid_assoc


// For the integers under addition example, F* discharges the laws automatically
val monoid_int_plus : monoid int
let monoid_int_plus = MkMonoid
    (0)
    (fun a b -> a + b)
    (function _ -> ())
    (function _ -> ())
    (fun a b c -> ())


// Same for multiplication, although we need a helper function
val mul_assoc : a:int -> b:int -> c:int -> Lemma (a * (b * c) == (a * b) * c)
let mul_assoc a b c = ()

val monoid_int_mul : monoid int
let monoid_int_mul = MkMonoid
    (1)
    (fun a b -> a * b)
    (function _ -> ())
    (function _ -> ())
    mul_assoc
    // alternative: (fun a b c -> ())   // FIXME somehow, this hangs


// For products, it's also straightforward to prove the laws
val monoid_product : monoid 'a -> monoid 'b -> Tot (monoid (Tuple2 'a 'b))
let monoid_product a b = MkMonoid
  (mempty a, mempty b)
  (fun (x,y) (x',y') -> (mappend a x x', mappend b y y'))
  (fun (x,y) -> monoid_id_left  a x; monoid_id_left  b y)
  (fun (x,y) -> monoid_id_right a x; monoid_id_right b y)
  (fun (x,x') (y,y') (z,z') -> monoid_assoc a x y z; monoid_assoc b x' y' z')


// As a follow-on: groups are monoids with an inverse for every element
module Group

type group 'a =
  | MkGroup :
  mon : (Monoid.monoid 'a) ->
  inv : ('a -> Tot 'a) ->
  inv_left  : (a:'a -> Lemma (mappend mon (inv a) a == mempty mon)) ->
  inv_right : (a:'a -> Lemma (mappend mon a (inv a) == mempty mon)) ->
  group 'a

// Example: integers under addition form a group
val group_int_plus : group int
let group_int_plus = MkGroup
  monoid_int_plus
  (fun x -> -x)
  (fun _ -> ())
  (fun _ -> ())
  
// Product groups
val group_product : group 'a -> group 'b -> Tot (group (Tuple2 'a 'b))
let group_product a b = MkGroup
  (monoid_product (MkGroup.mon a) (MkGroup.mon b))
  (fun (x,y) -> (MkGroup.inv a x, MkGroup.inv b y))
  (fun (x,y) -> MkGroup.inv_left  a x; MkGroup.inv_left  b y)
  (fun (x,y) -> MkGroup.inv_right a x; MkGroup.inv_right b y)