[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Re: SPAD and Aldor again
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] Re: SPAD and Aldor again |
Date: |
17 Nov 2006 14:39:12 +0100 |
Waldek Hebisch <address@hidden> writes:
| Martin Rubey wrote:
| > C Y <address@hidden> writes:
| >
| > > I think we should make the decision as a project not to wait any longer
for
| > > Aldor, and commit to improving SPAD - up until now I think there has been
| > > hesitation to commit serious effort to SPAD due to the possibility of
Aldor
| > > becoming available and making such work unnecessary. To my mind the first
| > > step to improving SPAD is to decide what SPAD should be, since right now
it
| > > doesn't have a formal language definition.
| >
| > For me this is totally clear: SPAD should become a free implementation of
the
| > Aldor language. It would not make sense to have to different languages
around.
| >
|
| I am affraid we will have two different languages: there are legal reasons
| and technical ones: I do not see why we should limit ourselfs to capabilites
| present in Aldor and (assuming that we want this) implementing _all_
| capabilities of Aldor is likely to take long time.
I agree. I don't believe that the goal of improved SPAD shall be a
clone of Aldor.
[...]
| OTOH design of dependent types in Aldor can be criticised. One thing
| is "Type : Type" (personaly I find this reasonable design choice).
This choice must be explored and studied carefully. Improved SPAD
must ideally have a formal semantics (but, in reallity I suspect we
will only approximate it) and the implications of Type:Type must be
understood, especially since people has expressed many times
connection with proof theory. I don't consider use of "pretend" a
good solution.
| Another is using unevaluated parameters (not doing beta convertion)
| for typechecking (more precisely for deciding type equivalence). However,
| "Type : Type" + equivalence after evaluating parameters would make compile
| time typechecking undecidable.
I'm fine with undecidable type checking in general , as long as we
have identified a large subset where it is decidable.
We must also look at how to convince the compiler to do delta
conversion without getting in a blackhole.
-- Gaby
- Re: [Axiom-developer] Re: SPAD and Aldor again, (continued)
- Re: [Axiom-developer] Re: SPAD and Aldor again, root, 2006/11/20
- Message not available
- [Axiom-developer] GCL and elf-loader, root, 2006/11/21
- [Axiom-developer] Re: GCL and elf-loader, Gernot Hueber, 2006/11/21
- [Axiom-developer] Re: GCL and elf-loader, Gabriel Dos Reis, 2006/11/21
- [Axiom-developer] Re: GCL and elf-loader, Gernot Hueber, 2006/11/21
- Re: [Axiom-developer] Re: SPAD and Aldor again, Antoine Hersen, 2006/11/21
- Re: [Axiom-developer] Re: SPAD and Aldor again, Gabriel Dos Reis, 2006/11/21
- Re: [Axiom-developer] Re: SPAD and Aldor again, Peter Broadbery, 2006/11/21
- Re: [Axiom-developer] Re: SPAD and Aldor again, Ralf Hemmecke, 2006/11/21
- Re: [Axiom-developer] Re: SPAD and Aldor again, Peter Broadbery, 2006/11/21
- Re: [Axiom-developer] Re: SPAD and Aldor again,
Gabriel Dos Reis <=
- [Axiom-developer] Re: SPAD and Aldor again, Gabriel Dos Reis, 2006/11/17
- Re: [Axiom-developer] Re: SPAD and Aldor again, Ralf Hemmecke, 2006/11/17
- Re: [Axiom-developer] Re: SPAD and Aldor again, Gabriel Dos Reis, 2006/11/17
- Re: [Axiom-developer] Re: SPAD and Aldor again, root, 2006/11/17
- Re: [Axiom-developer] Re: SPAD and Aldor again, Martin Rubey, 2006/11/17
- Re: [Axiom-developer] Re: Ping: case insensitive filesystems, Gabriel Dos Reis, 2006/11/17
- Re: [Axiom-developer] Re: Ping: case insensitive filesystems, Waldek Hebisch, 2006/11/17
- Re: [Axiom-developer] Re: Ping: case insensitive filesystems, Gabriel Dos Reis, 2006/11/17
- [Axiom-developer] compiler-improvements, Waldek Hebisch, 2006/11/15
- [Axiom-developer] Re: compiler-improvements, Gabriel Dos Reis, 2006/11/15