On Wednesday, October 19, 2005 1:09 AM Gaby wrote: > > My current work on designing and implementing a general, > efficient, scalable, complete representation of ISO C++ (with > concepts) in C++ has led me to look at the materials on proof > techniques in Axiom. I've read claims that Type:Type is > inconsistent with types-as-propositions stance. I'm curious > to learn how the type/proof techniques in Aldor would get > away with that. >
I think this is a very interesting question. It relates also to an email exchange a few weeks ago between Peter Broadbery, Ralf Hemmecke, Tim Daly, me and a few others concerning the structure of the upper levels of Axiom's type system. http://lists.gnu.org/archive/html/axiom-developer/2005-09/msg00225.html I think that our conclusion was (at least it was my view :) that Axiom's concept of Category as the type of Domain and Type as a Category is not implemented consistently in the current system. http://wiki.axiom-developer.org/206InterpreterCodeGenerationFailedForFun ctionReturningAType On the following page I tried to summarize Axiom's use of these terms: http://wiki.axiom-developer.org/AxiomLanguage Aldor on the other hand seems to take the concept of types as values more seriously than SPAD but the "two-level object model of categories and domains" still seems to lead to some confusion between domains and types. Here are few more references to "types as values" in the Aldor literature: From: http://www.cs.kent.ac.uk/people/staff/sjt/Atypical/technical.html by Simon Thompson, John Shackell and Erik Poll "A feature of the Axiom/Aldor is that types can be treated as values, so that the type Type is itself a type and so the system allows functions over types, such as the function which taking a type ty to a type of queues over ty, say, or a type of fields F to the category of vector spaces over F." -------- From: http://www.cs.ru.nl/~erikpoll/talks/axiom.pdf by Erik Poll Types as values Alternatively, using Aldor's notation for lambda, polyid : (T:Type)->T->T == (T:Type)(t:T):T +-> t; idType : Type -> Type == (T:Type):Type +-> T; In Aldor, (lambda x:A.b) is written as (x:A):B +-> b -------- Impredicativity and Type:Type The type of the polymorphic identity is a type PolyidType : Type == (T:Type)->T -> T; In fact, Type is a type MyType : Type == Type; MyTypeArrowType : Type == Type -> Type; MyType2 : Type == (polyid Type) Type ; Warning: application associates to the right! ---------- From: http://lists.gnu.org/archive/html/axiom-developer/2005-09/msg00234.html On 26 Sep 2005 16:30:49 +0200 Ralf Hemmecke wrote: Re: [Axiom-developer] types as values But having defined the function tt2 in Aldor like this: #include "axiom.as"; testtype2(): with { tt2: (Integer) -> Type; } == add { tt2(x:Integer):Type == { x=0 => Integer; Float; } } How can I use it in Axiom in a useful manner? ----------- Now specifically about the idea that "Type is a Type" might be inconsistent with types-as-propositions: I think that this is true only in the most restricted definition of what one means by a proposition. Certainly under this definition Type is too "large" to be a Set. But this does not mean that we cannot reason about it's properties using other formal methods, for example by means of equational logic in purely algebraic/ co-algebraic terms. There is quite a large literature about equational proof methods. Lately I have been reading the book "Vicious Circles: On the Mathematics of Non-Well-founded Phenomena" by Barwise and Moss. It seems clear that set theory based on the anti-foundation axiom (AFA) should, in principle provide formal proof methods for dealing with objects such as Aldor's Type. But I do not know of any specific research in this area. In addition, the book discusses the generalization of AFA to greatest fixed points, systems of equations, co-algebras and co-recursion which provide formal methods of reasoning about types such as streams, generators and iterators. It seems plausible to me to suppose that a large part of the mathematical expressiveness of the Axiom and Aldor languages is due to the apparent non-well-foundedness of it's type system. In this sense non-well-foundedness is a good thing: it makes it seem more likely that Type is "large enough" to contain to "all of mathematics" (whatever we might want that to mean :). I hope some of the contents of this email are useful to you and I look forward to hearing your views about Type:Type. Regards, Bill Page. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
