Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?
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 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. > ... > 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 fricas-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAC6x94TS05s_DnaimYQHgnqGFPeLxZAsYr15_zEDM1R6YGCZMA%40mail.gmail.com.
Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?
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 -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/116f4a2d-e8b3-200a-c761-ad485b4d2def%40martinb.com.
Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?
> 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 -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/00d40019-454e-fe31-f1ad-85ad6e65ec77%40hemmecke.org.
Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?
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 fricas-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit
Re: [fricas-devel] Why are inflexible data structure lengths not always encoded in the type?
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.) On Thu, Oct 29, 2020 at 5:10 PM Neven Sajko wrote: > > 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 > > -- > 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+unsubscr...@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. -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAC6x94Q-_7b57vEVuKMCnRYzSDW%2BEF16X0vjJiOy2wfhFyX%3DfA%40mail.gmail.com.
