Lambda the Ultimate

I doubt we could use contracts effectively for effect systems. The issue is that, while we can specify some post-conditions, we can never specify all of them. This is known as the 'Frame Problem' in AI.

Can you make this concrete? While you probably have a concrete idea of what you mean here, what that is is unclear to me...

The motivation for this is that many higher order functions satisfy nice contracts, but only when their argument is a pure function.

This also makes me think of another point: what is the relation between contracts and specifying properties separately like quickcheck? You could view contract checking as testing specified properties exactly on the values that actually get passed to your functions at runtime, instead of generating random test inputs. Can we perhaps generalize contracts so that you can express properties like map f (map g xs) = map (f . g) xs, and have them checked on the values that actually appear at runtime.

On which values to check them is unclear to me though. A contract like f : int -> int corresponds to the property isint x => isint (f x), but the above property of map doesn't seem to correspond to any contract. So there might be some additional power to be gained here.

I don't see how contracts could help with type classes.

Lets take a generic sum function:

sum xs = fold zero plus xs

The zero and plus have to come from somewhere. With typeclasses they come from the type of the elements of xs. That is, it's something like this:

sum<T : Num> : [T] -> T
sum<T> xs = fold T.zero T.plus xs

Where T is a type parameter. In a dynamically typed language you could pass in T as a record. Can we have an analogue for contracts? I envision T being a contract of type Num (or rather T satisfies the contract Num), which does double duty as a record for carrying zero and plus.

I don't really understand your question.

I agree that use of 'pure functions' is convenient, though it seems reasonable to even consider cost-effects (time, space, energy, heat, power). Making cost effects more explicit in the logic can help control costs.

Contracts specify effects in terms of post-condition checks. In a concurrent system, specifying invariants might also be reasonable, though I know of no decent way to check them without statically checked contracts.

Anyhow, effect systems are all about controlling when and where and what side-effects may occur. Contracts do allow you to specify which effects must occur in terms of local state, but are not so effective for limiting which effects may occur - you can't check everything. I.e. contracts are solving the opposite problem from effect systems. (This suggests contracts and effect systems could complement each other in a single system.)

The zero and plus have to come from somewhere.

Aye, but I've never seen it as the responsibility of the 'contracts' concept to provide such information. A 'contract', much like any assertion, is something you should be able to remove from a correct program without changing its behavior.

Of course contracts in their current form don't do these things, I know that and that's the point. Can they be extended to do these things? Isn't new things what this whole PLT business is about?

A contract on a function in its simplest form takes the function and produces a checked version of the function. For example:

int2int f = fun x -> 
                   assert(isint x)
                   let fx = f x 
                   assert(isint fx)
                   fx

It mediates values between the caller and the callee, ensuring that they have the right properties.

Why shouldn't contracts be able to dynamically mediate side effects? For example, if f performs a side effect, the contract could get notified and can choose to let the side effect through or to raise an error.

Note that this is already possible for some side effects:

doesntraiseanexception f = fun x -> try{ f x }catch{ error "It did throw an exception" }

A 'contract', much like any assertion, is something you should be able to remove from a correct program without changing its behavior.

Yes, the same applies to type systems and type classes. Types "should" be something that you can erase from a program without changing its behavior. Turns out that if you have type classes you can no longer do this, yet they seem to be useful.

Of course contracts in their current form don't do these things [...] Can they be extended to do these things?

The same question could be asked in another way: if you extend their current form to do these things, would the product still be recognizable as 'contracts'? To answer this question, you'll need to decide on what the essential properties are for 'contracts' that distinguish them from dependent typing and other features.

In scientific terms: you need to control your variables. If you are asking what 'contracts' can do, the definition of 'contract' mustn't be among your variables. Settle on a decent operational definition that fits how you are using the word, then explore it.

Isn't new things what this whole PLT business is about?

Not really. PL is simply about the design space of languages. New ideas are part of that, but a relatively small part when compared to composition of features: given N tried-and-true features, there are 2^N combinations. Which combinations will have nice properties? Which combinations are bad? To what extent can we justify such claims? The design-space is even larger than combinations: how shall we express the features? should we permute the features via layering (e.g. in-the-small vs. in-the-large)?

In order to simplify communication about PL, I believe it is better that we attempt to keep definitions constrained. E.g. it is better if 'contract' has a simple, constant meaning from one language to another. Unfortunately, this runs afoul of egos, marketing, and politics. E.g. if 'object oriented' is perceived as a 'good' thing, then people will stretch its definition to fit their languages to such an extent that the phrase no longer makes any useful distinction.

if f performs a side effect, the contract could get notified and can choose to let the side effect through or to raise an error

It is not clear to me that such auditing could be added to a language without support from some other effects management mechanism (such as sandboxes, object capabilities, monads, effect or information-flow typing, et cetera). To whatever extent you need some other effects management mechanism, it seems unreasonable that you would attribute the feature to the 'contracts' concept.

Auditing is AI-complete in any case: Most effects are achieved by composition of smaller effects. E.g. you win a game of chess one move at a time. In general, feedback is required before further progress, which constrains you to incremental auditing with minimal knowledge of ends or future behaviors. It takes a 'sufficiently smart' auditor to recognize he's being led to a bad end - that, or a sufficiently simple and high-level abstraction for actions (e.g. excluding ad-hoc scripts).

You could certainly verify effects by use of contracts. I just don't see contracts as the basis for constraining effects in the first place.

Types "should" be something that you can erase from a program without changing its behavior.

That the meaning of 'types' has been diluted over time to include many forms of typeful programming doesn't mean you should encourage the same fate for 'contracts'. After all, two wrongs don't make a right. It would be preferable if we can make a meaningful distinction between contracts and types (or otherwise just use one word).

This is known as the 'Frame Problem' in AI.

Which is widely seen as solved. Cf. Shanahan, M.P. (1997), Solving the Frame Problem: A Mathematical Investigation of the Common Sense Law of Inertia. MIT Press. It's seen, I think, as a problem with the way the event calculus was formalised.

I'll check out the book (if it seems interesting enough), but as far as "widely seen as solved", I must disagree. (You could check out the book's epilogue to see Shanahan's opinion.)

Either way, the solution isn't contracts.

So "widely seen as solved" may be in the same sense "expression problem" might be "widely seen as solved".