Now, one is not finished spelling out a monad when giving this collection of maps. One must also show that they satisfy certain constraints.
- T is functorial, meaning T g f = T(g) T(f)
- unit and mult are natural transformations, look up the meaning because unpacking it here would take to long
- mult( mult T ) = mult( T mult )
- mult( unit T ) = mult( T unit )
This set of constraints must go with the monad. This example provides a little more detail in terms of what binds a group of maps together, and hence of what might replace the notion of interface and explain what we see in practice. Good programmers invariably pick out just a few factorizations of possible interfaces -- from the giant sea of factorizations (read different ways to carve up the functionality). The reason -- i submit -- is because in their minds there are some constraints they know or at least intuit must hold -- but they have no good way at the language level to express those constraints. A really practical language should help the programmer by providing a way express and check the constraints that hold amongst the maps in an interface.
i submit that this idea is not the same as "design by contract". i am not proposing an Eiffel-like mechanism. Again, taking a functional approach to computation via category theory leads one towards modeling interfaces as categorical "situations" like monads, comonads, distribution laws, etc. This means that a large number of the constraints come down to
- functoriality
- naturality
- coherence
Language support for this approach might include keywords for these kinds of assertions. It is a gnarly beast to offer automatic and/or compiler support for checking general constraints. Even this limited family of constraints that i'm proposing can generate some very difficult computations, with very bad complexity. However, for those situations where a general purpose solution to check assertions of functoriality, naturality and coherence are infeasible, one can use these hints to generate tests to probe for possible failures. This idea follows the in the same spirit of replacing proof with proof-checking.
Of course, this is not the only way to go. i've yet to be convinced that category theory offers a good account of concurrency. Specifically, categorical composition does not line up well with concurrent composition. So, interfaces organized around types for concurrency is also something to consider. In this case, one might find a natural beginning in interfaces in which -- roughly speaking -- the methods constitute the tokens of a formal language the constructors of which are given by the types for concurrency paradigm.