On 29/10/2020 21:10, Neven Sajko wrote:
My guess would be that it would be better if Vector's constructor had
a length parameter, because that would enable greater type safety
(i.e. I couldn't pass a Vector of the wrong length to a function).
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.
Martin
--
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/f816ae04-a52a-d45d-7f83-9beb3af80c6d%40martinb.com.
