14 views

Skip to first unread message

Oct 29, 2020, 5:10:57 PM10/29/20

to fricas...@googlegroups.com

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

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

Oct 29, 2020, 6:09:32 PM10/29/20

to fricas-devel

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.

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.

Oct 30, 2020, 12:46:23 PM10/30/20

to fricas...@googlegroups.com

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

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

Oct 30, 2020, 1:29:07 PM10/30/20

to fricas-devel

> a: (VectorFL Double 3)

> b: (VectorFL Double (1 + 2))

...
> 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).
> single number which is equal in this case (in Idris they are

> definitionaly equal).

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.

Ralf

Oct 30, 2020, 2:06:34 PM10/30/20

to fricas...@googlegroups.com

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
> 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?

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

Oct 31, 2020, 9:49:51 AM10/31/20

to fricas-devel

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
>

> 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

> 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
> for example, attempts to add vectors of different lengths at compile

> time rather than runtime.

>

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.

> ...

Nov 1, 2020, 1:20:05 PM11/1/20

to fricas...@googlegroups.com

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
>

> 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?

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

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?

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu