Why you should care about equality in type dependent languages
Last fall I reviewed the first five chapter of the book Type-Driven 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 Type-Driven 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.
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
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
let res1 = add m1 m2 will type check but
let res2 = add m1 m3 will not.
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
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:
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 Type-Driven Development with Idris. This type is parameterized by the numbers
num2 but if we have a value of type
num2 must be equal because the only constructor
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
num2 can be proposed to be identical.
Type-Driven Development with Idris is an excellent introduction not only to type-driven development but also to type theory1 . 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.
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.