axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: Gabriel Dos Reis
Subject: [Axiom-developer] Re: [Aldor-l] [Axiom-math] Are Fraction and Complex domains.
Date: 15 May 2006 18:05:29 +0200

"Christian Aistleitner" <address@hidden> writes:

| Hello Gaby,
| 
| On Sun, 14 May 2006 20:56:09 +0200, Gabriel Dos Reis  
| <address@hidden> wrote:
| 
| > If you're after a non-functional type system,
| 
| I think, we all agree that for any programming language, it is good to  
| have _non_ functional functions.
| Just think about a system call time() behaving functional.

Indeed.  I'm not saying the whole language should be functional.  I'm
converned with the type system.

The type system allows for checking that expectations of functions are
met by their arguments.  That checking, and reasoning in general,
requires that we can replace equals for equals. If I defined a
function with a given type (the type is evaluated to some type value), an
later defined a variable or value of the same type (but this time, it
gets evaluated to another type value), how can I even call the
function with that variable?  And if the system let me do it, how can
I prove that the call and the result are sound?

| Besides, I am looking for a language, where same formalisms are treated in  
| the same way.
| For example all functions should be treated equal.

The troubel is terms and types are generally of the "kind".  This
whole point get back the Russell paradox, and solving it is what
prompted Russell to ivnent type theory.  
Even in the Calculus of Construction (of Thierry Coquand), there is a
sort of hierarchy.  It does seem like suppressing those differences
lead back directly to a form of Russell paradox.

| If one function is allowed to behave non-functional, all functions should  
| be allowed to do so.

I suspect there are functions, and functions :-)

| I'd like to model parametric categories and parametric domains by  
| functions, as I described before -- it just seems natural.

I understand the desire. However, my point is that if you have the
notion of terms and types (types are inhabited by terms), then there
must be a distinguishing property.  I suspect that the difference of
"functions" is close to it.

| Since there are non-functional functions, I'd allow all functions to be  
| non-functional.
| 
| So finally, I am maybe after a non-functional type system.
| 
| > please explain
| > clearly what they are useful for, with clear examples.
| 
| My previous examples in this directlions were probably not explicit enough:
| 
| System(): with {
|    timestamp: Integer;
|    cpuTemperature: Integer;
| } == add {
|    timestamp: Integer == { obtain the timestamp somehow }
|    cpuTemperature: Integer == { obtain the timestamp somehow }
| }

If this must be a type, what are the terms that inhabit it?

| 
| Of course, you can rewrite it to
| 
| System: with {
|    grabData: () -> %
|    timestamp: % -> Integer;
|    cpuTemperature: % -> Integer;
| } == add {
|    macro Rep == Record( ts: Integer, temp: Integer );
| 
|    grabData(): % == {
|       per record( obtain the timestamp somehow, obtain the temperature  
| somehow );
|    }
| 
|    timestamp( a: % ): Integer == { (rep a) . ts; };
|    cpuTemperature( a: % ): Integer == { (rep a) . temp; };
| }
| 
| , but would that be better? The latter version is the one we are more used  
| to, but is it really better?

I would claim is it better.  However, I would challenge the claim that
the former is a function that define types.

| To determine the given temperature and timestamp for the system involves 1  
| Function call for non functional Domains and 3 for functional Domains.
| 
| Of course, you can do a lot of rewriting tricks to say "non functionality"  
| is not needed.
| Of course, you can introduce a lot of "this is bad design" axioms to say  
| "non functionality" is not needed.

My objections are not at the level of rewriting or "this is bad
design" argument.  They are more fundamental. 

[...]

| > Explain also
| > how one reasons with such type system, how one writes relaible program
| > with such a type system.
| 
| Could you give an example in the functional world of what you mean by  
| "reason"?

By "reason", I meant essentially proof as in.

    http://www.nuprl.org/
    http://coq.inria.fr/
    http://www4.in.tum.de/~nipkow/LNCS2283/


If I do not have a functional type system, how am I supposed to do 
"separate compilation"?  How am I supposed to do calls?

-- Gaby




reply via email to

[Prev in Thread] Current Thread [Next in Thread]