Why you should care about equality in type dependent languages
Last fall I reviewed the first five chapter of the book TypeDriven Development with Idris with Idris by Edwin Brady.
Dependent types can be used for (at least) two purposes:
 Add additional information to types, e.g. the length of a vector. The compiler can then type check (at compile type) that operations on a vectors that requires vectors of the same length actually has the same length
 programming with dependent types can be used to “prove theorems”
The first part of TypeDriven Development with Idris focuses on the first aspect and I discussed this is my first review of the book. Now additional material has been released for reviewing and here I want to focus on chapter 8 dealing with Equality.
Recap
Idris is not the only programming language with support for dependent types. I recently learned about F* (pronounced F star) by Microsoft Research. The type system of F* supports dependent types. In my previous post I gave an example of a Money type dependent on time. Let me revise that example to use F. This will serve both as reminder about dependent types and show an alternative but similar approach from F.
F* does not have a native Date
data type. For the sake of the example we will just model time as a int
representing a timeline. One way of defining a Money
type indexed over time (here represented by a int
) could be
An instance of a money type can be instantiated with the Amount
constructor
Similar to the Idris example we can write an add
function that only type check when we add money
types with the same time value:
If we define two additional money
types:
then let res1 = add m1 m2
will type check but let res2 = add m1 m3
will not.
Equality
I consider my native programming language to be C#. I have been programming C# since 2003 but the topic of equality in C# still pops up from time to time. You have to distinguish between reference and value types when comparing things. And when you want to implement IEquatable<'T>
or IComparable<'T>
there is quite a few thinks to remember. If you are into DDD then equality means something different for aggregates and value objects. Eventually you might get it right but there are lots of places where you can get it wrong. Even if you did read “Item 6: Understand the Relationships Among the Many Different Concepts of Equality” in the excellent book Effective C# by Bill Wagner.
The F# structural equality approach seems much easier to work from an application developer point of view. Comparing maps, set, and tuples just works out of the box. But even in F# equality is a lengthy topic.
but in the end does it matter if you made an programming error
The C# interface IEquatable<T>
contains just one method:
where other
is of type T
is an object to compare with this object. According to the documentation the method returns a System.Boolean
that is
true if the current object is equal to the other parameter; otherwise, false.
However, this is an implementation detail. One cannot tell if you get the expected result just by looking at the type definition of Equals
. An implementation of Equals
that always returns true
fulfills all the requirements but it will give you unexpected results when comparing objects.
Can we do better than above? The answer is yes but it requires a programming language that supports dependent types. In Idris the natural numbers are defined by the Nat
type. Let us consider the dependent type
from chapter 8 in TypeDriven Development with Idris. This type is parameterized by the numbers num1
and num2
but if we have a value of type Eqnat
then num1
and num2
must be equal because the only constructor Same
for EqNat
requires num1
and num2
to be equal for the type to be constructed. I assume that it is no coincidence that this resembles one of the mathematical properties of equality, namely reflexivity: a = a
 an object is identical to itself.
The above dependent type definition for EqNat
is also referred to as propositional equality sine any to values num1
and num2
can be proposed to be identical.
Conclusion
TypeDriven Development with Idris is an excellent introduction not only to typedriven development but also to type theory^{1} . Usually the term page turner is used for fiction but I consider the term to be applicable to this book as well.
Type dependent languages might still not be applicable to enterprise software. But from a practical point of view you should still care about languages like Idris because eventually the might end up with a type system with more precise types. As a application developer that is a desirable situation. Quoting Jane Street’s Yaron Minsky we should strive to Make illegal states unrepresentable.” and that is definitely easier with a more expressive type system. Imagine the day where an array comes with extra information about the size of the array and say hello to static checks for out of bounds exceptions.
Footnotes

I recommend the essay Against a universal definition of ‘type’ by Tomas Petricek for a general scientic discussion about what types are. ↩
Please send messages and comments to my twitter account Twitter.
Edit page on GitHub. Please help me to improve the blog by fixing mistakes on GitHub. This link will take you directly to this page in our GitHub repository.
There are more posts on the front page.
Content of this blog by Carsten Jørgensen is licensed under a Creative Commons Attribution 4.0 International License.