RE: [Axiom-developer] Aldor and Lisp

[Page, Bill]

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.