iteratee Semantics of s, enumerators, enumeratees?
Conal Elliott
conal at conal.net
Sun Aug 22 09:18:32 EDT 2010
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<http://conal.net/papers/type-class-morphisms/>
*.
Regards, - Conal
On Sun, Aug 22, 2010 at 8:31 PM, John Lato <jwlato at 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?
>
> John
>
> On Sun, Aug 22, 2010 at 3:47 AM, Conal Elliott <conal at 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 at projects.haskell.org
>> http://projects.haskell.org/cgi-bin/mailman/listinfo/iteratee
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://projects.haskell.org/pipermail/iteratee/attachments/20100822/b72479c8/attachment.htm
More information about the Iteratee
mailing list