[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Curl, multiple inheritance, and interfaces (was Re: cheerfulstatic typing)

   Date: Fri, 11 Jan 2002 18:35:01 -0500 (EST)
   From: Kimberley Burchett <kimbly@cybercom.net>
   Cc: ll1-discuss@ai.mit.edu
   Precedence: bulk

   On Fri, 11 Jan 2002, Dan Weinreb wrote:

   >                              remember that email I sent a while ago
   > about how it would be nice if interfaces, in addition to simply
   > specifying the entrypoint names and their arg types and return types,
   > could also say more interesting things about their semantics, like
   > that write("foo") followed by write("bar") is the same as
   > write("foobar") in the absence of exceptions, or that addition is
   > commutative, etc? 

   I'm curious how far one could take this approach.  Suppose you start with
   a list of methods with type information for parameters and return values.  
   Now you start adding more and more details about the interface's
   "semantics".  This basically amounts to laying constraints on the set of
   allowed implementations of that interface.  E.g. in your above example, if
   an implementation doesn't fulfill the constraint that write("foo")
   followed by write("bar") is equivalent to write("foobar"), then that
   implementation is broken -- it violates an interface constraint.

This has been tried in the past. I believe Alphard was the name of a language
designed by Bill Wulf & Mary Shaw at CMU sometime before I showed up there
(1983). It allowed you to put specs like
    push(x, pop(push(y,s))) = push(x,s)
    top(push(x,s)) = x
in an interface. If your code didn't support the spec -- maybe your
push/pop/top implementation satisfies the *type*, but *implements* a queue,
not a stack -- then it was rejected by the compiler.

They wrote a paper on this, which I read a long, long time ago. I expect that
it did not work out due to the raw difficulty of the checking problem... or
else you'd have heard about it already.

It's a good idea, and one that deserves to be raised & considered from time to
time. Maybe one time, someone will figure out how to make it work, as we make
progress on related fronts.

The name of the programming-language static-analysis game is how to skate
close along the cliff of intractability/undecideability -- close enough to
extract some meaning from our programs, but without going over the edge.
Types never go over the edge. But you always want to get closer...