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'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> y (b (c i) (c (b b (b c (=
c i)))))<br>(fix b . (a -> b -> (a -> c -> d) -> d) -> c)=
-> c<br>Expr> y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k)))<br>
(fix c . ((a -> ((b -> c) -> d) -> (a -> d -> e) -> e)=
-> f) -> f)<br><br><font face=3D"times new roman,serif">These are so=
mewhat complex types; sorry about that.=A0 But here'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'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 <<a href=3D"mailto:lrpalmer=
@gmail.com" target=3D"_blank">lrpalmer at gmail.com</a>> wrote:<br>
> On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer <<a href=3D"mailto:lrp=
almer at gmail.com" target=3D"_blank">lrpalmer at gmail.com</a>> wrote:<br>
>><br>
>> On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish <<a href=3D"mailto=
:jvranish at gmail.com" target=3D"_blank">jvranish at gmail.com</a>> wrote:<br=
>
>>><br>
>>> There are good reasons against allowing infinite types by defa=
ult<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>
>>><br>
>>> <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>
>>><br>
>>> However, I think infinite types should be allowed, but only wi=
th an<br>
>>> explicit type signature. In other words, don't allow infin=
ite 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.<br>
><br>
> Oops! =A0I'm sorry, I completely misread the proposal. =A0Or read =
it correctly,<br>
> 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<br>
> more popular iso-recursive types (which Haskell uses). =A0There are pl=
entiful<br>
> undecidable problems with equi-recursive types, but there are ways to =
pull<br>
> it off. =A0The question is whether these ways play nicely with Haskell=
's type<br>
> system.<br>
><br>
> But because of the fundamental computational problems associated, ther=
e<br>
> needs to be a great deal of certainty that this is even possible befor=
e<br>
> considering its language design implications.<br>
><br>
>><br>
>> That inference engine seems to be a pretty little proof-of-concept=
,<br>
>> doesn't it? =A0But it is sweeping some very important stuff un=
der the carpet.<br>
>><br>
>> The proposal is to infer the type of a term, =A0then check it agai=
nst an<br>
>> annotation. =A0Thus every program is well-typed, but it's the =
compiler's job<br>
>> to check that it has the type the user intended. =A0I like the ide=
a.<br>
>><br>
>> But the inference engine is only half of the story. =A0It does no =
type<br>
>> checking. =A0Although checking is often viewed as the easier of th=
e two<br>
>> problems, in this case it is not. =A0A term has no normal form if =
and only if<br>
>> its type is equal to (forall a. a). =A0You can see the problem her=
e.<br>
>><br>
>> Luke<br>
>><br>
>>><br>
>>><br>
>>> Newtype is the standard solution to situations where you reall=
y need<br>
>>> an infinite type, but in some cases this can be a big annoyanc=
e. Using<br>
>>> newtype sacrifices data type abstraction and very useful type =
classes<br>
>>> like Functor. You can use multiparameter type classes and func=
tional<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). Allowi=
ng<br>
>>> infinite types would fix this.<br>
>>><br>
>>> I'm imagining a syntax something like this:<br>
>>> someFunctionThatCreatesInfiniteType :: a -> b | b =3D [(a, =
b)]<br>
>>><br>
>>> Thoughts? Opinions? Am I missing anything obvious?<br>
>>><br>
>>> - Job<br>
>>> _______________________________________________<br>
>>> Haskell-Cafe mailing list<br>
>>> <a href=3D"mailto:Haskell-Cafe at haskell.org" target=3D"_blank">=
Haskell-Cafe at haskell.org</a><br>
>>> <a href=3D"http://www.haskell.org/mailman/listinfo/haskell-caf=
e" target=3D"_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</=
a><br>
>><br>
><br>
><br>
</div></div></blockquote></div></div></div><br>
</blockquote></div><br><div><br></div>
--bcaec51a86603b475f049cc0660e--
More information about the Haskell-Cafe
mailing list