Why are Witchcraft’s “(semi-)principled type classes” a big deal

Published in

Scientific breakthrough of the afternoon

6 min readMar 15, 2019

The Witchcraft library, providing “common algebraic and categorical abstractions to Elixir” (such as monoids, functors, monads, etc.), is built atop the TypeClass package, which turns the notion of principled type classes into reality. (Highly recommend reading the library README.)

As far as I can tell, the term “principled type classes” has been coined by John A. De Goes, in his post titled Haskell’s Type Classes: We Can Do Better.¹

Type class laws (or properties) are usually not enforced

When I started learning Haskell and PureScript, everything seemed alien (still does), but I love the reasoning behind the structure of these languages. In the beginning, the gist for me was that in order to use type classes for a specific type, their required functions have to be implemented, and that’s it.

But that is not it, as instances would have to also satisfy type class laws²; otherwise the entire notion of type classes are for nothing³. They are noted in the documentations, but (a) I am easily intimidated by math and (b) took it as a given, that (magically) happens when providing a type class instance, when this is not the case.

As it turns out, this fact is noted in many places:

Implicitly, in the Haskell Typeclassopedia’s “Laws” section:
“As far as the Haskell language itself is concerned, the only requirement to be a Functor is an implementation of fmap with the proper type. Any sensible Functor instance, however, will also satisfy the functor laws, which are part of the definition of a mathematical functor.”
Why do all Haskell typeclasses have laws? question on Stackoverflow
Michael Vanier’s Yet Another Tutorial Series Part 3: (emphases mine)
“However, there is a catch: Haskell does not enforce the monad laws! The only thing Haskell cares about is that the definitions of return and >>= for a particular monad have the correct types. Whether they also obey the monad laws or not is up to the programmer.
Many people have thus asked “Why can’t Haskell enforce the monad laws?” And the answer is simple: Haskell isn’t powerful enough! To get a programming language and environment powerful enough to allow you to state and enforce monad laws from within the language, you would need to have something like a theorem prover.”
or the post mentioned in the beginning: Haskell’s Type Classes: We Can Do Better

Witchcraft’s type class laws are enforced by property-based testing

As John notes, “For non-dependently-typed languages, QuickCheck-style property verification is probably sufficient”, and this is exactly the route Brooklyn Zelenka (creator of TypeClass, Withcraft, Quark and Algae) took, but also provided the @force_type_class true and @force_type_instance true escape hatches [v], to be able to use type classes the “unprincipled” way.

Her Elixir.LDN 2017 talk, Witchcraft: Monads for the Working Alchemist, is a must see. I often use the talk slides as quick reference.

Example: `Witchcraft.Monoid`

Chose Monoid because it depends on Semigroup and needs to conform to multiple properties/laws/conditions.⁴

For reference:

Witchcraft 1.0 type class hierarchy (copied from talk slides)

1. Type class definition

Defined in the Witchcraft repo in lib/witchcraft/monoid.ex , its outline is this:

Definition of the Witchcraft.Monoid type class

Following the TypeClass documentation, a type class is composed of dependencies, a protocol, and properties.

1.1 Dependencies

They are marked with the extend/1 macro, and only immediate parents in the chain need to be specified, “as those type classes will have performed all of the checks required for their parents.”

Or put it another way, from extend/1 documentation: “Set a type class dependency. ie: another type class that need to be definsted before this one.”

extend/1 is optional. See Semigroup for example, as it has no dependencies.

1.2 A protocol

Functions, that must be implemented by every type class instance, can be specified using the where/1 macro. In the case of Monoid, it is an empty/1 function.

where/1 is optional. For example, theMonad type class only has properties, and has no other requirements for instances.

“defclass Foo generates a Foo.Proto submodule that holds all of the functions to be implemented”. The Foo.Proto submodule is a regular Elixir protocol⁵, and it will be automatically implemented when using definst/2,3 to define type class instances.

At this point, Witchcraft.Monoid.Proto exists with an empty/1 specification.

1.3 Properties [v]

