<div>Sorry for bringing back an ancient thread but I'd still like to understand this better.</div><div><br></div><div>It is still not obvious to me why typechecking infinite types is so hard. Is determining type 'equivalence' the hard part? or is that a separate issue?</div>
<div><br></div><div><br></div><div>I wrote a simple infinite type inferer and made an attempt at an algorithm that can answer your question.</div><div><br></div><div>The algorithm works like this: Given two types <b>a</b> and <b>b</b>: unify <b>a</b> with <b>b</b>, if the resulting type is 'equivalent' to the original <b>a,</b> then <b>b</b> must be (I think) at least as general as <b>a</b>.</div>
<div><br></div><div>To determine equivalence, I start with the head of both types (which are represented as graphs) and check to see if the constructors are the same. If they are then I set those two nodes 'equal' and recurse with the children. </div>
<div>It's a 'destructive' algorithm that effectively 'zips' the two graphs together. It returns false if it encounters two constructors that are different.</div><div><br></div><div><br></div><div>My current algorithm says that neither of the types you gave is strictly more general than the other, which I'm guessing is probably not true. I'm curious what the correct answer is and would appreciate someone pointing out the flaw in my reasoning/code :)</div>
<div><br></div><div>My test code is on github here: <a href="https://github.com/jvranish/InfiniteTypes">https://github.com/jvranish/InfiniteTypes</a></div><div><br></div><div>Also, is there a book you'd recommend that would explain this in further detail?</div>
<div><br></div><div>Thanks,</div><div><br></div><div>- Job</div><div><br></div><br><div class="gmail_quote">On Mon, Feb 16, 2009 at 5:16 PM, Luke Palmer <span dir="ltr"><<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish <span dir="ltr"><<a href="mailto:jvranish@gmail.com" target="_blank">jvranish@gmail.com</a>></span> wrote:<br>
</div><div class="gmail_quote"><div class="im"><blockquote class="gmail_quote" style="border-left:1px solid rgb(204, 204, 204);margin:0pt 0pt 0pt 0.8ex;padding-left:1ex">
I'm pretty sure that the problem is decidable, at least with haskell<br>
98 types (other type extensions may complicate things a bit). It ends<br>
up being a graph unification algorithm. I've tried some simple<br>
algorithms and they seem to work.<br>
<br>
What do you mean by "the inference engine is only half of the story"?<br>