{ t \in S | s <= t and \forall u \in S (s < u <= t) \implies u = t }

Sorry if I'm late to this discussion, but the hard part here
is defining the partial order <=, it seems to me.
I've tried to think about this at times and I keep getting
entangled in some highly recursive graph matching scheme.
I'm sure the Lisp community has done something with this,
anyone have a reference or something?

For example:

def myFunction(x, y, L):
      z = x+y
      L.append(z)
      return z

What is (or should be) the type of myFunction, x, y, and L?
Well, let's see. type(x) has an addition function that works
with type(y), or maybe type(y) has a radd function that works
with type(x)... or I think Python might try something
involving coercion....? in any case the result type(z) is acceptible to
the append function of type(L)... then I guess myFunction is of type
   type(x) x type(y) x type(L) --> type(z)...

I'm lost.

But that's only the start! Then you have to figure out efficient
ways of calculating these type annotations and looking up "minimal"
matching types.

Something tells me that this might be a Turing complete
problem -- but that doesn't mean you can't come up with
a reasonable and useful weak approximation. Please inform