This is somewhat of a note to myself to revist the responses posted.
I'm not 100% percent sure the original author (Mike) really had a grasp on what he was saying. On the one hand, he wanted to get an intuition as to which programs would be problematic to infer types for. But then he started talking about reducing inference for those problems to semi-unification; that's not the right idea! The idea is that you take a bog-standard undecidable problem (e.g. the halting problem), reduce that to semi-unification, and then reduce the reduction to a sample term in System F.
Of course, this would probably yield a term so complex that it would boggle the mind, and not provide the intuition that he was hoping for.
If, on the other hand, he was just interested in the idea of using a (partial) semi-unifier to (partially) perform type inference for System F, then that's a different story. Hard to tell. But lots of interesting points and links in the responses.
the informal ramblings of a formal language researcher
Subscribe to:
Post Comments (Atom)
2 comments:
Your page loaded really quick for all the content and images I'm impressed
Man there is alot of comment spam I have noticed. Is there any way to remove it from the blogs?
Post a Comment