> a: (VectorFL Double 3) > b: (VectorFL Double (1 + 2)) ... > a + b should compile because numeric values can be normalised to a > single number which is equal in this case (in Idris they are > definitionaly equal).
In FriCAS they are not (also not in Aldor). The reason is that no computation is done at compile time. Of course that could be changed if there were a sublanguage that the compiler could execute at compile time. But why would you believe that 3 is the same as 1 + 2? I can surely program NonNegativeInteger in such a way that 1+2 gives 6 (or perhaps 0). Would you then also claim that the type of a and b are the same? Integers are not a built-in type, but they are library-defined. How much of that you tell the compiler to use is a design decision. For FriCAS (and Aldor) the decision was that in types the compiler compares the syntaxes. So VectorFL(INT, 3), VectorFL(INT, 1+2) and VectorFL(INT, 2+1) would be 3 different types (although behaving the same). > So my conclusion from this (unless you tell me otherwise) is that > Axiom/FriCAS needs a more powerful type system (like Idris) to be able > to do this sort of thing simply. You are right. Ralf -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/00d40019-454e-fe31-f1ad-85ad6e65ec77%40hemmecke.org.
