Re: Can Contracts be Equated with Types?
Posted: Aug 9, 2006 1:32 AM
> I did reply on March 21st:
> Hi Achilleas,
> I'm sorry it took me so long to get back to you. This new
> job has me swamped. I've looked at your idea, and it does
> seem solid for languages without side-effects (for example
> Unimperative, or Joy or Haskell). For languages with
> side-effects, then I don't see how we can practically
> measure the output of a function (since it can affect any
> part of the state). I hope this makes some sense. I think
> your idea merits further exploration in the context of
> smaller, easier to study languages. I do think that LtU
> would have some good feedback. If you are nervous about
> sharing your ideas, I suggest to start by asking questions
> to find out about related work. There is a possibility
> this idea is currently being researched. However, it
> definitely makes me think about what could be done
> applying your idea to Unimperative. Keep coming up with
> good ideas!
> > I would be more than happy to
> > send you again the e-mail, if you wish.
> I encourage you to post it here!
Ah, ok. Somehow I did not get hold of it.
I disagree that it can not be applied to languages without referential transparency.
I won't be posting these ideas to LtU, because I am too lazy to formalize them. If anyone is interested, feel free to pick up the idea and make a formal paper out of it.
Anyway, for anyone interested, the idea is:
A block of code has a set of inputs (allowed values) and outputs (possible outcomes). When two blocks of code are paired up in a sequence, the outputs of the 1st block must be a subset of the inputs of the 2nd block. A compiler rejects a block of code that does not conform to this simple rule. This technique could enable static contract evaluation.
The set of inputs can be precisely defined by declaring contracts.
In order to implement this, sets should be smartly represented, either as sets of discrete values, or ranges, or intersections/unions. You do not have to perform big computations, because the I/O sets are small usually.
The real interesting trick in this technique is that when two blocks of code are combined, new sets of inputs and outputs are created for the combined block, which does not necessarily include the values of the two blocks that where combined.
The above does not relate to the halting problem in anyway. It does not tell you if an algorithm terminates or not; it is a mechanism for checking contracts at compile-time, instead of run-time.
I am optimistic about this technique that it can even tell you if some algorithms loop forever, by treating the Program Counter as an input/output value.
The input/output information can be kept around in libraries, so as that when one uses the library, the contracts are part of the system.