For anyone interested in iteratees (etc) and not yet on the iteratees mailing list.
I'm asking about what iteratees *mean* (denote), independent of the various implementations. My original note (also at the end below):
With the encouragement & help of Conrad Parker, I've been looking at iteratees, enumerators, enumeratees. I can find plenty written about them, but only about benefits and implementation. In sifting through chunks, error/control messages, and continuations, I find myself longing for a precise semantic basis. I keep wondering: what simpler & precise semantic notions do these mechanisms implement? Has anyone worked out a denotational semantics for iteratees, enumerators, enumeratees -- something that simplifies away the performance advantages & complexities? I've worked out something tentative, but perhaps I'm covering old ground.
Hi Conal,
I've always regarded your work in essentially the same category as Edward Kmett's (and most of Oleg's): stuff that's incredible powerful and concise, but I can't understand at all what it means. I've admired a lot of your work, particularly on Pan, FRP, and automatic differentiation, but most of the rest I couldn't understand at all.
I'll take a look at your Denotational Design paper again; maybe now that I have a lot more experience I'll be able to make sense of it.
JohnOn Sun, Aug 22, 2010 at 8:18 AM, Conal Elliott <conal@conal.net> wrote:
Hi John,
Thanks for the reply. A denotational semantics would be independent of any implementation, so it would apply to any of them, as long as they have the same programming interface. The purpose is to simply & precisely say what the types and their building blocks (API) mean by providing a precise, implementation-independent, and simple-as-possible math model. Such a semantics can be used to prove properties and to define correctness of any implementation. It also gives clear feedback on how elegant or inelegant a library design is.
For instance, given a type, Map k v, of finite maps, we might say the meaning is the type of partial functions from k to v, either k -> v (where absent is _|_) or k -> Maybe v (where absent is Nothing). Then we'd give the meaning of each Map operation as a function of the meanings of its arguments. This example and several others are given in the paper Denotational design with type class morphisms.
Regards, - ConalOn Sun, Aug 22, 2010 at 8:31 PM, John Lato <jwlato@gmail.com> wrote:Hi Conal,
To my knowledge, nobody has attempted this. Oleg may have some ideas, but I don't think he's written about it. I really don't know anything about denotational semantics, so I couldn't do this myself. For some time I've thought it would be good if somebody were able to put together a formal semantics for iteratees, so I'd be very interested if you'd share what you have so far.
Would a denotational semantics apply equally to multiple implementations, or would it be tied to a specific implementation?
JohnOn Sun, Aug 22, 2010 at 3:47 AM, Conal Elliott <conal@conal.net> wrote:
With the encouragement & help of Conrad Parker, I've been looking at iteratees, enumerators, enumeratees. I can find plenty written about them, but only about benefits and implementation. In sifting through chunks, error/control messages, and continuations, I find myself longing for a precise semantic basis. I keep wondering: what simpler & precise semantic notions do these mechanisms implement? Has anyone worked out a denotational semantics for iteratees, enumerators, enumeratees -- something that simplifies away the performance advantages & complexities? I've worked out something tentative, but perhaps I'm covering old ground.
- Conal
_______________________________________________
Iteratee mailing list
Iteratee@projects.haskell.org
http://projects.haskell.org/cgi-bin/mailman/listinfo/iteratee