No subject

Tue Feb 1 14:29:29 CET 2011

```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<b=
r>
missing/misunderstanding =A0something?</blockquote></div><div><br>Sorry it =
took me so long to respond.=A0 It took a while to formulate this example.<b=
r><br>Here are two (convoluted) functions, passed to the fixtypes inference=
engine:<br>

<br><font face=3D"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=3D"times new roman,serif">These are so=
mewhat complex types; sorry about that.=A0 But here&#39;s a challenge:=A0 i=
s one of these types more general than the other?=A0 For example, if you wr=
ote the first term and gave the second signature, should it typecheck?=A0 I=
f 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 th=
at would give away the answer :-)<br><br>Luke<br></font></font><br></div><d=
iv><div></div><div class=3D"h5"><blockquote class=3D"gmail_quote" style=3D"=
border-left:1px solid rgb(204, 204, 204);margin:0pt 0pt 0pt 0.8ex;padding-l=
eft: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=3D"mailto:lrpalmer=
@gmail.com" target=3D"_blank">lrpalmer at gmail.com</a>&gt; wrote:<br>
&gt; On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer &lt;<a href=3D"mailto:lrp=
almer at gmail.com" target=3D"_blank">lrpalmer at 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=3D"mailto=
:jvranish at gmail.com" target=3D"_blank">jvranish at gmail.com</a>&gt; wrote:<br=
>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; There are good reasons against allowing infinite types by defa=
ult<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=3D"http://www.nabble.com/There%27s-nothing-wrong-with-=
infinite-types%21-td7713737.html" target=3D"_blank">http://www.nabble.com/T=
here%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 wi=
th an<br>
&gt;&gt;&gt; explicit type signature. In other words, don&#39;t allow infin=
ite 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! =A0I&#39;m sorry, I completely misread the proposal. =A0Or 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). =A0There are pl=
entiful<br>
&gt; undecidable problems with equi-recursive types, but there are ways to =
pull<br>
&gt; it off. =A0The 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, ther=
e<br>
&gt; needs to be a great deal of certainty that this is even possible befor=
e<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? =A0But it is sweeping some very important stuff un=
der the carpet.<br>
&gt;&gt;<br>
&gt;&gt; The proposal is to infer the type of a term, =A0then check it agai=
nst an<br>
&gt;&gt; annotation. =A0Thus 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. =A0I like the ide=
a.<br>
&gt;&gt;<br>
&gt;&gt; But the inference engine is only half of the story. =A0It does no =
type<br>
&gt;&gt; checking. =A0Although checking is often viewed as the easier of th=
e two<br>
&gt;&gt; problems, in this case it is not. =A0A term has no normal form if =
and only if<br>
&gt;&gt; its type is equal to (forall a. a). =A0You can see the problem her=
e.<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 reall=
y need<br>
&gt;&gt;&gt; an infinite type, but in some cases this can be a big annoyanc=
e. 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 func=
tional<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). Allowi=
ng<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 =3D [(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>