[...]The Comonad.Reader » Generatingfunctorology[...]…
]]>Ach! So confusing.
]]>Also, I think some of the usual isomorphisms such as the x^2 -> 2*x^2/2 one break down for the same reason the connection between ~~a and a breaks down, because we are working in an intuitionistic setting.
(At least my hand-wavy attempts to try to realize negative values as continuations accepting a given value type seemed to run into that)
]]>If D^2 = 0, then given a functor F described by a generating function
F x = a_0 + a_1*x + a_2*x^2 + …
then
F D = a_0 + a_1*D
cuts off the series.
It also seems that D as a ’singleton pattern’ is affine (permits weakening), because nothing currently prevents you from ‘not using’ the D, as evidenced by the possibility of a_0 being non-zero.
]]>I love the notion of D as a singleton type.
I’ve been thinking about the idea of trying to represent the infinite cases using bivariate generating functions.
The idea would be that you ‘hang up on the number line’ quantities based on two parameters. One the number of traversals of the structure of size >= m that touch n values to give you an idea of the branching structure. Then clearly for n > m, the tail of the series = 0.
You then count the number of cases involved in using productive corecursion to visit n values in the structure rather than the number of distinct ways you can use well-founded recursion to build a structure of a given size.
I haven’t had time in the last couple of days to investigate the idea any further though.
[Edit: this doesn't appear to be sufficient and I haven't been able to find any good closed forms this way yet]
]]>Currently mining the material written on species and what is in that Flajolet/Sedgewick book.
Awesome link, aed. Thanks!
]]>Did you ever read this or this? I spent lots of time thinking similar thoughts but eventually got stuck.
]]>