You may want to read up on Hindley-Milner type infererence. Here seems to be a Python implementation:
http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hindley-milner-type-inference-implementation-in-python/ Apparently MyPy has type inference as well. On Tue, Sep 15, 2015 at 7:11 PM, Edward K. Ream <[email protected]> wrote: > This is an Engineering Notebook post. Feel free to ignore. > > TL;DR: I'm looking for a problem that a) seems impossible and b) hasn't > been significantly studied. The problem I am thinking of involves > gathering data in new ways to help devs understand programs (their own or > other people's). > > ===== Introduction and motivation > > The original title of this post was going to be, "how to we know when > something is impossible?" > > History is full of examples of seemingly impossible inventions. In Leo's > history, @clean is the best example. For many years I had thought about > the problem of doing without sentinels, and each time I looked at the > problem I saw that sentinels were essential. I finally saw that Leo can > get the sentinels *from the outline itself*, thereby bypassing sentinels > in external files. > > So proofs that something is impossible must be approached with skepticism. > > Contrary to popular opinion, however, it *is* sometimes possible to prove > that something is impossible. For example, Galois paved the way for the > proof that for every *n* > 4, there exist polynomials of degree *n* which > are not solvable by radicals > <https://en.wikipedia.org/wiki/Galois_theory#Solvable_groups_and_solution_by_radicals>. > The immediate result is that some geometric constructions are impossible > with just compass and straight edge. > > Let's turn to workarounds to practical impossibilities. The traveling > salesman problem > <https://en.wikipedia.org/wiki/Travelling_salesman_problem> is known to > be NP-hard, so there is good reason to suppose that no general, efficient, > *perfect* solution will ever be found. Indeed, given the actual answer > to a particular NP-hard problem, it is often *still* NP-hard to verify > that the answer correct! > > But consider this quote from the wikipedia page: > > "Even though the [traveling salesman] problem is computationally > difficult, a large number of heuristics and exact methods are known, so > that some instances with tens of thousands of cities can be solved > completely and even problems with millions of cities can be approximated > within a small fraction of 1%". > > So in engineering and mathematics there is a gray area surrounding the > notion of impossibility. Yes, something may be impossible, strictly > speaking, but often that impossibility doesn't matter. > > ===== Translating Python to C: an impossible solved problem > > I am convinced that this problem, like the traveling salesman problem, is > impossible *in some sense*. Indeed, naive approaches to turning Python > into C are almost certainly misguided foolishness. Among the many gotchas > that naive approaches fail to appreciate are the subtle semantic difference > between Python objects and libraries and the (supposedly) corresponding C > objects and libraries. So a naive Python-to-C translator just isn't likely > to happen. > > But just as with the traveling salesman problem, excellent workarounds are > available now, and these workarounds are only going to get better. cython > <http://cython.org/>allows construction of C extensions for Python using > Python 3.x syntax. The overview page > <http://docs.cython.org/src/quickstart/overview.html> discusses the > details. Most importantly, from my point of view, optional type > annotations can make cython programs almost arbitrarily efficient. I expect > that good work is coming regarding type inference in Python. > > In short, converting Python code to C is *already* solved for many > practical cases, and advances in type inference for Python will only > improve matters. > > A Leo script that could contribute a bit to this general problem. This > script would convert naming conventions to type annotations. I think this > could be useful in a number of ways. But this is a smallish project, no > more than a week or so, I would guess. > > ===== A big, unsolved, unnoticed problem > > Over the last few years I have tried in vain to understand how various > type-checking/inference algorithms have worked. In particular, pylint and > rope do excellent (if limited) type inference. But even though I have > studied the code as imported in Leo, have have not been able really to > grasp what is going on. Neither pylint nor rope document the theory of > operation. It seems that I need better tools to understand the code. > > Naturally, the tools would have to be tailored to each individual app. > Understanding complex code is never going to be routine. > > So that's it. Imo, all juicy projects must come from a real, urgently > felt, need. Understanding Python programs is a real need. I'm not sure > how urgent it seems to me now, but this seems like the only real problem > that I personally have any interest in. > > Your comments please, Amigos. > > Edward > > -- > You received this message because you are subscribed to the Google Groups > "leo-editor" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at http://groups.google.com/group/leo-editor. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/d/optout.
