Christian: Thank you for asking for additional reading material. Nicolas: Thank you for providing additional reading material.
On Thursday, May 10, 2012 at 7:02 AM, nicolas.o...@gmail.com wrote: > I can describe the background to understand my last email. > > From the programming point of view, I have been told since yesterday > that what I explained has already been explained better in "Stream > Fusion From Lists to Streams to Nothing at All" from Coutts > Leschinskiy and Stewart: > > metagraph.org/papers/stream_fusion.pdf > (http://metagraph.org/papers/stream_fusion.pdf) > > The article is very clear if you can get used to the strange Haskell > syntax and its lack of brackets. > > <off-topic> > From the cultural/theoritical point of view, there is quite well > understood link between data-structures and > some categorical structures. > ( I try stay informal and put fancy names and link to definitions > inside brackets ) > > Types of finite recursive data structures (think of a list) are > defined by being the smallest solution to an > equation like List = 1 + Any x List. Here 1 means the type that > contains only nil, Any means the type of anything, x corresponds to a > pair and + to a choice. So this reads: a list is either nil or a pair > of anything and another list. > Being the smallest solution means that it contains only finite > data-structures. > ( http://en.wikipedia.org/wiki/Initial_algebra ) > > An element of such a type is characterised by how they can be reduced/folded. > ( http://en.wikipedia.org/wiki/Catamorphism ) > fold: forall A, List -> ((1 + Any x Acc) -> Acc) -> Acc > Meaning that there is a one to one mapping between lists and functions of > type: > forall Acc, ((1 + Any x Acc) -> Acc) -> Acc > This is the type of #(reduce _ l): you give it a function that takes > either no arguments and give you > an initial Accumulator or take an element of the list and and the last > Accumulator and returns a new Accumulator, and it returns the last > Accumulators. > > This one to one correspondence can be seen as (reduce _ l) in one > direction and #(_ (fn [p] (and p (apply cons p))) in the other > direction. > > This definition of lists (as functions) has been used in programming > languages without data constructors. > ( System F for example, http://en.wikipedia.org/wiki/System_F ). > > If you look to infinite data structures, like Streams, they are the > biggest solutions of similar equations: > Stream = 1 + Any x Stream (if you accept a Stream can finish early) > > They are dual (which means you invert all arrows in all definitions) to Lists. > ( see Final Coalgebra in http://en.wikipedia.org/wiki/Initial_algebra ) > > A stream is characterised as how it is unfolded/generated. > unfold : forall B, (B -> 1 + Any x B) -> B -> Stream > (See how the arrows are reversed with respect to fold) > And so they are in one to one correspondence with : > exists Seed, (Seed x (Seed -> 1 + Any x Seed)) > > Which means any Stream can be defined as a Seed, of a given type Seed > that you can choose freely, > and a way to grow from the seed, a function grow that takes a Seed and > tells you: > - either that the Stream is finished > - or the first element of the Stream and the Seed for the rest of the Stream. > > For example the stream of even natural numbers can be seen as the seed > 0 together with a function > grow = (fn [ seed ] [ seed (+ seed 2) ]), saying that first element > is equal to the seed and the rest of the stream > is the one defined by a seed = seed + 2 . > > A very good paper showing this style of programming, and more, is : > > http://eprints.eemcs.utwente.nl/7281/01/db-utwente-40501F46.pdf > </off-topic> > > Sorry for the long off-topic. > > Best regards, > > Nicolas. > > -- > You received this message because you are subscribed to the Google > Groups "Clojure" group. > To post to this group, send email to clojure@googlegroups.com > (mailto:clojure@googlegroups.com) > Note that posts from new members are moderated - please be patient with your > first post. > To unsubscribe from this group, send email to > clojure+unsubscr...@googlegroups.com > (mailto:clojure+unsubscr...@googlegroups.com) > For more options, visit this group at > http://groups.google.com/group/clojure?hl=en > > -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en
