[ANN] RequiredInterfaces.jl

As @Keno mentioned on slack some time ago, InterfaceSpecs.jl is an experimental try at defining a common ground interface for writing formal specifications of source code, to be later checked with various (potentially SAT or SMT) solvers. In contrast, RequiredInterfaces.jl doesn’t have that big a goal - the philosophy is that all this kind of information really ought to be represented by a type, and abstract types (which aren’t really more than a name) are a perfect fit for that already (modulo the fact that we can only explicitly subtype one abstract type). It should pretty much always be possible to add onto this with more formal specifications later on, but from my POV, we’re missing the first step of making “what is required to be implemented” possible, before we can start to talk about whether such implementations are correct in a deeper, semantic sense.

Interfaces.jl has a similar POV, except that it also extends the notion of a required method of an interface with optional methods - this is something I decidedly don’t want; the purpose of an (interface) type is to provide guarantees that a given set of methods exists and can be called without fear of a runtime MethodError. So any “optional” method of an interface really ought to be an interface of its own, extending the parent interface by that method, so that users who want to communicate that they require that method are able to do so. This again is a natural extension of abstract types - a type implementing a subinterface must already dispatch just the same as a type implenting the parent interface. Additionally, you’re free to use any type parameters you want in your interfaces, and impose any conditions on them you require - it’s all the same to RequiredInterfaces.jl, because it acknowledges that in Julia, abstract types are interfaces with all constraints and requirements being implicit and stem from the methods actually required to implement the interface.

My personal need for this package (and why I’ve written my own instead of using the existing ones) stems from the (upcoming) PropCheck.jl (EDIT: PropCheck.jl has been released now - check out the announcement here!) - I wanted to communicate which method signatures are required for people to implement in order to hook into its API, which is something the existing solutions just don’t capture. It’s good to be able to specify properties that should hold on an interface, but we really ought to put as many guarantees as possible into types, and use those as existing guarantees/requirements.

15 Likes