|
From: | Christian Aistleitner |
Subject: | [Axiom-developer] Re: [Aldor-l] [Axiom-math] Are Fraction and Complex domains. |
Date: | Tue, 16 May 2006 12:09:52 +0200 |
User-agent: | Opera Mail/9.00 (Linux) |
Hello,
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?
I designed the some really bad case for functional type systems and implemented it assuming Aldor would be functional (function.as) and assuming it is not functional (not_functional.as).
I do not see any problems with reasoning in both examples. As I already explained in my previous mail:
You can use a functional type system to simulate a non functional one.And you claim it is possible to reason in a functional type system (which I do not doubt).
So, using your method of reasoning and my method of expressing non functionality by a functional type system allows you to reason in a non functional type system.
You can reason in a system with List( Integer ) and List( Character ) being different. So it should not be a problem to reason in a system with List( Integer, timestamp ) and List( Integer, different timestamp ).
| 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".
Sorry, but I am not familiar with the word "term" in this context. You probably do not mean terms as used for polynomials and probably also not term as in "mathematical expression" or as used in formal grammars.
Since large parts of your mail deal with "term" I'd better postpone the rest of my answer until I understand what you mean by "term".
-- Kind regards, Christian
functional.as
Description: Binary data
non_functional.as
Description: Binary data
[Prev in Thread] | Current Thread | [Next in Thread] |