Why are inflexible data structure lengths not always encoded in the type?

[Neven Sajko]

Hello,

While I am slowly learning Fricas, I noticed a pattern (or the lack of
it) that struck me as odd. Namely, some data structure types of fixed
size have constructors which take a parameter to define the size as
part of the type (e.g., SquareMatrix), while others (like Vector) do
not take a parameter that specifies the data structure's fixed length.

Is this an oversight or a product of an intentional decision? Is it
beneficial or detrimental? Is this important at all?

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).

Is there a way to define a function that takes a Vector of length 3 as
input, so the input argument's length would be checked by Fricas
automatically when calling the function?

Thank you,
Neven Sajko

[Bill Page]

Checkout the DirectProduct domain. Granted, this name might not be so obvious.

In a computer algebra system like FriCAS the name "Vector" should
probably be reserved for something with specific mathematical
properties. e.g. as in differential geometry.
But I think that there are some good arguments that the current
implementation of the Vector domain is also less than satisfactory
from this point of view.

There is another group of domains that specifically support various
types of "array" data structures. (Although none of them as far as I
know are fixed length structures.)

> --
> 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 fricas-devel...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAL%2BbK4Pnw5ZrdEmwrpAY2Ocj9LiDSayNg9mgrZBESGjh%2BWL%3DAw%40mail.gmail.com.

[Martin Baker]

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

[Ralf Hemmecke]

> 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

[Martin Baker]

On 30/10/2020 17:29, Ralf Hemmecke wrote:
> 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?

Yes, that is the reason that Idris has a proof system built into the
language, it is completely separate from language constructs like:

if 1+2=3 then ...

where the user can define equality in different ways.

Instead it uses Martin-Löf equality types which only has one
constructor: Refl.

Martin

[Bill Page]

On Fri, Oct 30, 2020 at 12:46 PM Martin Baker <ax8...@martinb.com> wrote:
>
> 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 than 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.
>

In my opinion the static type system of FriCAS (as inherited from
Axiom) is more about enabling ubiquitous polymorphism (function
overloading) than it is about program correctness. In FriCAS the
intended result type as well as the type and number of arguments are
used to disambiguate function calls. This is an important part of
generic programming in FriCAS.

It seems to me that program correctness in FriCAS is usually addressed
at a higher level by "contract and design" rather than "simple" type
correctness. By that I mean that we try to see our specific
programming goals as an instance of something a little more generic
and possibly already existing, i.e. belonging to a particular category
in the FriCAS sense. If nothing close enough exists then we might
start by defining such categories. Then we implement one or more
domains that satisfy these categories by representing it using
existing domains a little lower down in the type heterarchy which
ultimately depends on something built-in (or supplied by the
underlying Lisp). I think this model better fits FriCAS objective as a
high level mathematical computer *algebra* system based on abstract
algebra. I think this purely algebraic approach is largely in contrast
to the logic proof-theoretic approach that you discuss below.

> ...

[Waldek Hebisch]

On Thu, Oct 29, 2020 at 09:10:44PM +0000, Neven Sajko wrote:
>
> While I am slowly learning Fricas, I noticed a pattern (or the lack of
> it) that struck me as odd. Namely, some data structure types of fixed
> size have constructors which take a parameter to define the size as
> part of the type (e.g., SquareMatrix), while others (like Vector) do
> not take a parameter that specifies the data structure's fixed length.
>
> Is this an oversight or a product of an intentional decision? Is it
> beneficial or detrimental? Is this important at all?

Sometimes fixed size is important to have needed mathematical
properties. For example, SquareMatrix with integer coefficients
has ring structure, in particulatr multiplicative 1. This is
only possible for fixed dimension. OTOH variable size
structure are much more convenient and preferable in
"programming" contexts.

>
> 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).

This is problematic. Length of result may be a complicated
function of arguments, then typechecking would be quite complicated.
In FriCAS there is another problem: types exist at runtime,
and it take time to create types and you need memory to store
them. Usually this is not a problem, but computations at
type level are orders of magnitude less efficient than
computations on ordinary values. So one really does not
want to create types at whim. For example, single 'Vector(Integer)'
replaces all types with specified length (wihich could be hundreds
of types in relalistic program).

There are also limits of typechecker: "obviously corrrect" types
mat be rejected by current FriCAS typechecker.

> Is there a way to define a function that takes a Vector of length 3 as
> input, so the input argument's length would be checked by Fricas
> automatically when calling the function?

In general is is quite easy to create fixed length type as
wrapper around variable size type. And efficientcy is quite
good. OTOH trying to create variable size type from
parametric family of fixed size types is quite problematic.

So it is natural to provide mainly variable size types and
create fixed size wrappers when needed. For example main
part of SquareMatrix is just wrapper around variable size
Matrix (but due to math SquareMatrix does not offer some
matrix operations and offers some operations not available
for general matrices).

--
Waldek Hebisch