definition of topic and Coq API

[aa755]

For some time, I have been wondering whether a Topic of type T cannot be defined as Node [T]. On a related note, I don't understand the following line from the ICRA11 paper on roshask: "The type we want is not an inductive list, for it is always infinite, nor is it simply a coinductive stream of pure values." IIUC, unlike Coq, Haskell lists should be considered as colists. For example one can write the following in Haskell:

repeatInf:: a -> [a]
repeatInf x = x:(repeatInf x)

More specifically, if someone has time, I would be grateful if they could let me know if something is wrong with the way I exported roshask API to Coq, as explained below.

First I axiomatized the Ros.Node.Node monad in Coq: http://www.cs.cornell.edu/~aa755/ROSCoq/coqdocnew/ROSCOQ.shim.Haskell.RoshaskNodeMonad.html (In this webpage, all colored words are hyperlinked (recursively) to the place they are defined.)

After each axiom is declared, I specify how that construct should be realized in Haskell after extraction. For example, the following line in the above file says that the Axiom nreturn in Coq should be realized by Ros.ROSCoqUtil.nreturn in Haskell.

Extract Constant nreturn => "Ros.ROSCoqUtil.nreturn"

All axioms in Coq are realized by a function in https://github.com/aa755/roshask/blob/master/src/Ros/ROSCoqUtil.hs

Next, I defined the ROSMsgType typeclass at: http://www.cs.cornell.edu/~aa755/ROSCoq/coqdocnew/ROSCOQ.shim.Haskell.RoshaskMsg.html

It has only two functions, which subscribe/publish a CoList in the above defined Node Monad. This corresponds to a haskell definition of topics as Node [T], as I mentioned in the first line.

Finally, I defined Coq types for ROS messages, closely following what roshask generates. One difference, is that instead of defining instances of RosBinary, Typable, e.t.c., it just provides an instance of the above ROSMsgType typeclass. Here is an example, that I wrote down by hand: http://www.cs.cornell.edu/~aa755/ROSCoq/coqdocnew/ROSCOQ.shim.Haskell.ROSStringMsg.html

I wrote an example in Coq to use the above API. http://www.cs.cornell.edu/~aa755/ROSCoq/coqdocnew/ROSCOQ.shim.Haskell.examples.echo.html The last line asks Coq to extract this program to haskell. I found the extract to run as expected.

If something is wrong the way I exported part of the roshask API to Coq, especially if bad things like segfault, memory leaks can happen, please let me know. Any other comments are also welcome.

Thanks, also for replying to my other issue about automatically generating ROS message types in Coq. I will implement that soon.

[acowley]

I'm excited to check out those links! As to the opening verbiage, the point is simply that we have an infinite stream with interleaved effects.

[acowley]

It's entirely possible I'm misunderstanding something, but the way you've organized things around the ROSMsgType class doesn't seem right to me. When you subscribe to a topic, for example, mechanisms parameterized by the topic name kick into action. The subscribing node asks the master about publishers of that topic name, receives information on the endpoints to connect to, and then wires things up so that some kind of stream is initialized.

The way you've set it up here looks like each message type instance is responsible for that connectivity functionality as opposed to just serialization. Large parts of dealing with those node-to-node interactions are independent of the message type.

This probably comes back to me not thinking right about your core suggestion of a topic being a list in the Node monad. I guess the point you're making is that the connectivity functionality is all in Node, but I'm not sure what is gained by defining things like subscribe for each message type when the only unique part is the serialization.

As my first reply suggested, I'd rather not burry the IO in a pure list type on the Haskell side. Yes this can be done with unsafeInterleaveIO, but that encourages people to use tools appropriate for pure lists on these things where getting each new element is relatively slow and expensive. For instance, pattern matching on a topic as though it were a regular list is probably a bad idea as it completely hides the networking in a CORBA-like manner. Instead of this, we provide an API for working specifically with topics that, hopefully, is better tailored to network streams of time-stamped values.

The echo example looks awesome, btw. Being able to write in Coq with such smooth interoperation with roshask's existing plumbing will be a fantastic tool.

[aa755]

Thanks a lot for your feedback.

The way you've set it up here looks like each message type instance is responsible for that connectivity functionality as opposed to just serialization. Large parts of dealing with those node-to-node interactions are independent of the message type.

I agree that subscribe and publish do not belong to the ROSMsgType class, and this class should be only concerned with serialization. However, I did not want to export serialization related details to Coq, at least for the time being. For now, the only thing that serialization buys is the ability to publish or subscribe to topics of that type. Hence I short-circuited one step. I'll try to fix this.

As my first reply suggested, I'd rather not bury the IO in a pure list type on the Haskell side.

I agree, and I have been trying to fix this. Initially, I was stuck trying to mimic in Coq your Haskell definition of Topic, because it seems to violate the strict positivity requirement of CoInductive types: https://github.com/aa755/ROSCoq/blob/92d2cbaff2c832f2a9b9a2256bc0250572b0e9f4/src/shim/Haskell/RoshaskMsg.v#L20 I think I can make Topic axiomatic too, instead of defining it using coinduction, and then export some key topic combinators from roshask to Coq.

[aa755]

Your suggestion to avoid defining a topic as a list in the Node monad was very helpful. Indeed, I encountered deadlocks in the old design. Following your suggestion, I directly axiomatized the Topic type of roshask. http://www.cs.cornell.edu/~aa755/ROSCoq/coqdocnew/ROSCOQ.shim.Haskell.RoshaskTopic.html Deadlocks seem to have disappeared now!