I have started using the language Idris instead of Axiom/FriCAS because the type system seems more powerful to me. However I could be wrong and its important to challenge ones assumptions so, if anyone has time to read this missive, I would welcome your thoughts.
The type system in Axiom/FriCAS apears to me to limit the things I can do. I am not critisising the authors, past and present, it is amazing that decades after it was written only now can the posibility that other languages may be overtaking it in some areas be considered. I am only considering the type system here, as a CAS I still think Axiom/FriCAS is the best.
One area where other languages type systems are better is catagery theory constructs such as monads. This was discussed here:
https://www.euclideanspace.com/prog/scratchpad/spad/topics/category/monad/
or here:
https://groups.google.com/d/topic/fricas-devel/7Nf3obGnvO4/discussion
Here I would like to disuss some simpler aspects and I think vectors give one of the simplest examples to explain my thinking.
Axiom/FriCAS supports dependant types and one of the simplest and best known examples of the use of dependant types is vectors. For example, if we are adding two vectors, using dependant types allows us to check that the vectors are the same length at compile time rather than possibly getting an error at runtime.
So why doesn't Axiom/FriCAS use dependant types for vectors and matrices? Surely, if we want to make our code as reliable as possible, we want to take every opportunity to catch errors at compile time. Isn't that why we use static types?
If carrying around the length at the type level is a problem for Axiom/FriCAS when using vectors then surely the situation will be even worse for more complicated dependant types.
One issue is that, in the general case, we cant determine if two values are equal at compile time but in many (most?) cases we can. If Axiom/FriCAS can't determine that the two lengths are equal then it can fall back to checking at runtime. I assume this issue would be the same for any use of dependant types so I guess this is not a special issue for vectors.
I posted the following here.
For me one of the great advantages of static types is that more errors are found at compile time rather that runtime. When we combine this with dependent types it means that we can detect, for example, attempts to add vectors of different lengths at compile time rather than runtime.
So why doesn't Axiom/FriCAS use dependent types for vectors and matrices? Surely, if we want to make our code as reliable as possible, we want to take every opportunity to catch errors at compile time? If carrying around the length at the type level is a problem for Axiom/FriCAS when using vectors then surely the situation will be even worse for more complicated dependent types.
One issue is that, in the general case, we cant determine if two values are equal at compile time but in many (most?) cases we can. If Axiom/FriCAS can't determine that the two lengths are equal then it can fall back to checking at runtime. I assume this issue would be the same for any use of dependent types so I guess this is not a special issue for vectors.
I think there are genuine reasons why the original designers chose not to do this and I would like to investigate this here. I think the reason comes down to limitations in the type system in Scratchpad/Axiom/FriCAS and that languages like Idris are only now coming up with type systems that make this sort of thing practical. (I am not criticising here, quite the opposite, its amazing that after so many decades only now have the type systems in a few other programs caught up in some respects)
So to help me think through the issues I will try to work out how this might be done. So we could define a type VectorFL (for vector fixed length) like this:
VectorFL(R : Ring, Len : NNI) : Exports == Implementation where
So now we can define an addition function:
+ : (%, %) -> %
So we want this to type match if the lengths are all the same. Imagine we have instances of the following types, which ones can we add?
- a: (VectorFL Double 3)
- b: (VectorFL Double (1 + 2))
- c: (VectorFL Double x)
- d: (VectorFL Double (0 + x))
- e: (VectorFL Double (x + 0))
- f: (VectorFL Double (x + y))
(Where x & y are variables that can't be assigned a value at compile time.)
- 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).
- c + d would compile in Idris because they normalise to the same thing (again they are definitionaly equal) I don't know about FriCAS.
- c + e would not compile automatically in Idris but they can be made to compile by manually providing a proof that x = x + 0 (in Idris they are propositionaly equal).
- (note the importance of having a proof system built into the language - I like Tim's aim of making things provable but I think this is a strong argument that this needs to be built into the language and not a separate language)
- e + f we may not be able to determine this at compile time if y depends on some complex recursion. Perhaps the program could drop back to checking at runtime however in Idris if the above version won't compile then an alternative form needs to be provided like this:
+ : (%, %) -> Maybe %
I think this is a much better way of doing it only for the case where equality of lengths cant be proven.
So far we have just considered + which is relatively simple because all we have to do is check that all types are the same. However when we are working with different length vectors in the same signature we move up to a higher complexity. For example consider concat:
concat : ((VectorFL Double x), (VectorFL Double y)) -> (VectorFL Double (x + y))
Here we can't use % because each vector has a different length. We need to check that the length of the result is the sum of the lengths of the two operands. This sort of thing may not be needed much for vectors but when we go to matrices it is more important. For example when we are multiplying two matrices the operands can have different dimensions provided the number of rows in one is the same as the number of columns in the other.
The Idris language can handle all these sort of things very simply without any extra syntax.
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.
So, in Axiom/FriCAS, these errors are detected at runtime not compile time.
(1) -> vector([1,2,3])+vector([4,5]) >> Error detected within library code: Vectors must be of the same length
So to help me think through the issues I will try to work out how this might be done. So we could define a type VectorFL (for vector fixed length) like this:
VectorFL(R : Ring, Len : NNI) : Exports == Implementation where So now we can define an addition function: + : (%, %) -> %
I don't know if there is anything like this already in Axiom/FriCAS? There are some domains in https://github.com/fricas/fricas/blob/master/src/algebra/array1.spad like this one:
IndexedFlexibleArray(S : Type, mn : Integer) : Exports == Implementation where
But I don't think thats what I want? I think its intended to be mutable like this which wasn't quite what I had in mind:
growWith : (%, I, S) -> %
growWith(r, n, x) ==
y := new(n::N, x)$PrimitiveArray(S)
a := r.f
for k in 0 .. r.physLen-1 repeat y.k := a.k
r.physLen := n
r.f := y
r
from: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect.idr
So why doesn't Axiom/FriCAS use dependant types for vectors and matrices? Surely, if we want to make our code as reliable as possible, we want to take every opportunity to catch errors at compile time. Isn't that why we use static types?
In Idris a vector can be defined like this:
||| Vectors: Generic lists with explicit length in the type ||| @ len the length of the list ||| @ elem the type of elements data Vect : (len : Nat) -> (elem : Type) -> Type where ||| Empty vector Nil : Vect Z elem ||| A non-empty vector of length `S len`, consisting of a head element and ||| the rest of the list, of length `len`. (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
We can then define an addition operation on it. It actually seems to be done indirectly like this
implementation Num a => Num (Vect n a) where (+) = zipWith (+)
From Idris-dev/libs/contrib/Data/Matrix/Numeric.idr
but lets assume its defined more directly like this:
(+) : (Vect n a) -> (Vect n a) -> (Vect n a)
Where 'n' and 'a' are type variables
Idris uses algebraic types. see this page for theory.
Rewrite Rules
https://github.com/fricas/fricas/blob/master/src/algebra/rule.spad