Lambda the Ultimate

If I remember correctly, Aldor does not allow Vector(3+4) to be simplified to Vector(7). Is that right?

From discussions with the designer of Aldor, Stephen Watt during the Aldor Workshop 2007 in London, Ontario I believe that Jim is correct. On the other hand I am not sure how such simplifications would add to the expressivity or power of the Aldor language - especially since in general we do not have (cannot have?) a strong definition of equality between types.

Probably you are already aware of this publication:

Integrating Computer Algebra and Reasoning through the Type System of Aldor

by Erik Poll and Simon Thompson

Frontiers of Combining Systems (FroCoS'2000), volume 1794 of LNCS, pages 136-150, 2000. © Springer-Verlag

Abstract

A number of combinations of reasoning and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Aldor -- the Axiom Library Compiler -- and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct and explain a prototype implementation of a modified type-checking system written in Haskell.

See: http://www.cs.ru.nl/~erikpoll/publications/frocos2000.html

Logical and Dependent Types in the Aldor Computer Algebra System

Simon Thompson, August 2000.

pdf: http://axiom-portal.newsynthesis.org/refs/articles/aldor-calc2000.pdf

Also: http://www.cs.kent.ac.uk/people/staff/sjt/Atypical

I am not sure of the status of the modifications to Aldor proposed by Thompson et al. Perhaps this is something that can be pursued more easily now that Aldor is available as (semi-)open source.

The reason we chose that static type equivalence be based on (fully dereferenced) syntactic equality was so that all types could be treated the same way. There are a number of benefits that come from having user-defined types able to do everything that a "builtin" type can do.

For example, in a mathematical setting one typically wants to have several different implementations for numeric domains. It would be inelegant to have Vector(3+7) equivalent to Vector(7) for 3,4,7 in a language-defined type, but not for 3,4,7 in a program-defined wrapper for GMP.

With syntactic static equivalence, two types that are statically equivalent are guaranteed to be dynamically equivalent, but not vice versa. In practice this has not been a problem. Typically we have Vector(n) and Vector(3+7) never arises.

The other stance that would allow all types to be treated completely uniformly would be to have all type expressions fully evaluate at compile time. I believe this would lead to worse problems however in the Aldor setting. With the heavy use of mutually recursive and dependent types in the library, we could not have separate compilation with static type checking.

In "Logical and Dependent Types in the Aldor Computer Algebra System"
Abstract. We show how the Aldor type system can represent propositions of first-order logic, by means of the "propositions as types" correspondence. The representation relies on type casts (using pretend) but can be viewed as a prototype implementation of a modified type system with type evaluation reported elsewhere [9]. The logic is used to provide an axiomatisation of a number of familiar Aldor categories as well as a type of vectors.

[9] Integrating Computer Algebra and Reasoning through the Type System of Aldor (op. cit.)

----

Simon Thompson argues in favor of type evaluation for the purposes of implementing a proof system in Aldor. This is especially interesting in the context of Axiom since in effect this actuallys adds the "axiom" concept to Axiom.

In particular

http://www.cs.kent.ac.uk/people/staff/sjt/Atypical/AldorExs/index.html

provides links to programs that implement this logic in Aldor, including for example:

monGrpAx.as -- axiomatising monoids and groups.

In the context of Axiom I find this demonstration rather convincing. The problems of extending this approach to more general programming contexts however might be more severe since appropriate "axioms" may not arise in so natural a manner.

Notwithstanding Curry-Howard, I am unhappy with the fundamental idea of "dependent types" in Aldor. The reason is that deep down I would really like the semantics to have a simple relationship to mathematical category theory. In category theory one of the most basic and primitive notions is that of an arrow

f:A->B

which of course in the context of sufficiently complicated categories becomes the abstraction of the concept of "function". The connection with functions in Aldor is obvious. But if we allow dependent types, this correspondence is no longer so obvious.

It seems to me that such dependencies might better arise in the definition of categorical limits but I have not read anything in the literature on such an approach. Does anyone have a recommendation on where I might find something written the subjection of the categorical semantics of dependent types?