I was chatting with someone about Interfaces/Type-classes and how in their language of choice you do not get default functions. It reminded me of a little implementation trick I used in my thesis to hot swap model implementations in an evaluator I wrote.
I will show this trick using the dependently typed language Idris but make not that I don’t see any real reason why this cannot be achieved in a language that supports polymorphism and indexed data types.
The core idea of this trick is to realise that within Idris Interfaces are realised as algebraic data types.
We can show this by approximating the Num interface with the following record:
and an implementation that instantiates the fields with implementations for Nat
We can now start to write functions that use this ‘interface’, and where we would have an interface constraint we now explicitly pass around an implementation.
Now with this setup we can also provide default functions.
Here is an approximation for the Eq interface:
We can construct factories to then build the default implementations for methods if they are provided.
Here we now construct an instance of MyEq for Nats.
First we define equality.
Then we can build an implementation that uses a ‘default’ implementation.
and one that does not.
As a final thought, what about implementing default implementations in terms of the ‘interface’ itself. For that I would suggest removing those functions as fields and write functions that use the ‘interface’.
PS
The reason records are not highlighted nicely is due to issues with Idris’ highlighting code for records.