<div dir="ltr"><div><div><div><div>Yes, it is a coinductive structure (though I had a mental picture of the list as a coinductive structure, which is what it exactly is as far as infinite lists in Haskell are concerned). I got my terms wrong; thanks for that. <br><br></div><div>Let me clarify. By terminal, I meant that the structure itself is made up of finite and infinite structures and you've some way of getting to that finite part (my intuition as a terminal symbol). <br><br></div><div>Take the following for an example.<br><br>data Stream a = Stream a (Stream a) <br></div><div><br></div><div>Stream, by virtue of construction, will have a finite element (or it can be a co-inductive structure again) and an infinite element (the continuation of the stream). <br><br>However, take the OP's code under question<br></div><div><br></div></div>oddsFrom3 = map (+2) oddsFrom3 -- Goes into an infinite loop; violates condition for co-inductiveness; See Link1<br><br></div><div>The above is not guarded by a constructor and there is no way to pull anything useful out of it without going to an infinite loop. So, it has essentially violated the guardedness condition (Link1 to blame/praise for this). This is basically something like<br><br>==========<br></div><div>loop :: [Integer]<br>loop = loop -- This compiles, but god it will never end<br>==========<br></div><div><br></div></div><div>I shouldn't have used the term terminal and I think this is where the confusion stems from. My intuition and what it actually is very similar, yet subtly different. This might further clarify this (Link1)<br></div><br><div><br>=============<br> every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating<br></div>=============<br><br>As for inductive vs co-inductive meaning, I think it is because I see the co-inductive construction as a special case of the inductive step (at least Haskell lets me have this intuition).<br><br><br><br>Link1: <a href="http://adam.chlipala.net/cpdt/html/Coinductive.html">http://adam.chlipala.net/cpdt/html/Coinductive.html</a><br><div class="gmail_extra">Link2: <a href="http://c2.com/cgi/wiki?CoinductiveDataType">http://c2.com/cgi/wiki?CoinductiveDataType</a><br></div><div class="gmail_extra"><div class="gmail_quote"><br>On Mon, Aug 17, 2015 at 11:29 PM, Rein Henrichs <span dir="ltr"><<a href="mailto:rein.henrichs@gmail.com" target="_blank">rein.henrichs@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 dir="ltr">It isn't an inductive structure. It's a *coinductive* structure. And yes, coinductive structures are useful in plenty of scenarios.</div><div class="HOEnZb"><div class="h5"><br><div class="gmail_quote"><div dir="ltr">On Mon, Aug 17, 2015 at 10:30 AM akash g <<a href="mailto:akaberto@gmail.com" target="_blank">akaberto@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Oh, it is a valid value (I think I implied this by saying they'll compile and you can even evaluate). Just not useful in any given scenario (an inductive structure where you don't have terminals).<br> <br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Aug 17, 2015 at 10:57 PM, akash g <span dir="ltr"><<a href="mailto:akaberto@gmail.com" target="_blank">akaberto@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 dir="ltr"><div><div><div><div><div><div><div>@Rein:<br></div>Perhaps I should have been a bit more clear. There is no way to get a terminal value from said function. <br><span><br><br>oddsFrom3 :: [Integer]<br> oddsFrom3 = map (+2) oddsFrom3<br><br></span></div>Try a head for it perhaps.<br><br></div><span>oddsFrom3 = map (+2) oddsFrom3<br></span></div><=> ((head oddsFrom3) + 2) : map (+2) ((tail oddsFrom3) + 2)<br></div><=> ((head (map (+2) oddsFrom3) + 2) : map (+2) ((tail oddsFrom3) + 2)<br><br></div>Sure, it doesn't hang until you try to evaluate this (in lazy language evaluators). However, for any inductive structure, there needs to be a (well any finite number of terminals) terminal (base case) which can be reached from the starting state in a finite amount of computational (condition for termination). Type sigs don't/can't guarantee termination. If they don't have a terminal value, you'll never get to the bottom (bad pun intended) of it.<br><br></div><div><br>Take an infinite list as an example.<br></div><div><br>x a = a : x a<br></div><div><div><div><div><div><div><br></div><div>Here, one branch of the tree (representing the list as a highly unbalanced tree where every left branch is of depth one at any given point). If such a structure is not present, you can never compute it to a value and you'll have to infinitely recurse.<br><br></div><div>Try x a = x a ++ x a<br><br></div><div>And think of the getting the head from this. You're stuck in an infinite loop.<br><br></div><div>You may also think of the above as a small BNF and try to see if termination is possible from the start state. A vaguely intuitive way of looking at it for me, but meh, I might be missing something.<br></div><div><br></div><div><br></div></div></div></div></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Aug 17, 2015 at 10:23 PM, Rein Henrichs <span dir="ltr"><<a href="mailto:rein.henrichs@gmail.com" target="_blank">rein.henrichs@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 dir="ltr"><span>> <span style="font-size:13.1999998092651px;line-height:19.7999992370605px">The initial version which the OP posted doesn't have a terminal value. </span><div><span style="font-size:13.1999998092651px;line-height:19.7999992370605px"><br></span></div></span><div><span style="font-size:13.1999998092651px;line-height:19.7999992370605px">The point is that it doesn't need a terminal value. Infinite lists like oddsFrom3 and (repeat "foo") and (let xs = 1 : xs) are all perfectly valid Haskell values.</span></div></div><div><div><br><div class="gmail_quote"><div dir="ltr">On Mon, Aug 17, 2015 at 6:17 AM Doug McIlroy <<a href="mailto:doug@cs.dartmouth.edu" target="_blank">doug@cs.dartmouth.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> > oddsFrom3 :: [Integer]<br>
> > oddsFrom3 = 3 : map (+2) oddsFrom3<br>
> ><br>
> ><br>
> > Thanks for your help.<br>
><br>
> Try to expand a few steps of the recursion by hand e.g.:<br>
><br>
> 3 : (map (+2) (3 : map (+2) (3 : map (+2) ...)))<br>
><br>
><br>
> As you can see, the deeper you go more 'map (+2)' are applied to '3'.<br>
<br>
Some more ways to describe the program, which may be useful:<br>
<br>
As with any recursive function, assume you know the whole series and<br>
then confirm that by verifying the inductive step. In this case<br>
oddsFrom3 = [3,5,7,9,11,...]<br>
map (+2) oddsFrom3 = [5,7,9,11,13,...]<br>
voila<br>
oddsFrom3 = 3 : map (+2) oddsFrom3<br>
<br>
Assuming we have the whole series, we see its tail is<br>
computed from the whole by adding 2 to each element.<br>
Notice that we don't actually have to know the values in the<br>
tail in order to write the formula for the tail.<br>
<br>
Yet another way to describe the program: the "output" is taken<br>
as "input". This works because the first element of the output,<br>
namely 3, is provided in advance. Each output element can then<br>
be computed before it is needed as input.<br>
<br>
In an imperative language this would be done so:<br>
integer oddsFrom3[0:HUGE]<br>
oddsFrom3[0] := 3<br>
for i:=1 to HUGE do<br>
oddsFrom3[i] = oddsFrom3[i-1] + 2<br>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
</blockquote></div>
</div></div><br>_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
<br></blockquote></div><br></div></div></div></div>
</blockquote></div><br></div>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
</blockquote></div>
</div></div><br>_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
<br></blockquote></div><br></div></div>