/laws

Implementation and property-based verification of functional programming abstractions' laws

Primary LanguageScalaGNU General Public License v3.0GPL-3.0

This repository is ⚰️ ARCHIVED ⚰️

The last day of operation was on November 23, 2022


Laws

codecov License: GPL v3

Laws is a set of sample implementations of the fundamental functional programming abstractions, with the sole purpouse of showing the definition and the property-based verification of their algebraic structure's laws. They are implemented here as type classes for types of kind * and for higher order type operators of kind * -> * and, given the exemplificative nature of this work, they are strictly limited to the most basic, but still most important, ones. To notice that the implementations in this repository are not meant to be used in production code and, by no means, are intended as a state of the art in library design and modules composition. In more than one case, on the contrary, the semantic cohesion, the ease of understanding and the clarity, as reduction of boilerplate code, have been preferred to optimization and usability. For real life collections of production-ready functional programming abstractions, the suggestion is to have a look at libraries like Scalaz or Cats.

Code Structure

Currently the project includes the following structures

(*) No laws abided by

Each structure lives in its own Scala file called Module and every module provides

- the type definition
- a set of instances
- a syntax extension
- a definition of the laws using the syntax extensions
- a definition of the laws using the structure's primitives (for quick comparison)

An extra file with the supporting Algebra completes the project. The structure of the source code, as can be seen, is very linear and easy to navigate so, for further details, the best advise is to look into the the code itself.

Structures

Semigroup

A semigroup consists of a set A (type for us from now on) and a binary operation combine. A possible way to represent it in Scala is

trait Semigroup[A] {
  def combine: (A, A) => A
}

For the algebra (the type A and its operations) to be a valid semigroup combine has to abide by the associativity law for every a1, a2 and a3 in A

(a1: A, a2: A, a3: A) => (a1 <> a2) <> a3 == a1 <> (a2 <> a3)

Notice that the syntax extension allows us to use the more compact notation <> for combine. The right hand side of the expression above, in fact, is the actual body of the law definition in the code itself (see below)

trait SemigroupLaws[A] {

  implicit def F: Semigroup[A]

  def combineAssociativity(a1: A, a2: A, a3: A): Boolean =
    (a1 <> a2) <> a3 == a1 <> (a2 <> a3)
}

[ Code, Laws Check, Reference ]

Monoid

A monoid is a specialization of a semigroup. To be a monoid any semigroup needs to define also an identity element for the combine operation. With that we mean an element in the type A that, when combined with any other element in A trhough the combine operation, results in the other element itself. It can be called empty and a possible implementation is

trait Monoid[A] extends Semigroup[A] {
  val empty: A
}

where, as per its own definition, it has to satisfy the identity law for every a in A

(a: A) => (a <> empty) == a && (empty <> a) == a

Worth nothing that in the actual implementation of the law, we had to go through the implicit handle for the instance in use to access the Monoid[A] empty element. This is not present in the expression above just to keep the read more fluent. The real implementation of the law is in fact

sealed trait MonoidLaws[A] extends SemigroupLaws[A] {

  implicit def F: Monoid[A]

  def emptyIdentity(a: A): Boolean =
    (a <> F.empty) == a && (F.empty <> a) == a
}

[ Code, Laws Check, Reference ]

Covariant Functor (Functor)

A covariant functor or functor is an abstract data type that has the capability for its vaules to be mapped over. More specifically, given a functor fa it's possible to obtain another functor fb with the same structure as fa, through the application of a function f: a -> b to every element in fa. It's worth noting that this is the first type class we meet that abstracts over an higher order type operator (or type constructor) and not over a type. This is because functor is an abstraction for type constructor (in this case first order kinded types or types of kind * -> *) and not for regural types (or types of kind *). In Scala we can represent it as

trait Functor[F[_]] {
  def map[A, B]: F[A] => (A => B) => F[B]
    
