On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish <span dir="ltr">&lt;<a href="mailto:jvranish@gmail.com" target="_blank">jvranish@gmail.com</a>&gt;</span> wrote:<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;">

I&#39;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&#39;ve tried some simple<br>
algorithms and they seem to work.<br>
<br>
What do you mean by &quot;the inference engine is only half of the story&quot;?<br>
>From what I understand, the inference engine infers types via<br>
unification, if the types unify, then the unified types are the<br>
inferred types, if the types don&#39;t unify, then type check fails. Am I<br>
missing/misunderstanding &nbsp;something?</blockquote><div><br>Sorry it took me so long to respond.&nbsp; It took a while to formulate this example.<br><br>Here are two (convoluted) functions, passed to the fixtypes inference engine:<br>
<br><font face="courier new,monospace">Expr&gt; y (b (c i) (c (b b (b c (c i)))))<br>(fix b . (a -&gt; b -&gt; (a -&gt; c -&gt; d) -&gt; d) -&gt; c) -&gt; c<br>Expr&gt; y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k)))<br>
(fix c . ((a -&gt; ((b -&gt; c) -&gt; d) -&gt; (a -&gt; d -&gt; e) -&gt; e) -&gt; f) -&gt; f)<br><br><font face="times new roman,serif">These are somewhat complex types; sorry about that.&nbsp; But here&#39;s a challenge:&nbsp; is one of these types more general than the other?&nbsp; For example, if you wrote the first term and gave the second signature, should it typecheck?&nbsp; If you figure it out, can you give an algorithm for doing so?<br>
<br>I&#39;m not going to say how I came up with these functions, because that would give away the answer :-)<br><br>Luke<br></font></font><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

<br>
<br>
I almost think that the problem might be solvable by just generating<br>
the appropriate newtype whenever an infinite type shows up, and doing<br>
the wrapping/unwrapping behind the scenes. This would be a hacked up<br>
way to do it, but I think it would work.<br>
<div><div></div><div><br>
<br>
On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer &lt;<a href="mailto:lrpalmer@gmail.com" target="_blank">lrpalmer@gmail.com</a>&gt; wrote:<br>
&gt; On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer &lt;<a href="mailto:lrpalmer@gmail.com" target="_blank">lrpalmer@gmail.com</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish &lt;<a href="mailto:jvranish@gmail.com" target="_blank">jvranish@gmail.com</a>&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; There are good reasons against allowing infinite types by default<br>
&gt;&gt;&gt; (mostly, that a lot of things type check that are normally not what we<br>
&gt;&gt;&gt; want). An old haskell cafe conversation on the topic is here:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; <a href="http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types%21-td7713737.html" target="_blank">http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737.html</a><br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; However, I think infinite types should be allowed, but only with an<br>
&gt;&gt;&gt; explicit type signature. In other words, don&#39;t allow infinite types to<br>
&gt;&gt;&gt; be inferred, but if they are specified, let them pass. I think it<br>
&gt;&gt;&gt; would be very hard to shoot yourself in the foot this way.<br>
&gt;<br>
&gt; Oops! &nbsp;I&#39;m sorry, I completely misread the proposal. &nbsp;Or read it correctly,<br>
&gt; saw an undecidability hiding in there, and got carried away.<br>
&gt;<br>
&gt; What you are proposing is called equi-recursive types, in contrast to the<br>
&gt; more popular iso-recursive types (which Haskell uses). &nbsp;There are plentiful<br>
&gt; undecidable problems with equi-recursive types, but there are ways to pull<br>
&gt; it off. &nbsp;The question is whether these ways play nicely with Haskell&#39;s type<br>
&gt; system.<br>
&gt;<br>
&gt; But because of the fundamental computational problems associated, there<br>
&gt; needs to be a great deal of certainty that this is even possible before<br>
&gt; considering its language design implications.<br>
&gt;<br>
&gt;&gt;<br>
&gt;&gt; That inference engine seems to be a pretty little proof-of-concept,<br>
&gt;&gt; doesn&#39;t it? &nbsp;But it is sweeping some very important stuff under the carpet.<br>
&gt;&gt;<br>
&gt;&gt; The proposal is to infer the type of a term, &nbsp;then check it against an<br>
&gt;&gt; annotation. &nbsp;Thus every program is well-typed, but it&#39;s the compiler&#39;s job<br>
&gt;&gt; to check that it has the type the user intended. &nbsp;I like the idea.<br>
&gt;&gt;<br>
&gt;&gt; But the inference engine is only half of the story. &nbsp;It does no type<br>
&gt;&gt; checking. &nbsp;Although checking is often viewed as the easier of the two<br>
&gt;&gt; problems, in this case it is not. &nbsp;A term has no normal form if and only if<br>
&gt;&gt; its type is equal to (forall a. a). &nbsp;You can see the problem here.<br>
&gt;&gt;<br>
&gt;&gt; Luke<br>
&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Newtype is the standard solution to situations where you really need<br>
&gt;&gt;&gt; an infinite type, but in some cases this can be a big annoyance. Using<br>
&gt;&gt;&gt; newtype sacrifices data type abstraction and very useful type classes<br>
&gt;&gt;&gt; like Functor. You can use multiparameter type classes and functional<br>
&gt;&gt;&gt; dependencies to recover some of the lost abstraction, but then type<br>
&gt;&gt;&gt; checking becomes harder to reason about and the code gets way more<br>
&gt;&gt;&gt; ugly (If you doubt, let me know, I have some examples). Allowing<br>
&gt;&gt;&gt; infinite types would fix this.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; I&#39;m imagining a syntax something like this:<br>
&gt;&gt;&gt; someFunctionThatCreatesInfiniteType :: a -&gt; b | b = [(a, b)]<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Thoughts? Opinions? Am I missing anything obvious?<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; - Job<br>
&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt; Haskell-Cafe mailing list<br>
&gt;&gt;&gt; <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
&gt;&gt;&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;&gt;<br>
&gt;<br>
&gt;<br>
</div></div></blockquote></div><br>