FriCAS has the FriCAS interpreter for interaction with the user and the FriCAS compiler for building library modules. ## FriCAS TypesTypes are one of the most important concepts in FriCAS. Like Modula 2, PASCAL, FORTRAN, and Ada, the programming language emphasizes strict type-checking. Unlike these languages, types in FriCAS are dynamic objects: they are created at run-time in response to user commands. The FriCAS interactive language is oriented towards ease-of-use. The FriCAS interpreter uses type-inferencing to deduce the type of an object from user input. Type declarations can generally be omitted for common types in the interactive language. The FriCAS compiler language (version 1 of the language is called SPAD, version 2 of the language is called Aldor) on the other hand is based on strong static types that must be explicitly specified by the programmer. ## Type Inference in the FriCAS InterpreterConsider fricas (1) -> (1+2)/3
Type: Fraction(Integer)It is sort of interesting, isn't it, that FriCAS insists on calling "1" a fraction just because of the way it was calculated? There is a way to say that you want the answer as an integer. Of course this isn't always possible: fricas (1/3)::Integer But for this example it is: fricas ((1+2)/3)::Integer
Type: IntegerFriCAS is very strict with types (meaning: that it must be
completely unambiguous where each operation takes place).
The division of 1+2 by 3 takes place in fricas ((1+2)/3)::Polynomial Integer
Type: Polynomial(Integer)fricas ((1+2)/3)::SquareMatrix(1,
fricas ((1+2)/3)::SquareMatrix(3,
fricas ((1+2)/3)::SquareMatrix(3,
## Types of Objects, Domains, and CategoriesIn FriCAS the concept of "Type" is universally applied at all levels. From the Axiom Book: Appendix B Glossary - The type of any category is the unique symbol Category.
- The type of a domain is any category to which the domain belongs.
- The type of any other object is either the (unique) domain to which the object belongs or a subdomain of that domain.
- The type of objects is in general not unique.
## From the Axiom Book: Technical Introduction Every Axiom object is an instance of some domain. That
domain is also called the type of the object. Thus the
Domains are defined in FriCAS by programs of the form: Name(Parameters): JoinCategorys with Exports == Extends add Rep := RepDomain Implementation The Fraction(S: IntegralDomain): QuotientFieldCategory S with if S has canonical and S has GcdDomain and S has canonicalUnitNormal then canonical == LocalAlgebra(S, S, S) add Rep:= Record(num:S, den:S) coerce(d:S):% == [d,1] zero?(x:%) == zero? x.num Thus the type of We also say that the domain Fractions are represented as the domain In FriCAS domains and subdomains are themselves objects that have types. The type of a domain or subdomain is called a category. Categories are described by programs of the form: Name(...): Category == JoinCategorys with Exports add Imports Implementation The type of every category is the distinguished symbol
For example: QuotientFieldCategory(S: IntegralDomain): Category == Join(Field, Algebra S, RetractableTo S, FullyEvalableOver S, DifferentialExtension S, FullyLinearlyExplicitRingOver S, Patternable S, FullyPatternMatchable S) with _/ : (S, S) -> % ++ d1 / d2 returns the fraction d1 divided by d2. numer : % -> S ++ numer(x) returns the numerator of the fraction x. denom : % -> S ... if S has PolynomialFactorizationExplicit then PolynomialFactorizationExplicit add import MatrixCommonDenominator(S, %) numerator(x) == numer(x)::% denominator(x) == denom(x) ::% ... Categories say nothing about representation. Domains, which are instances of category types, specify representations. See also Rep And Per. Categories form hierarchies (technically, directed-acyclic
graphs). A simplified hierarchical world of algebraic
categories is shown below. At the top of this world is
SetCategory +---- Ring ---- IntegralDomain ---- Field | +---- Finite ---+ | \ +---- OrderedSet -----+ OrderedFinite Figure 1. A simplified category hierarchy. ## Confusion of Type and Domain The most basic category is fricas typeOf(Type)
Type: Typefricas typeOf(typeOf(Type))
Type: TypeThe second result above indicates that currently FriCAS thinks that
type of For example of parametric type: the domain Another example. Enter the type fricas Polynomial(Integer)
Type: TypeRef: Axoim Book "Chapter 2 Using Types and Modes". ## Overloading and Dependent TypesMany FriCAS operations have the same name but different types and these types can be dependent on other types. For example fricas )display operation differentiate We can see how the interpreter resolves the type: [14] (D,D1) -> D from D if D has PDRING D1 and D1 has SETCAT in the following example fricas )set message bottomup on
Type: Expression(Integer)Notice that fricas EXPR INT has PDRING SYMBOL
Type: Booleanfricas SYMBOL has SETCAT
Type: BooleanSince in FriCAS Type is class of all type one can do fricas (Integer, Type: Tuple(Type)and get |