tag:blogger.com,1999:blog-11295132.post114995926296648953..comments2017-07-18T12:14:11.585-07:00Comments on A Neighborhood of Infinity: Monads, Kleisli Arrows, Comonads and other Rambling ThoughtsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger12125tag:blogger.com,1999:blog-11295132.post-43869804011880263452014-01-19T10:31:48.474-08:002014-01-19T10:31:48.474-08:00"This is a function where the nth element of ...<i>"This is a function where the nth element of the output depends only on the first n values of the input. This pattern fits many types of processing in dataflow applications such as audio processing."</i><br /><br />Well, usually... <a href="http://www.youtube.com/watch?v=jMS7tyh_C0Q" rel="nofollow">there are exceptions</a>.Danielhttps://www.blogger.com/profile/11384619047799752406noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-67648986560069586132011-07-30T06:03:15.066-07:002011-07-30T06:03:15.066-07:00Followup to the two questions in my prior comment....Followup to the two questions in my prior comment.<br /><br />Monad can't abstract a comonad, because it has no method, m a -> a, for creating a new observation. A monad can abstract the history of prior observations. Afaics, for a language with multiple inheritance, a subtype of comonad could also be a subtype of monad, thus providing a monadic interface to the history of observations. This is possible because the comonad observation factory method, m a -> a, is impure (the state of the comonad blackbox changes when history is created from it).<br /><br />Composition of functions, m a -> b, which input a comonad is pure (i.e. no side-effects, referentially transparent, declarative not imperative) where those functions are pure (e.g. they do not invoke m a -> a to create a new observation). In short, the method (m a -> b) -> m a -> m b is pure if m a -> b is.shelbyhttps://www.blogger.com/profile/04192118408905938326noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-33594190493281602342011-07-27T08:16:42.514-07:002011-07-27T08:16:42.514-07:00Monad is the model for any parametric type that we...Monad is the model for any parametric type that we know the generative structure of, so we can compose functions on lifted outputs, because the type knows how to lift (i.e. construct, generate, 'unit' or 'return') instances of its type parameter to its structure.<br /><br />Comonad is the model for any parametric type that we don't know how to generate its structure, but we can observe instances of the type parameter its structure as they occur. We will only know its final structure when it is destructed, and observation ceases. We can't lift instances of its type parameter to its structure, so we can't compose functions on outputs. Instead, we can compose functions with lifted inputs (and optionally outputs, i.e. map on observations), because the type has observations.<br /><br />Conceptually monad vs. comand duality is related to the duality of induction vs. coinduction, and initial vs. final (least vs. greatest) fixpoint, because we can generate structure for a type that has an initiality, but we can only observe structure until we reach a finality.<br /><br /><a href="http://tunes.org/wiki/induction_20and_20co-induction.html" rel="nofollow">Induction and Co-induction</a><br /><a href="http://tunes.org/wiki/initiality_20and_20finality.html" rel="nofollow">Initiality and Finality</a><br /><a href="http://en.wikipedia.org/wiki/Coinduction" rel="nofollow">Wikipedia Coinduction</a><br /><br />I had visited this blog page before (and not completely grasped it), then I read this page again trying conceptualize the <a href="http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/" rel="nofollow">sum vs. products duality</a> for eager vs. lazy evaluation.<br /><br />Perhaps I am in error, but it appears that with lazy evaluation and <a href="http://en.wikipedia.org/wiki/Corecursion#Definition" rel="nofollow">corecursion</a>, monad can be used instead of comonad, e.g. isn't it true a stream can be abstracted by a monadic list in haskell?<br /><br />So dually, am I correct to interpret that <a href="http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/#comment-806" rel="nofollow">laziness isn't necessary</a> for modeling compositionality of coinductive types, when there is comonad in the pure (referential transparent) part where the composition is?shelbyhttps://www.blogger.com/profile/04192118408905938326noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-42056780322600318212010-10-01T11:17:55.336-07:002010-10-01T11:17:55.336-07:00I know that this is centuries old, but this may be...I know that this is centuries old, but this may be helpful in finding the right syntax for comonads: <a href="http://www.cs.cmu.edu/afs/cs/Web/People/fp/papers/mscs00.pdf" rel="nofollow">Pfenning and Davies, 2001</a>. The category-theoretic semantics, a monad for the "diamond" and a comonad for the "box", is discussed in this paper: <a href="http://www.cs.nott.ac.uk/~nza/papers/Alechina++:01a.pdf" rel="nofollow">Alechina et al., 2001</a>. The box and the diamond are essentially the "m" functor used above.<br /><br><br />In the case of monads you can form a fancy (monadic) term trivially by returning an ordinary value (this is called diamond introduction), but to consume (to eliminate the diamond) it you need a "bind" construct. For comonods, it turns out that use of fancy data (box elimination or unboxing) is trivial, but forming a piece of fancy data (box introduction or boxing) is the big deal: you have to form it without a reference to local variables.Saintalihttps://www.blogger.com/profile/02645553817579923971noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-41670088008935435492009-07-01T21:59:09.364-07:002009-07-01T21:59:09.364-07:00yakov,
In Control.Monad you'll find the funct...yakov,<br /><br />In Control.Monad you'll find the function join :: Monad m => m (m a) -> m a<br />Mathematicians usually define monads in terms of this.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-53424035646505570662009-07-01T21:56:44.284-07:002009-07-01T21:56:44.284-07:00However, part of the definition of monads is that ...<i>However, part of the definition of monads is that there is a map m (m c)→m c.</i><br /><br />Which definition?<br /><br />I could not find such operation in standard Monad type classyakovhttps://www.blogger.com/profile/14260132358343297792noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-9727377725332892322008-10-08T11:45:00.000-07:002008-10-08T11:45:00.000-07:00Re: nolrai_I just had the same thought today... I ...Re: nolrai_<BR/><BR/>I just had the same thought today... I think, if you are using streams, then each stream represents the _future_ from that point onward. If you want a comonad that talks about the past, try a non-empty list (i.e. list'[a] = a * (1 + list'[a])). Then your join will get a list of histories.<BR/><BR/>(Disclaimer: not my idea, see Uustalu and Vene's "Signals and Comonads".)Chris Kinghttps://www.blogger.com/profile/18278436935541738068noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-19116217239522816232008-06-01T09:05:00.000-07:002008-06-01T09:05:00.000-07:00hmm I was looking at making lists into a comonad, ...hmm I was looking at making lists into a comonad, and got distracted by the fact that the empty list messes every thing up. and so I defined a infinite list data type and made that a comonad, but your join doesn't work, because those sublists are finite, so instead:<BR/>cojoin s = s : cojoin (tail s)<BR/><BR/>ie cojoin [x1,x2,x3..] = [[x1,x2,x3..],[x2,x3,x4..],[x3,x4,x5..]..]<BR/>Don't quite know what this represents though, infinite pasts maybe?nolrai_noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-77629988767695527352008-01-22T09:45:00.000-08:002008-01-22T09:45:00.000-08:00Well , my idea of a "codo" notation would be to si...Well , my idea of a "codo" notation <BR/>would be to simply replace join , return and bind with their comonadic duals in the translation of do notation . Example in the stream comonad described here:<BR/>http://www.cas.mcmaster.ca/~carette/CAS706/F2006/presentations/comonads.pdf<BR/> <BR/>fibo = 1 fby 1 fby <BR/> codo x <- fibo <BR/> ((+) (counit x)<BR/> (counit (next x)))<BR/>It seems to be alright , it has different types from monadic counterpart :<BR/>w a <- w a and it finises with an expression of type aDannoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-59161825626180019072008-01-21T13:47:00.000-08:002008-01-21T13:47:00.000-08:00binaryten,The paper is "The Essence of Dataflow" b...binaryten,<BR/><BR/>The paper is "The Essence of Dataflow" by Uustalu and Vene. But the link isn't broken.<BR/><BR/>For a concrete example of a comonad check out my own "Evaluating cellular automata is comonadic" (http://sigfpe.blogspot.com/2006/12/evaluating-cellular-automata-is.html).sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-55589512977209220392008-01-21T12:24:00.000-08:002008-01-21T12:24:00.000-08:00The link to the 'paper' seems to be out of date. D...The link to the 'paper' seems to be out of date. Do you know of another reference as I would like to have a peruse to see where you are 'coming from' so to speak. Your comments about a reverse abstraction of a monad are extremely curious. Now I know I won't be sleeping early tonight :-)binarytenhttps://www.blogger.com/profile/00026031379066841446noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1162433123796608602006-11-01T18:05:00.000-08:002006-11-01T18:05:00.000-08:00"Silly me...I think I've just figured it out now."..."Silly me...I think I've just figured it out now."<BR/><BR/>Before anyone is misled, I should add that what I figured out wasn't that nice. I think that a nice definition of 'codo' that is dual to 'do' is an open problem.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.com