Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?

2020-10-31 Thread Bill Page
On Fri, Oct 30, 2020 at 12:46 PM Martin Baker 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

Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?

2020-10-30 Thread 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

Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?

2020-10-30 Thread 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

Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?

2020-10-30 Thread 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

Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?

2020-10-29 Thread 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

[fricas-devel] Why are inflexible data structure lengths not always encoded in the type?

2020-10-29 Thread 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