Hello,
My name is Joie Murphy and I am a Summer Research Student at the US National Institute of Standards and Technology (NIST), working with Drs. Spencer Breiner and Eswaran Subrahmanian. We are currently gathering user requirements for category theoretic software to be developed by or with NIST in the future. This questionnaire will give us insight about your past or present use of CT software and your ideal uses for such software. Providing us with the information on how you would like to use this type of software will help us to make the right design choices in development.
The survey is available on Google Forms: http://goo.gl/forms/vfOgR26dHnKynHU23
If you have any colleagues who might be willing to fill out this survey, you can forward our message or you can provide us with their contact information at the end of the survey. If you have any questions or concerns, please feel free to contact us by replying to this email.
We would like to thank you for your participation in this initial step of the development process.
Regards,
Joie Murphy
Carter,
Thanks for your reply. I removed the Haskell mailing list from the cc because I don’t know the list’s etiquette, but please forward this response back to the list if you are aiming for a public discussion.
I’m not quite sure what you mean by “extensional elements”? Is this extension in the sense of “one class extends another” (in which case this would be expressed explicitly by functors). Or extension in the (related) sense of “the extension of a proposition”, the elements which satisfy it. These sorts of issues would probably be expressed as functors into (some computational implementation of) finite sets.
Let me know and I’m happy to talk some more.
Thanks again,
Spencer Breiner
NIST
Carter,
Hi. This is Spencer Breiner; I am Joie’s supervisor here at NIST. Extensionality is certainly an issue when we are talking about categorical models of type theory, but I don’t see it as such an issue here (which could just be lack of insight).
Certainly it would depend on which type of functional component in the software is involved. In the simplest case, defining a finite category of paths from a directed acyclic graph poses no problems; ditto for path equations in the finite case.
Of course, once we allow cyclic graphs we can get infinite categories, and (if I remember correctly) path equations becomes semi-decidable. In particular, we really need to distinguish between the abstract category and its presentation in terms of generators and relations.
Whether this is a problem or not depends on what we want to do with the category. Functors out are no problem, functors in might be. The real issue seems to be whether you need and are able to check equalities between arrows. Where it does arise, I suspect the solution would be something like in HoTT, where we use computer-aided proof search to verify the equations that we need. Are there particular sorts of things that you would like to do with categories (besides modeling type theory ;-), where you think these sorts of issues would probably arise?
For the work with Joie we are focused on user interface and functional requirements, but I am very interested in these sorts of questions.
Thanks,
Spencer