On Wed, Apr 2, 2008 at 6:54 PM, Ralf Hemmecke wrote: > ... > I have the impression, you don't like dependent types.
That is correct. I think they spoil the otherwise very simple correspondence between domains/operations in Aldor and objects/arrows in a category. I would like Axiom/Aldor to have a very simple categorical semantics but dependent types make things considerably more complex. See for example the references in reply to: http://lambda-the-ultimate.org/node/2737#comment-40977 > Don't you think that dependent types could be useful for modeling > sheaves of structures? > I am not convinced that dependent types are important for representing sheaves. For sure I am interested in topos theory (a categorical generalization of set theory based on sheaves). Ultimately I would like Axiom (Spad/Aldor) to be support enough categorical constructs to directly represent topoi. In fact Aldor may already be sufficient for this task and Spad is very close. My belief is that doing this will make it possible to represent sheaves without dependent types - but this remains to be demonstrated. > Or suppose you have an index set I and a family of sets (U_i)_{i \in I}. > Let U be the (disjoint) Union of all the U_i and define a function > > f: I -> U > > which has the property that f(i) \in U_i. > This construction can be given a more categorical description: You are saying that f is a segment of the projection of a fiber bundle onto its base space F: U -> I where F f = id(I). Abstracting from it's topological foundations, viewing the mapping F "in reverse" as a bundle of fibers is a fundamental idea in topos theory. > Simply writing I->U tells you nothing about this special property. > Dependent types do. > I agree that dependent types provide more information about a function than is contained in the signatures written without dependencies. The question is: What information do we expect to be available in the types versus that which is available by direct knowledge of the construction? If the type system is too complicated, then using it improperly might also become a source of error. On the other hand, if we have some higher-order operations that construct f as a segment of F then we know it has the properties you specified by the nature and definition of this operation. Saul Youssef referred to this kind of approach to "correctness by design" in his paper on implementing category theory in Aldor: http://axiom-portal.newsynthesis.org/refs/axiombib/webpublishedreference200501181190226284 "We suggest that an axiom that: 'Domain is a category with product, coproduct, initial, final and exponential object' captures what one needs to assume to provide a convenient basis for rigorous arguments about the correctness of Aldor applications." Refs: See especially Slice Categories, Section 6 Page 9, ibid. Also: http://physics.bu.edu/~youssef/homepage/talks/categories/23.html More generally: http://en.wikipedia.org/wiki/Bundle_(mathematics) I think "correctness by design", i.e. by construction, is fundamentally more "algebraic" then logical "proof of correctness" of a program. Notice however that Saul Youssef does make use of dependent types in his Aldor programming. Perhaps if Aldor/Spad took some of these constructions as language primitives so that the representation of category theory is more complete, then the need for dependent types would disappear. Does this all make sense to you? Regards, Bill Page. ------------------------------------------------------------------------- Check out the new SourceForge.net Marketplace. It's the best place to buy or sell services for just about anything Open Source. http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
