From: "Arnaud Delobelle" <arno@marooned.org.uk>
{ 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 if I'm going over old ground or otherwise am missing something. Thanks, -- Aaron Watters === http://www.xfeedme.com/nucular/pydistro.py/go?FREETEXT=melting