> At the most basic and abstract level the reason why I want there to be > a concept of "sub-domain" in FriCAS is so that FriCAS can be formally > modeled as a topos. This means that FriCAS must have limits (e.g. > products such as Record), co-limits (co-products such as Union), > exponentiation (Mapping) and a sub-object classifier. Unions and > sub-objects is where (Boolean) logic enters the system.
So be it. But then there is the general problem. In category theory everything happens 'up to isomorphism', in particular uniqueness. Do you have a suggestion how you would handle that Record(a: A, b: B) is 'isomorphic' with Record(b: B, a: A)? Or, if you like take Cross and don't include the tags a and b. Similarly you had this isomorphism problem in your last mail... NonNegativeInteger = Union(Zero(Integer),PositiveInteger) You must give the compiler a chance to generate exactly the same code for both sides. Until I read a paper that rigorously proves that the topos view on SPAD makes for a better language, I don't believe it. Ralf --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en -~----------~----~----~----~------~----~------~--~---
