Why are Witchcraft’s “(semi-)principled type classes” a big deal
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 aFunctor
is an implementation offmap
with the proper type. Any sensibleFunctor
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 ofreturn
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:
1. Type class definition
Defined in the Witchcraft repo in lib/witchcraft/monoid.ex
, its outline is this:
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 definst
ed 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.Generator
protocol. 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’sData.Functor
or Haskell’sData.Functor
for instance.
..
Algebraic structure must also satisfy properties/laws:
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.