Hello everyone! I’m excited to announce the first version of RequiredInterfaces.jl, a tiny package whose sole purpose is to give package authors the ability to declare the minimum required methods a type needs to implement to be able to hook into an interface, defined as an abstract type.
Please do check out the documentation and if you’re interested in “Why interfaces based on abstract types?”, check out the underlying philosophy that’s also part of the documentation (this also includes a “this is where we could go” section, in terms of interfaces, traits, etc).
For now, the package is mostly geared towards the “what methods users of an interface need to implement” part of defining an interface, as well as testing for minimal compliance with such an interface (i.e., are the required methods implemented in some capacity). Some of the future work/planned features include:
What are users guaranteed to get out of an interface in terms of callable methods?
I.e., the “what can I use?” counterpart to “what do I need to implement?”
More specific pre-/postconditions on such interface functions.
These are likely very far away, mostly because verifying that an implementation conforms to them is a hard problem.
Also, I want to particularly point out that this package is not intended as a general “formally specify & check all properties of an interface/type/thing”. While an admirable goal, I think that’s out of scope for the foreseeable future, at least in a manner that’s practical & accessible to a general programming audience. I do have ideas for that kind of stuff, but they’re not yet really ripe for discussion This package is more geared towards currently practical application.
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.
I’ve just released v0.1.4, with a number of new features, such as support for Type{T} in @required signatures and support for callable structs, as well as a number of bugfixes. Check out the full release notes here!
This package is more geared towards currently practical application.