In this post we will consider the interplay between dependently typed data structures and interfaces.
This post is a literate Idris file so there will be some cruft related to Idris that will remain until I get round to 1 improving Idris’ literate mode support.
First we need to hide a few things from the default…
%hide List %default total
Consider the following interface that defines equality for a provided type:
interface Equals (type : Type) where eq : (a,b : type) -> Bool notEq : (a,b : type) -> Bool notEq a b = not (eq a b)
At first glance there is nothing surprising about its definition. For example, let us look at the definition of equality for a simple cons-list data type.
Here is the data type:
data List : (type : Type) -> Type where Empty : List type Extend : (value : type) -> (rest : List type) -> List type %name ConsList.List rest, restA, restB
Here is the implementation:
listEq : Equals type => (a,b : List type) -> Bool listEq Empty Empty = True listEq Empty (Extend value rest) = False listEq (Extend value rest) Empty = False listEq (Extend value rest) (Extend x restA) with (eq value x) listEq (Extend value rest) (Extend x restA) | False = False listEq (Extend value rest) (Extend x restA) | True = listEq rest restA
Which we can provide for an
Equals type => Equals (List type) where eq = listEq
Let us now consider ’lists with length’, otherwise known as: Vectors.
Here is the data type:
data Vect : (size : Nat) -> (type : Type) -> Type where Empty : Vect Z type Extend : (value : type) -> (rest : Vect curr type) -> Vect (S curr) type %name SizedList.Vect rest, restA, restB
Here is an implementation:
vectEq : Equals type => (a,b : Vect size type) -> Bool vectEq Empty Empty = True vectEq (Extend value rest) (Extend x restA) with (eq value x) vectEq (Extend value rest) (Extend x restA) | False = False vectEq (Extend value rest) (Extend x restA) | True = vectEq rest restA
Which we can provide an
Equals instance for:
Equals type => Equals (Vect n type) where eq = vectEq
Notice that in the type signature for
vectEq, and our
Equals, implementation we have assumed that the compared vectors are of the same length.
We see this with the short hand:
(a,b:...) in our type signatures.
When we compare vectors, however, it might be the case that they are potentially the different sizes, and potentially that they might be the same size.
We need a better implementation.
So let us write one:
namespace Proper vectEq : Equals type => (a : Vect sizeA type) -> (b : Vect sizeB type) -> Bool vectEq Empty Empty = True vectEq Empty (Extend value rest) = False vectEq (Extend value rest) Empty = False vectEq (Extend value rest) (Extend x restA) with (eq value x) vectEq (Extend value rest) (Extend x restA) | False = False vectEq (Extend value rest) (Extend x restA) | True = Proper.vectEq rest restA
Now constructing an
Equals instance will not result in a type error.
[alt] Equals type => Equals (Vect size type) where eq a b = Proper.vectEq a b
When we call
eq it will only work with vectors that are the same length.
This is the definition of
Equals: given two values of the same type.
To access the correct implementation we need to call
Proper.vectEq explicitly, or really just
The question is to me is:
Given this one obvious limitations of Interfaces in a dependently typed setting are they useful at all for dependently typed programming.
In all my years playing with Idris, Interfaces are handy in a few settings:
- Providing an API to work with structures work on similar data. i.e.
- when defining operations on single instances of values i.e.
- when composing programs based on the above:
However, when I write my Idris libraries and Idris programs I find that interfaces are not always the best thing to use. In fact I shy away from using interfaces unless absolutly necessary.
I think there is a class of interface (of which
Equals is a prime example,
DecEq another) where we may need to think a little on their use in a dependently typed setting.
But maybe we need:
namespace TheFuture interface DEquals (ty : idx -> Type) where eq : ty a -> ty b -> Bool notEq : ty a -> ty b -> Bool notEq a b = not (eq a b)
But how do we then shoe horn
Vect into this…
DEquals (Vect size type) where will not type check.
We would have to rewrite the type of
Vect to be
Vect : Type -> Nat -> Type for it to work, but this itself will cause interfaces such as
Functor to no longer work…
Idris’ support for namespaces alleviates the need for interfaces as it allows one to present similar named constructs and distinguish between them. But how to ensure that we have consistent names across our code base…
Do we need to rethink interfaces in a dependently typed setting?
The short answer is: I do not know.
I haven’t performed a literature review of what the other team are doing or what the other PL people think about it.
Maybe having modules as first class constructs might help, or maybe Idris’ support syntactic overloading is intriguing. By that I mean if you provide implementations for certain operators you get Do-notation and List-notation for free. I do not mean DSL notation or ‘syntax’ notation that allows one to produce horrible mix fix unicode abominations that are hard to read.
I might be wrong here, and I am sure several people I know, and many I don’t know, will correct me. But if it was a solved issue, it would have been addressed in Idris2.
By round too I mean I have been planning on doing it for half a decade or there about… ↩︎