Re: [Haskell-beginners] oddsFrom3 function

17 Aug 2015

      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.

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).

Take  the following for an example.

data Stream a = Stream a (Stream a)

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).

However, take the OP's code under question

oddsFrom3 = map (+2) oddsFrom3  -- Goes into an infinite loop; violates
condition for co-inductiveness; See Link1

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

==========
loop :: [Integer]
loop = loop  -- This compiles, but god it will never end
==========

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)

=============
every co-recursive call must be a direct argument to a constructor of the
co-inductive type we are generating
=============

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).

Link1: http://adam.chlipala.net/cpdt/html/Coinductive.html
Link2: http://c2.com/cgi/wiki?CoinductiveDataType

On Mon, Aug 17, 2015 at 11:29 PM, Rein Henrichs 
wrote:
...
It isn't an inductive structure. It's a *coinductive* structure. And yes,
coinductive structures are useful in plenty of scenarios.
On Mon, Aug 17, 2015 at 10:30 AM akash g  wrote:
...
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).
On Mon, Aug 17, 2015 at 10:57 PM, akash g  wrote:
...
@Rein:
Perhaps I should have been a bit more clear.  There is no way to get a
terminal value from said function.
oddsFrom3 :: [Integer]
oddsFrom3 = map (+2) oddsFrom3
Try a head for it perhaps.
oddsFrom3 = map (+2) oddsFrom3
<=> ((head  oddsFrom3) + 2) : map (+2) ((tail  oddsFrom3) + 2)
<=> ((head (map (+2) oddsFrom3) + 2) : map (+2) ((tail  oddsFrom3) + 2)
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.
Take an infinite list as an example.
x a = a :  x a
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.
Try x a = x a ++ x a
And think of the getting the head from this.  You're stuck in an
infinite loop.
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.
On Mon, Aug 17, 2015 at 10:23 PM, Rein Henrichs 
...
wrote:
...
...
The initial version which the OP posted doesn't have a terminal
value.
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.
On Mon, Aug 17, 2015 at 6:17 AM Doug McIlroy 
wrote:
...
...
> oddsFrom3 :: [Integer]
> oddsFrom3 = 3 : map (+2) oddsFrom3
>
>
> Thanks for your help.
Try to expand a few steps of the recursion by hand e.g.:
3 : (map (+2) (3 : map (+2) (3 : map (+2) ...)))
As you can see, the deeper you go more 'map (+2)' are applied to '3'.
Some more ways to describe the program, which may be useful:
As with any recursive function, assume you know the whole series and
then confirm that by verifying the inductive step. In this case
        oddsFrom3          = [3,5,7,9,11,...]
        map (+2) oddsFrom3 = [5,7,9,11,13,...]
voila
        oddsFrom3 = 3 : map (+2) oddsFrom3
Assuming we have the whole series, we see its tail is
computed from the whole by adding 2 to each element.
Notice that we don't actually have to know the values in the
tail in order to write the formula for the tail.
Yet another way to describe the program: the "output"  is taken
as "input". This works because the first element of the output,
namely 3, is provided in advance. Each output element can then
be computed before it is needed as input.
In an imperative language this would be done so:
        integer oddsFrom3[0:HUGE]
        oddsFrom3[0] := 3
        for i:=1 to HUGE do
                oddsFrom3[i] = oddsFrom3[i-1] + 2
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners