[Aldor-l] [fricas-devel] Re: Indexed Union

[David Casperson]

Bill Page wrote:

> Subject: Re: [Aldor-l] [fricas-devel] Re: Indexed Union
> 
> 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:

[more thoughtful comments on sheaves and co-products elided]

I think that a far more fundamental question is "what is the
relationship between the object- and the meta-language?"  In this
case the meta-language is Aldor in which we express ideas and
algorithms about mathematics of interest.

As category theory is very expressive it is tempting to view all
mathematics as applied category theory and say that the objects
that we want to talk about: rings, Lie algebras, etc., are
categories.  That would make category theory the object
language.  This doesn't necessarily imply anything about the
meta-language, except that it ought to be able to manipulate the
things of the object language easily.

To be more explicit about my fear here, let me give an example:
Maple completely confounds the notion of variable in the object
language of mathematics with the notion of programming variable.
This has the upside of making the user interface easy to
understand and makes simple Maple programming easy.  On the other
hand, writing robust programs that operate correctly in the
presence of possible assignments to "mathematical" variables is
hellishly difficult.

Translated back into Aldor, the category theoretic constructions
that we want to talk about need not necessarily be the category
theoretic constructs that we want to use to talk about category theory.

None of this is to say yea or nay to dependent types.  But we
ought to think about whether we are designing the type system of
Aldor to be easy to reason about (as in SE or formal proofs of
correctness), or whether we are designing it to cleverly mirror
some object language.  It isn't a priori the case that these two
goals lead to the same thing.

My two (Canadian) cents worth.

David
-- 
Dr. David Casperson, Assistant Professor     |  casper at unbc.ca
Department of Computer Science               |  (250)   960-6672 Fax 960-5544 
College of Science and Management            |  3333 University Way
University of Northern British Columbia      |  Prince George, BC   V2N 4Z9
                                              |  CANADA