From: "Arnaud Delobelle" <<a href="mailto:arno@marooned.org.uk">arno@marooned.org.uk</a>><br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>{ t \in S | s <= t and \forall u \in S (s < u <= t) \implies  u = t }</blockquote><div><br>Sorry if I'm late to this discussion, but the hard part here<br>is defining the partial order <=, it seems to me.
<br>I've tried to think about this at times and I keep getting<br>entangled in some highly recursive graph matching scheme.<br>I'm sure the Lisp community has done something with this,<br>anyone have a reference or something? 
<br><br>For example:<br><br>def myFunction(x, y, L):<br>      z = x+y<br>      L.append(z)<br>      return z<br><br>What is (or should be) the type of myFunction, x, y, and L?<br>Well, let's see. type(x) has an addition function that works
<br>with type(y), or maybe type(y) has a radd function that works<br>with type(x)... or I think Python might try something<br>involving coercion....? in any case the result type(z) is acceptible to<br>the append function of type(L)... then I guess myFunction is of type
<br>   type(x) x type(y) x type(L) --> type(z)...<br><br>I'm lost.<br><br>But that's only the start!  Then you have to figure out efficient<br>ways of calculating these type annotations and looking up "minimal"
<br>matching types.<br><br>Something tells me that this might be a Turing complete<br>problem -- but that doesn't mean you can't come up with<br>a reasonable and useful weak approximation.  Please inform<br></div>
</div>if I'm going over old ground or otherwise am missing something.<br><br>Thanks,  -- Aaron Watters<br>===<br><a href="http://www.xfeedme.com/nucular/pydistro.py/go?FREETEXT=melting">http://www.xfeedme.com/nucular/pydistro.py/go?FREETEXT=melting
</a><br><br>