[Axiom-developer] Re: [Aldor-l] [Axiom-math] Are Fraction and Complex domains.

[Christian Aistleitner]

Hello,

> > Do you really want a type system whose language is not functional?
>
> Actually, I haven't thought about this. I somehow have the feeling that
> the Aldor compiler implements such a functional type language. But I
> don't know whether this is on purpose.

I do not have this feeling. Quite on the contrary. (Note: we are talking  
about the Aldor compiler, not about the Aldor language)

I came across several situations, where the Aldor compiler gave me error  
messages like:

Dom is of type Cat(Param), but a type Cat(Param) is expected.

So at several places, the compiler did not act functional. However, I  
cannot recollect an example, as such problems occur very rarely, and  
typically you try to get rid of such situations.

Long ago, I discussed these matters with Manuel Bronstein and he said the  
compiler would actually _not_ "know" that Cat(Param) is the same as  
Cat(Param). It would "guess" so by caching. This would at least explain  
why Cat(Param) is mostly equal to Cat(Param) -- "cache hit", but also  
sometimes not equal "cache miss".
However, we did not get too much into the details, as we were discussing  
about garbage collection back then.

Maybe things changed.
Maybe I failed to correctly remember, what Manuel told me.
But from my experience I can tell this pictures suits me well.

So I assume from the compiler point of view, Aldor is not functional.


> > | BTW, I would rather say, Integer is a type constant. If Integer() is
> > | defined and works in Axiom then please show me a definition of the
> > | language that makes it clear that if one defines
> >
> > Please, first, show me how you meaningfully work with a type system
> > where the type language is not functional.

I could give lots of examples, were non-determinism comes into play  
(Randomness of all sorts. Also System specific values -- increasing  
timestamps from real-time clocks, id's of attached USB devices, ...).
But you could possibly always answer "This is poor design, convert this  
into a function within a package. Then the undeterministic part is hidden  
in a function within a domain. So the Domain itself can act functional."

But maybe I do not want to hide those things for whatever reasons?

Additionally, from a language (not compiler!) point of view, I would  
consider
Dom( Param ): Cat == add { ... }
a function. A function of type Param -> Cat whose value is add { ... }.
Nothing else.
Just a plain function -- nothing special about it.

In that manner, it would be pointless to argue that indeterministic parts  
would have to be hidden inside a function of a package. Because a function  
is a function.

To underpin, that the given Dom is a function, look at the attached  
test.as file. It gives you a a domain in the usual domain syntax and the  
usual function syntax. Introducing DomVar in the variant is necessary,  
sinc the compiler causes troubles otherwise. But i'd consider that a  
compiler problem.

To sum it up. From a language point of view, I'd consider a function a  
function in the computer science sense. No need to restrict to the  
mathematical interpretation of a functional relation.

However, I agree that the mathematical sense would sometimes be useful.
In an ideal language, I would probably wish for two different function  
construction mechanisms. One for functional relations, one for functions  
in the computer science sense.
Or at least some marking of functional relations.

> [...]
> shows that Dom and Dom() need not be identical and one can still have a
> consistent type system.

I totally agree.

> I would even call it functional (if Dom() always produces the same
> value). It is only that things of type Cat and things of type ()->Cat
> are not identified even if they happen to have the same name.

And at least I am more than happy with that.

> But of course, I could live with that identification if it is clearly
> documented that ()->Cat can be identified with Cat.

I would not. In a fully typed system, I would not be happy with a thing  
having two types.

--
Kind regards,
Christian

test.as
Description: Binary data