On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer <span dir="ltr">&lt;<a href="mailto:lrpalmer@gmail.com">lrpalmer@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;">
<div class="Ih2E3d">On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish <span dir="ltr">&lt;<a href="mailto:jvranish@gmail.com" target="_blank">jvranish@gmail.com</a>&gt;</span> wrote:<br></div><div class="gmail_quote"><div class="Ih2E3d">
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
There are good reasons against allowing infinite types by default<br>
(mostly, that a lot of things type check that are normally not what we<br>
want). An old haskell cafe conversation on the topic is here:<br>
<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>
<br>
However, I think infinite types should be allowed, but only with an<br>
explicit type signature. In other words, don&#39;t allow infinite types to<br>
be inferred, but if they are specified, let them pass. I think it<br>
would be very hard to shoot yourself in the foot this way.</blockquote></div></div></blockquote><div><br>Oops!&nbsp; I&#39;m sorry, I completely misread the proposal.&nbsp; Or read it correctly, saw an undecidability hiding in there, and got carried away.<br>
<br>What you are proposing is called equi-recursive types, in contrast to the more popular iso-recursive types (which Haskell uses).&nbsp; There are plentiful undecidable problems with equi-recursive types, but there are ways to pull it off.&nbsp; The question is whether these ways play nicely with Haskell&#39;s type system.<br>
<br>But because of the fundamental computational problems associated, there needs to be a great deal of certainty that this is even possible before considering its language design implications.<br>&nbsp;</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="gmail_quote"><div class="Ih2E3d"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"></blockquote></div><div><br>That inference engine seems to be a pretty little proof-of-concept, doesn&#39;t it?&nbsp; But it is sweeping some very important stuff under the carpet.<br>

<br>The proposal is to infer the type of a term,&nbsp; then check it against an annotation.&nbsp; Thus every program is well-typed, but it&#39;s the compiler&#39;s job to check that it has the type the user intended.&nbsp; I like the idea.<br>

<br>But the inference engine is only half of the story.&nbsp; It does no type checking.&nbsp; Although checking is often viewed as the easier of the two problems, in this case it is not.&nbsp; A term has no normal form if and only if its type is equal to (forall a. a).&nbsp; You can see the problem here.<br>
<font color="#888888">
<br>Luke<br><br></font></div><div class="Ih2E3d"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
<br>
Newtype is the standard solution to situations where you really need<br>
an infinite type, but in some cases this can be a big annoyance. Using<br>
newtype sacrifices data type abstraction and very useful type classes<br>
like Functor. You can use multiparameter type classes and functional<br>
dependencies to recover some of the lost abstraction, but then type<br>
checking becomes harder to reason about and the code gets way more<br>
ugly (If you doubt, let me know, I have some examples). Allowing<br>
infinite types would fix this.<br>
<br>
I&#39;m imagining a syntax something like this:<br>
someFunctionThatCreatesInfiniteType :: a -&gt; b | b = [(a, b)]<br>
<br>
Thoughts? Opinions? Am I missing anything obvious?<br>
<br>
- Job<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div></div><br>
</blockquote></div><br>