  def lift[A, B]: (A => B) => F[A] => F[B] =
    f => fa => map(fa)(f)
}

Notice that another function lift[A, B] can be derived from map (lift is actually what's called fmap in Haskell). It better describes another capability that can be provided by a functor. It allows, in fact, to create a morphism from a function from A to B to a function from F[A] to F[B], that is the same as saying that it allows to lift a function on types to a function on type constructors F[_].

For an instance of Functor[F[_]] to be a valid functor, the map operation must preserve the identity morphism for every F[A] in A and the composition of morphisms for every F[A] in A and every f from A => B and g from B => C

(fa: F[A]) => (fa map identity[A]) == fa
(fa: F[A], f: A => B, g: B => C) => (fa map (g compose f)) == (fa map f map g)

[ Code, Laws Check, Reference ]

Contravariant Functor (Contravariant)

To understand what a contravariant functor is let's focus on the adaptive semantic of the functor clearly visible in its Function1 instance below.

implicit def functionFunctor[X]: Functor[X -> ?] =
  new Functor[X -> ?] {
    def map[A, B]: (X -> A) => (A => B) => (X -> B) =
      fa => f => Func(f compose fa)
  }

We can see that it allows to transform the output type inside the context Function1 composing an A => B to the function application fa.apply. Reasoning along the same line, we could argue that we might also want to adapt the input type of another Function1 where we fix the output and that can be defined as ? -> Y. In this case we cannot map the input type otherwise we wouldn't be able to apply the Function1 anymore. map clearly cannot do that. The types don't align. What we can do instead, is to prepend a morphism to Function1 that would give us exactly the type we need in input still remaining inside the context Function1. This is exactly what a contravariant functor is designed to do with its contramap. Let's have a look at a possible instance

implicit def functionContravariant[Y]: Contravariant[? -> Y] =
  new Contravariant[? -> Y] {
    def contramap[A, B]: (B -> Y) => (A => B) => (A -> Y) =
      fb => f => Func(fb compose f)
  }

The reader might observe that satisfying just this very specific need wouldn't be worth the troubles of an abstraction formalization and that's an absolutely reasonable objection. Contravariant functor actually doesn't work only in this particular scenario. On the contrary its peculiarity is that it generalizes this behavior and applies the adaptation to any other context that models a form of processing. That is the same as saying that we can have this feature for any higher order type operator for which we can define a contramap[A, B]. As an example, let's consider a Show[B] abstraction defined as

trait Show[B] {
  def show: B => String
}

that converts to string a type B. A contravariant functor for Show can adapt the show function to accept any other type in input as long as we can provide a morphism from this other type to B. It can do that because we implemented a valid contramap for Show that can generate a Show[A] given an A => B withiout even providing the implementation for show: A => String. All we have to do is use the contramap function like in the example below making sure all the types are in line.

val fb: Show[B] = Show[B]
val f: A => B = ???

// this gives us a working instance of Show[A] fully implemented
val fa: Show[A] = fb contramap f

val anA: A = ???
fa.show(anA) // Works fine

The contravariant functor type class can be defined as

trait Contravariant[F[_]] {
  def contramap[A, B]: F[B] => (A => B) => F[A]
  
  def lift[A, B]: (A => B) => F[B] => F[A] =
    f => fb => contramap(fb)(f)
}

A valid instance of this type class needs to abide by the following laws (that are actually dual to the functor's laws)

(fa: F[A]) => (fa contramap identity[A]) == fa
(fc: F[C], f: A => B, g: B => C) => (fc contramap (g compose f)) == (fc contramap g contramap f)

Observe that also contravariant functor provides a function lift[A, B] (that's actually what's called contramap in Haskell). It can be simply seen, like in the case of functor, as a way to lift a function into a context, but in an inverted way.

[ Code, Laws Check, Reference ]

Invariant Functor (Invariant)

Cartesian

Applicative Functor (Applicative)

Monad