On Fri, Oct 30, 2020 at 12:46 PM Martin Baker <[email protected]> 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAC6x94TS05s_DnaimYQHgnqGFPeLxZAsYr15_zEDM1R6YGCZMA%40mail.gmail.com.
