I Can See Right through You

I've been doing some reading and thinking about contracts and hybrid type checking, and there's something I haven't seen mentioned yet.

Those of us who use languages with decent support for abstraction are used to thinking of operations that can have different implementations—depending, for example, on the particular class associated with an object.

But there are some operations for which multiple implementations don't really make sense. For example, consider an interface for integers that supports even and odd operations. In a language with nominal typing, you can't get very specific about what these methods return:

  trait Integer {
    def isOdd: Boolean
    def isEven: Boolean
  }

But in a language where your contracts can be more specific, you could say something like:

  trait Integer {
    def isOdd: { _ % 2 == 1 }
    def isEven: { _ % 2 == 0 }
  }

That is, the contract of odd specifies that it returns whether its argument is odd, and similarly for even.

Assuming that you don't mind putting code in your interface, you can make sure that no override of these methods violates the contract by insisting on the implementation:

  trait Integer {
    final def isOdd: { _ % 2 == 1 } = this % 2 == 1
    final def isEven: { _ % 2 == 0 } = this % 2 == 0
  }

Holy redundancy, Batman! The type is the implementation! In fact, if these are pure functions, the types specify the only reasonable implementation of these operations (modulo optimizations, such as using a shift instead of a division operation).

If, like me, you tend to assume that everything you encounter is just a special case of some more general phenomenon, you might want to give this sort of function a name. I'm inclined to use the word transparent, because the function's type acts like a window that lets you see the whole inside of the function—although I'm not sure that term wouldn't lead to confusion with referential transparency, which is something else.

But if this phenomenon is indeed sufficiently common to receive a name, you might want to support it directly in a programming language, with something like:

  trait Integer {
    def isOdd transparently this % 2 == 1
    def isEven transparently this % 2 == 0
  }

On a related note, if a contract is a function, then that function might have a sort of transparency—that is, a reflection facility that let you inspect a contract might not just let you test whether the contract holds of a particular value, but also let you look directly at the code that specifies the contract. An alternative is to hide the contents of the contract, and reveal only whether one contract implies another; but since that is impossible to deduce in general, the reflection system would probably serve you better by giving you the raw code and letting you make of it what you will.