[Axiom-developer] Re: [Aldor-l] exports and constants

[Gabriel Dos Reis]

"Antoine Hersen" <address@hidden> writes:

[...]

| Also I do not know much about dependent type, but I think it is a run time
| feature only contrary to polymorphic type.

http://portal.acm.org/citation.cfm?id=292560&coll=Portal&dl=GUIDE&CFID=2132016&CFTOKEN=35552809

http://portal.acm.org/citation.cfm?id=289451&dl=GUIDE&coll=Portal&CFID=2132016&CFTOKEN=35552809

| So how much optimization can we hope to do ? For example can I do unboxing
| for my polynomial if I am not sure that they will be over machine integer at
| compile time ? Do we have to use dynamic language trick ?

for real word programs, this is still a reaserch topic.
So far, from experience, I can tell you that existing technologies are
good at exploiting invariant known at *compile-time*.  This is why
people still loves C or Haskell :-/

[...]

| The type system is quite unique and has some resemblance to modern typed
| language, for example aldor "Category", from far, look like Haskell "class
| type".

only on the surface.

| But from my limited knowledge, type as first class value and dependent type
| his quite unique.

not really.  See above and chase references in there.

| There is a paper about the aldor type system on aldor.com I have not taken
| the time to read it completely but it could be a start even if it only
| represent a subset of Aldor.
| 
| Chapter 18: Recomendation is very interesting.
| 
| I will support the adition of algebraic datatype and I think any addition or
| modification that make Aldor closer to the popular modern functionall
| languages will be welcome.

This is a major addition.  One that I have been thinking of the last
two months.  I just don't know how to do it properly.  And I lack
a precise language description.
Algebraic datatype and "true" pattern matching help write very
readable codes.  Pattern matching is what makes Boot so enjoyable to
read.

| Also some question that come in my mind :
| 
| Do we need a "type system" for the type definition( think Haskell "kind") ?

Yes, we do.

| What about "pretend" is it really needed ? and the special place of Rep, rep
| and per ?

For any serious program yes.  Even, Haskell has unsafe stuff. 

| Is it possible to implement type inferrence ?

We need to have type inference for Aldor (or Axiom if we can wait that
long).  The explicit polymorphism à la System F is just unbearable by
moment. 

| Are any modification needed to make it even more suited for programming
| computer algebra ?

We need way to "reflect" objects -- I'm awaiting Tim's work on pf2sex.
That should bring us a handle on way to better support generic
programming in Axiom.

[...]

| But a very large piece of un documented C code will not be very ususefull if
| nobody with a good knowledge of it is willing and able to spend a lot of
| time on cleaning( I think it does not compile under recent version of gcc),
| writing documentation and debugging( optimization above O1 does not seem to
| preserve semantic).

The same is true for any language, especially Lisp, Boot, or SPAD.

-- Gaby