Properties/laws are defined via the properties/1 macro and the class’ property functions use the required functions (defined in thewhere/1 block, see 1.2 above) to ensure that the laws hold.

properties/1 is not optional, because type classes need to have at least one law. (See ³.)

The property function declared will be used by the property checker by random input from property generators of types that have an instance for the given type class. From TypeClass' documentation:

All custom structs need to implement the TypeClass.Property.Generator protocol. This is called automatically by the prop checker. Base types have been implemented by this library.

And this is where the “principled” attribute in the title comes in. Section 2. walks through specific examples from the Witchcraft library.

It is important to note that properties/1 wraps the property functions in a Property submodule, so in the case of Monoid, the end result is:

iex(1)> Witchcraft.Monoid.Property.left_identity([])
trueiex(2)> Witchcraft.Monoid.Property.right_identity("")
true

2. The property checking of type classes

The implementation ofFunction's monoid instance:

definst Witchcraft.Monoid, for: Function do
  def empty(sample) when is_function(sample), do: &Quark.id/1
end

The property checker is called at compile time, when an instance is defined with definst/2,3 below. It is basically a wrapper around Elixir’s defimpl/2 with some compile time checks for the escape hatches [^].

At this point,

datatype  == Function
class     == Witchcraft.Monoid

run!/4 is called twice, because the Monoid class has two properties: left_identity/1 and right_identity/1 , that are defined in Witchcraft.Monoid.Property. [^]

Once execution gets to run!/4, it means that the data type, that one wants to implement the type class for, has to have an implementation for the TypeClass.Property.Generatorprotocol. More on generators (TypeClass.property.Generator implementations per data type) and custom generators in a later post [TODO: add post and link here].

Function, the data type here, already has an implementation in TypeClass library:

# lib/type_class/property/generator.exdefimpl TypeClass.Property.Generator, for: Function do  def generate(_) do
    Enum.random([
      &inspect/1,
      &is_number/1,
      fn id -> id end
    ])
  end
end

That is, data_generator's value in run/4 is irrelevant in this case then, because:

data_generator = TypeClass.Property.Generator.Function.generate(nil)    
#=> &:erlang.is_number/1

but

apply(property_module, prop_name, [data_generator])
==
Witchcraft.Monoid.Property.left_identity(&:erlang.is_number/1)

which turns to

Therefore type class properties have to return “truthy” values in order for a data type to be deemed conforming.

(Looking at generator implementations in Witchcraft or in Algae it seems that the input is always ignored, but don’t let that fool anyone: it is needed when custom generators come in the picture.)

[^] The article mentions that principled type classes can be implemented in Idris (because it is also a theorem prover), but just want to note here that this is also a work in progress in PureScript. See issue 110 and pull requests 111 and 197.
[^] Type classes represent abstractions from category theory or algebraic structures (that can be perceived as categories in category theory).
.
For example, according to the functor definition, two condition must hold: “functors must preserve identity morphisms and composition of morphisms.”
These are always noted in the documentation, see PureScript’s Data.Functor or Haskell’s Data.Functor for instance.
..
Algebraic structure must also satisfy properties/laws:

From https://en.wikipedia.org/wiki/Category_(mathematics)

3. [^] From John A De Goes post, “If you can’t define laws for a type class, then it’s not useful as an abstraction, and you should not try to define a type class. Instead, just write lawless functions and pass them around (or think harder about those laws!).”

Harry Garrood’s post, “Down with Show! Part 1: Rules of thumb for when to use a type class” is a very in-depth treatment of the topic and a treasure trove of information. (Spoiler: one of the sub headings is “Have at least one law”.)

This Twitter thread is also relevant.

4. [^] “Category theorists sometimes look with scorn on semigroups, because unlike a monoid, a semigroup is not an example of a category.” (from nLab)
The Stackoverflow question Viewing Semigroups as Categories? is also relevant.

5. [^]
defclass source: https://github.com/expede/type_class/blob/master/lib/type_class.ex#L129

where/1 implementation registers all required functions in a module attribute, and defclass will call run_where!/0 that takes care of defining the type_class.Proto protocol.