Lambda the Ultimate

Most static OO languages require the list to be of some base class that determines the list type. Existential types in functional languages serve a similar purpose. Of course, you're left with a bunch of upcasting and downcasting.

See HLists, a way of having heterogeneous linked lists in Haskell. I'm not sure if this is what you want, though I don't see how this can be done without just knowing the type of each element. http://homepages.cwi.nl/~ralf/HList/

thanks - interesting paper. in more general terms, i think i need to look at dependent types (which, i think, are the basis for the paper, though i've only skimmed it so far).

You might want to have a look at Merd, a largely incomplete, dynamic functional language with some interesting features. In Merd, as I understand it, lists contain a union of types.

http://merd.sourceforge.net/

Relevant excerpt from Merd web site:

# Try hard to keep the more precise types
  [ 1, "foo" ] !! [ 1 | "foo" ]
means the type of list [ 1, "foo" ] is a list of elements of type 1|"foo"

# existential-like types with subtyping:
  [x,y] !! [Int|String] with x !! Int ; y !! String
means type of list [x,y] is a list of elements of type Int|String

  [ 1, "foo" ].map(+ 1) is ill-typed, but
  [ 1, "foo" ].map(+ 1|&|"bar") gives [ 2, "foobar" ] 

I agree that a DbC point of view is probably a better way to go with Python. WRT to your suggestions, most of the examples of predicates have to do with class level properties. Can you have predicates that test method parameters?

One thing that strikes me is that you are trying to have Named Assertions. But this simply redirects the question to why we would believe that assertions() as provided by Python are insufficient as a DbC mechanism (not to mention whether this is really a Unit Test problem). Well, I suppose the Eiffel folks would argue that there is no formal mechanism for documenting the assertions as part of the class/method/property signature. I guess you could also hold that there's no mechanism for automatically enforcing the classs level invariants.

Anyhow, if documentation is the aim, I think you need to have the predicates as a formal part of the declaration syntax, lest it's impossible to discern what's a pre, post, or invariant.

You make some good points, there are a few things that I should flesh out to increase the clarity of my ideas.

The point of named assertions is reusability -

compare this:

pred Iterable:
  hasattr(self, "__iter__")

def map(fn, lst:Iterable):
  # ...

def filter(fn, lst:Iterable):
  # ...

with something like:

def map(fn, lst):
  ?:
    hasattr(lst, "__iter__")
  # ...

def filter(fn, lst):
  ?:
    hasattr(lst, "__iter__")
  # ...

In the long run, you can increase the modularity and reusability of your conditions if you define them as self-standing predicates.

You can easily have predicates that test method parameters, but if your conditions are specific to a single method, it makes more sense to put them in the method conditional block rather than in an external predicate. One should only define an external predicate if one intends on using the same conditions in multiple places.

An example of a predicate that tests a method parameter:

pred negative:
  self