I have been skeptical of the notion of "interface" lately.
First of all, there is comment from Erik Meijer who said something like "interface without laws is useless" (he was referring to "interface" as a concept in OOP languages, and by "laws" he meant some algebraic laws). Basically what he wanted to know was the algebra, not just interface.
And if you look at it from Curry-Howard correspondence perspective, where programs are proofs and types are theorems, then basically, since type is an interface, you could say that theorems are interfaces in mathematics. So there already is a very precise notion of what is interface.
On the other hand, I also kinda like the notion of DSL as an interface, as described in the recent article here on HN: http://degoes.net/articles/modern-fp/
What seems to be the main contention here - should the interface just use the names (akin to philosophical nominalism) and leave them open to interpretation or should it somehow encode the properties of things it describes (akin to philosophical realism)?
Indeed, this quickly becomes obvious after writing Haskell for awhile. Lawless typeclasses just seem clunky and get less reuse compared to their lawyer'd up brethren.
You also can get a very slight taste of this in C#, Java, etc as well where larger interfaces seem clunky and get less reuse than smaller interfaces. In C#, if an interface has some nice properties, typically the extension methods on these interfaces with allow for a combinational explosion of generic utility functions. So this might be one way to judge the "algebraicness" of interfaces. You see this a lot of the LINQ collections libraries, which seem to have put some thought into laws.
Unfortunately in these languages you can only go so far due to the lack of higher kinded polymorphism (T<A> types vs just Type<A> types).
One thing that baffles me a little bit about LINQ in .NET is that it's got a dual identity.
On one hand you've got the IEnumerable<T> interface, which supports the fluent syntax and is extremely easy to riff on with extension methods. (The "fluent syntax" itself is just a bunch of extension methods.)
On the other hand you've got the mechanisms you need to support the query syntax, which behave more like duck typing. If you implement a couple methods with certain names and signatures, not all of which are formalized by an interface, then the compiler will let you use query syntax with objects of that type. It also turns out that the stuff you need to implement are roughly the bind and return operations from a monad. . . but not exactly. In particular, the element they use in place of bind is a bit more complicated, and not in a way that adds any real expressive power. It just makes the signature a bit more irritating to support.
In other news, re: lack of higher kinded polymorphism - That's something that the maintainers of F# have forcefully resisted adding to the language. The argument, which I've yet to take the time to look into deeply, is that typeclasses interact poorly with formal interfaces so you shouldn't allow a language to have both. I'm a bit skepty on that one, though, since I'd assume there would be wailing coming from the Scala community if it were really that bad.
Maybe, but I'm inclined to guess that it could probably be made workable without much more pain than what it takes to interact with F#'s curried functions from C#.
Usually the recommended approach for making F# code usable from C# is to add an object-oriented wrapper layer to the F# library. That ends up being much, much easier in practice than trying to deal with F# code on its own terms from C#.
Abstract types have existential type. ML/Coq modules are just existentially-typed "package" data. Haskell type-classes are just another variation on the same concept, with only one instantiation of the type-class allowed at each internal type so the compiler can search for instances coherently.
Which reminds me, I should finish reading Tomer Ullman's PhD thesis to see if he managed to integrate existential types into his theory of causal-role concepts and theory formation.
I somehow wanted to say that. Interface are only the surface of an algebra. Having an iterator interface doesn't mean a lot, but when you study linearly recursive structures you somehow understand the car / cdr, next / hasNext relationship. Otherwise it looks very awkward and shallow.
That said, even without this, Interfaces forces to think toward minimal assumptions which is a very important property.
First of all, there is comment from Erik Meijer who said something like "interface without laws is useless" (he was referring to "interface" as a concept in OOP languages, and by "laws" he meant some algebraic laws). Basically what he wanted to know was the algebra, not just interface.
And if you look at it from Curry-Howard correspondence perspective, where programs are proofs and types are theorems, then basically, since type is an interface, you could say that theorems are interfaces in mathematics. So there already is a very precise notion of what is interface.
On the other hand, I also kinda like the notion of DSL as an interface, as described in the recent article here on HN: http://degoes.net/articles/modern-fp/
What seems to be the main contention here - should the interface just use the names (akin to philosophical nominalism) and leave them open to interpretation or should it somehow encode the properties of things it describes (akin to philosophical realism)?