Home » forums » LtU Forum

Algebraist Network

The network of Aldor users and developers at:

would like to promote the development and use of the Aldor programming language by facilitating the interaction between developers and users of the language. Readers of this forum are cordially invited to join this new community.

Aldor is a programming language with an expressive type system well-suited for mathematical computing and which has been used to develop a number of computer algebra libraries. Originally known as A#, Aldor was conceived as an extension language for the Axiom system, but is now used more in other settings.

In Aldor, types and functions are first class values that can be constructed and manipulated within programs. Pervasive support for dependent types allows static checking of dynamic objects. What does this mean for a normal user? Aldor solves many difficulties encountered in widely-used object-oriented programming languages. It allows programs to use a natural style, combining the more attractive and powerful properties of functional, object-oriented and aspect-oriented styles.

(aldor.org)
By billpage at 2008-03-25 15:39 | LtU Forum | previous forum topic | next forum topic | other blogs | 7460 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

"Pervasive support for dependent types"

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

By Jim Apple at Tue, 2008-03-25 17:36 | login or register to post comments

simplification of types

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.

By billpage at Thu, 2008-03-27 18:28 | login or register to post comments

Yes and no

Certain simplifications are perfectly fine. Those for which there are guaranteed terminating algorithms, for example. So pure integer arithmetic is fine.

You can have a strong definition of equality between types, but that has one ``drawback'': that cannot be done algorithmically for what most people consider to be an 'interesting' set of types. So either you generally disallow such things, or you require proof.

And that is really one fundamental design decision behind Aldor: it is a programming language, and programming in it should not require users to write proofs. This is unlike other languages with dependent types, especially Epigram, where proofs are part-and-parcel of programming in it.

The fallacy in Aldor's design is clear to anyone who hangs out here: Curry-Howard. Proofs are already there, they are just called programs.

Such simplifications would definitely add a lot to the safety of the language. Right now, when you implement a Group, the compiler must trust that you did it right. In a language that really has dependent types, you ought to be able to show that, in the language itself. In a way, now that we know that Haskell's type system is Turing complete, we also know that its type system is strictly more powerful than Aldor's, even though Aldor allows types to depend on values and Haskell's does not.

By Jacques Carette at Thu, 2008-03-27 20:11 | login or register to post comments

Papers by Erik Poll and Simon Thompson

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.

By billpage at Fri, 2008-03-28 04:35 | login or register to post comments

Should 3+4 = 7?

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.

By Watt at Fri, 2008-03-28 15:33 | login or register to post comments

Prototype implementation of a modified type system for Aldor

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.

By billpage at Fri, 2008-03-28 17:34 | login or register to post comments

dependent types are bad

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?

By billpage at Sun, 2008-03-30 14:48 | login or register to post comments

Bart Jacobs

Bart Jacobs' book, papers and thesis.

By Derek Elkins at Sun, 2008-03-30 16:01 | login or register to post comments

Perhaps...

Syntax and Semantics of Dependent Types?

By Paul Snively at Sun, 2008-03-30 16:05 | login or register to post comments

Or even...

Or The Groupoid Interpretation of Type Theory, which appeared in the 25 years of Martin-Loef Type Theory book.

I seem to recall that Lambek and Scott argue for type theory as a foundation for category theory in their Introduction to Higher-Order categorical logic, though I can't check that, since I seem to have mislaid my copy.

By Charles Stewart at Mon, 2008-03-31 12:21 | login or register to post comments

The usual way of

The usual way of interpreting type dependency categorically is via locally cartesian closed categories (i.e., a CCC in which every slice category is also a CCC). This approach was introduced by Seely in his 1984 paper "Locally Cartesian Closed Categories and Type Theory". This seems to be on his home page, but the McGill webserver is not responding as I write this message.

By neelk at Sun, 2008-03-30 18:47 | login or register to post comments