login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for FriCAS language revision 2 of 2

1 2
Editor: page
Time: 2013/04/28 19:35:45 GMT+0
Note:

changed:
-Axiom has the [Axiom interpreter] for interaction with the
-user and the [Axiom compiler] for building library modules.
-
-Axiom Types
-
-  Types are one of the most important concepts in Axiom.
FriCAS has the [FriCAS interpreter] for interaction with the
user and the [FriCAS compiler] for building library modules.

FriCAS Types

  Types are one of the most important concepts in FriCAS.

changed:
-languages, types in Axiom are dynamic objects: they are
languages, types in FriCAS are dynamic objects: they are

changed:
-  The Axiom interactive language is oriented towards
-ease-of-use. The [Axiom interpreter] uses type-inferencing
  The FriCAS interactive language is oriented towards
ease-of-use. The [FriCAS interpreter] uses type-inferencing

changed:
-  The [Axiom compiler] language (version 1 of the language
  The [FriCAS compiler] language (version 1 of the language

changed:
-Type Inference in the Axiom Interpreter
Type Inference in the FriCAS Interpreter

changed:
-It is sort of interesting, isn't it, that Axiom insists on
It is sort of interesting, isn't it, that FriCAS insists on

changed:
-Axiom is very strict with types (meaning: that it must be
FriCAS is very strict with types (meaning: that it must be

changed:
-example?).  So Axiom provides the user a way to "coerce" an
example?).  So FriCAS provides the user a way to "coerce" an

changed:
-  In Axiom the concept of "Type" is universally applied at
  In FriCAS the concept of "Type" is universally applied at

changed:
-Domains are defined by Axiom by programs of the form::
Domains are defined in FriCAS by programs of the form::

changed:
-      add Rep == RepDomain
      add Rep := RepDomain

changed:
-In Axiom domains and subdomains are themselves objects that
In FriCAS domains and subdomains are themselves objects that

changed:
-is 'Category'. The type of 'Type' itself is undefined. For
-example: the domain 'List' is able to build "lists of elements
is 'Category'.  Since 'Type' is a category its type is 'Category'.

\begin{axiom}
typeOf(Type)
typeOf(typeOf(Type))
\end{axiom}

The second result above indicates that currently FriCAS thinks that
type of 'Category' is again 'Category'.  However, it is safer
to treat is as undefined, because any definition leads to
paradoxes.

For example of parametric type: the domain 'List' is able to build "lists of elements

changed:
-expression to Axiom. This looks much like a function call
-as well. It is! The result is stated to be of type 'Domain',
-which denotes the collection of all domains.
expression to FriCAS. This looks much like a function call
as well. It is! The result is stated to be of type 'Type'.

removed:
-But note well that 'Domain' is a domain but 'Type' is a
-category. !!!?
-

changed:
-  Many Axiom operations have the same name but different
  Many FriCAS operations have the same name but different

removed:
-In light of the above definitions of 'Type' in Axiom, it
-would seem that the type of
-\begin{axiom}
-I:=Integer
-\end{axiom}
-
-which Axiom prints as 'Domain' is actually a 'Category'.
-That certainly is confusing terminology... I guess we just
-have to remember that whenever we see 'Type: Domain' what
-Axiom really means is 'Type: SomeCategory(...)'.
-

changed:
-As #209 reports, Axiom internally generates a call to the
-function '|Domain|' and then fails with an undefined. That
-seems peculiarly broken to me and I wonder if the last
-commercial version of Axiom has this same behaviour or was
-something lost in the porting to the open source gcl-based
-version? I thorough search of the current Axiom sources did
-not turn up any function, package or domain named 'Domain'.
-
-From BillPage Thu Sep 29 14:12:59 -0500 2005
-From: Bill Page
-Date: Thu, 29 Sep 2005 14:12:59 -0500
-Subject: The domain Domain?
-Message-ID: <20050929141259-0500@wiki.axiom-developer.org>
-
-There are numerous places in the Axiom BOOT code that seems to
-treat this name in a special manner as if it might be "built-in".
-Eg. ::
-
-  interp/bootfuns.lisp.pamphlet:(def-boot-val |$Domain| '(|Domain|)        
-  interp/br-con.boot.pamphlet:    is [[h,:.],:t] and MEMBER(h,'(Domain SubDomain))
-  interp/clammed.boot.pamphlet:  form in '((Mode) (Domain) (SubDomain (Domain))) = 
-  interp/g-cndata.boot.pamphlet:      domain in '((Mode) (Domain) (SubDomain (Doma
-  interp/i-analy.boot.pamphlet:  if ( oo = "%" ) or ( oo = "Domain" ) or ( domainF
-  interp/i-coerce.boot.pamphlet:    t1 in '((Mode)  (Domain) (SubDomain (Domain))) =>
-  interp/i-funsel.boot.pamphlet:  MEMBER('(SubDomain (Domain)),types1) => NIL
-  interp/i-output.boot.pamphlet:  categoryForm? domain or domain in '((Mode) (Domain) (SubDomain (Domain))) =>
-  interp/i-spec1.boot.pamphlet:  saeTypeSynonymValue := objNew(sae,'(Domain))
-  interp/i-spec1.boot.pamphlet:  objMode triple = '(Domain) => triple
-  interp/i-spec1.boot.pamphlet:      objMode(val) in '((Domain) (SubDomain (Domain))) =>
-  interp/i-spec2.boot.pamphlet:    else if categoryForm?(type) then '(SubDomain (Domain))
-  interp/i-spec2.boot.pamphlet:  type in '((Mode) (Domain)) => '(SubDomain (Domain))
-  interp/parse.boot.pamphlet:        and m in '((Mode) (Domain) (SubDomain (Domain))) => D
-  interp/setq.lisp.pamphlet:  CAPSULE |Union| |Record| |SubDomain| |Mapping| |Enumeration| |Domain| |Mode|))
-  interp/setq.lisp.pamphlet:(SETQ |$Domain| '(|Domain|))
-  interp/sys-pkg.lisp.pamphlet:    BOOT::YIELD BOOT::|Polynomial| BOOT::|$Domain| BOOT::STRINGPAD
-  interp/trace.boot.pamphlet:      (objMode value in '((Mode) (Domain) (SubDomain (Domain)))) =>
-
-However in searching for use and meaning of the domain 'Domain',
-in all the Axiom algebra library I can find only one place that
-explicity uses this domain.
-
-In 'algebra/forttyp.spad.pamphlet' in the domain 'TheSymbolTable'
-it reads::
-
-    Entry : Domain  := Record(symtab:SymbolTable, _
-                              returnType:FSTU, _
-                              argList:List Symbol)
-
-For details see [SandBox Domains And Types].
-
-So apparently at least in 1992, such a domain might have existed
-in Axiom.
-
-Oddly (or perhaps as we might expect :) compiling this code in
-the current version of Axiom produces some error messages::
-
-   Semantic Errors: 
-      ![1]  Domain is not a known type
-      ![2]  void is not a known type
-
-yet the compile does apparently successfully complete. But
-does it work?
-

Bill also discussed use of 'Domain' in Spad code. For details see [SandBox Domains And Types].



FriCAS has the FriCAS interpreter for interaction with the user and the FriCAS compiler for building library modules.

FriCAS Types

Types 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 Interpreter

Consider

fricas
(1+2)/3

\label{eq1}1(1)
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
Cannot convert the value from type Fraction(Integer) to Integer .

But for this example it is:

fricas
((1+2)/3)::Integer

\label{eq2}1(2)
Type: Integer

FriCAS 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 Fraction Integer (field of rational numbers) and that is where the answer will be, even if it is 1. Most people would automatically "retract" this to the integer 1. But in general, there is no natural way to do so (why not retract 1 to a natural number, for example?). So FriCAS provides the user a way to "coerce" an answer to another type. You can coerce 1 to any of many, many types, for example, as a polynomial, or even as a matrix (or the unit element of any ring).

fricas
((1+2)/3)::Polynomial Integer

\label{eq3}1(3)
Type: Polynomial(Integer)
fricas
((1+2)/3)::SquareMatrix(1,Integer)

\label{eq4}\left[ 
\begin{array}{c}
1 
(4)
Type: SquareMatrix?(1,Integer)
fricas
((1+2)/3)::SquareMatrix(3,Integer)

\label{eq5}\left[ 
\begin{array}{ccc}
1 & 0 & 0 
\
0 & 1 & 0 
\
0 & 0 & 1 
(5)
Type: SquareMatrix?(3,Integer)
fricas
((1+2)/3)::SquareMatrix(3, Polynomial Complex Integer)

\label{eq6}\left[ 
\begin{array}{ccc}
1 & 0 & 0 
\
0 & 1 & 0 
\
0 & 0 & 1 
(6)
Type: SquareMatrix?(3,Polynomial(Complex(Integer)))

Types of Objects, Domains, and Categories

In 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 typeOf -1 is inferred by the interpret to be Integer and the typeOf the variable x:Integer is declared to be Integer. Similarly the typeOf "daniel" is String. The type of an object, however, is not unique. The type of integer 7 is not only Integer but also NonNegativeInteger, PositiveInteger, and possibly, in general, any other subdomain of the domain Integer.

Domains are defined in FriCAS by programs of the form:

  Name(Parameters): JoinCategorys
    with Exports == Extends
      add Rep := RepDomain
        Implementation 

The Name of each domain is used to refer to the collection of its instances. For example, Integer denotes "the integers", Float denotes "the floating point numbers" etc. For example:

  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 Fraction Integer is QuotientFieldCategory Integer with canonical. The axiom canonical means that equal elements of the domain are in fact identical.

We also say that the domain Fraction(S) extends the domain LocalAlgebera(S,S,S). Domains can extend each other in a circular mutually recursive manner so in general the extended relationship forms a directed graph with cycles.

Fractions are represented as the domain Record(num:S, den:S).

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 Category. The category Name is used to denote the collection of domains of that type. For example, category Ring denotes the class of all rings.

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, the class of algebraic sets. The notions of parents, ancestors, and descendants is clear. Thus ordered sets (domains of category OrderedSet) and rings are also algebraic sets. Likewise, fields and integral domains are rings and algebraic sets. However fields and integral domains are not ordered sets:

  SetCategory +---- Ring ---- IntegralDomain ---- Field
              |
              +----  Finite    ---+
              |                    \
              +---- OrderedSet -----+ OrderedFinite

  Figure 1. A simplified category hierarchy.

Confusion of Type and Domain

The most basic category is Type. It denotes the collection of all domains and subdomains. Note carefully that Type does not denote the class of all types! The type of all categories is Category. Since Type is a category its type is Category.

fricas
typeOf(Type)

\label{eq7}\hbox{\axiomType{Category}\ }(7)
Type: Type
fricas
typeOf(typeOf(Type))

\label{eq8}\hbox{\axiomType{Category}\ }(8)
Type: Type

The second result above indicates that currently FriCAS thinks that type of Category is again Category. However, it is safer to treat is as undefined, because any definition leads to paradoxes.

For example of parametric type: the domain List is able to build "lists of elements from domain D" for arbitrary D simply by requiring that D belong to category Type.

Another example. Enter the type Polynomial (Integer) as an expression to FriCAS. This looks much like a function call as well. It is! The result is stated to be of type Type.

fricas
Polynomial(Integer)

\label{eq9}\hbox{\axiomType{Polynomial}\ } (\hbox{\axiomType{Integer}\ })(9)
Type: Type

Ref: Axoim Book "Chapter 2 Using Types and Modes".

Overloading and Dependent Types

Many FriCAS operations have the same name but different types and these types can be dependent on other types. For example

fricas
)display operation differentiate
There are 15 exposed functions called differentiate : [1] (D,(D3 -> D3),NonNegativeInteger) -> D from D if D has DIFEXT(D3) and D3 has RING [2] (D,(D2 -> D2)) -> D from D if D has DIFEXT(D2) and D2 has RING
[3] (D,NonNegativeInteger) -> D from D if D has DIFRING [4] D -> D from D if D has DIFRING [5] (D,NonNegativeInteger) -> D from D if D has DVARCAT(D2) and D2 has ORDSET [6] D -> D from D if D has DVARCAT(D1) and D1 has ORDSET [7] (D,(D3 -> D3)) -> D from D if D has FFCAT(D2,D3,D4) and D2 has UFD and D3 has UPOLYC( D2) and D4 has UPOLYC(FRAC(D3)) [8] (FullPartialFractionExpansion(D2,D3),NonNegativeInteger) -> FullPartialFractionExpansion(D2,D3) from FullPartialFractionExpansion(D2,D3) if D2 has Join(FIELD,CHARZ) and D3 has UPOLYC(D2) [9] FullPartialFractionExpansion(D1,D2) -> FullPartialFractionExpansion(D1,D2) from FullPartialFractionExpansion(D1,D2) if D1 has Join(FIELD,CHARZ) and D2 has UPOLYC(D1) [10] (GeneralUnivariatePowerSeries(D2,D3,D4),Variable(D3)) -> GeneralUnivariatePowerSeries(D2,D3,D4) from GeneralUnivariatePowerSeries(D2,D3,D4) if D3: SYMBOL and D2 has RING and D4: D2 [11] (D,List(D3),List(NonNegativeInteger)) -> D from D if D has PDRING(D3) and D3 has SETCAT [12] (D,D1,NonNegativeInteger) -> D from D if D has PDRING(D1) and D1 has SETCAT [13] (D,List(D2)) -> D from D if D has PDRING(D2) and D2 has SETCAT
[14] (D,D1) -> D from D if D has PDRING(D1) and D1 has SETCAT [15] (D,(D2 -> D2),D) -> D from D if D2 has RING and D has UPOLYC(D2) and D2 has Join(SRNG, ABELMON)
There are 14 unexposed functions called differentiate : [1] (IntegrationResult(D1),Symbol) -> D1 from IntegrationResult(D1) if D1 has FIELD and D1 has PDRING(SYMBOL) [2] (IntegrationResult(D1),(D1 -> D1)) -> D1 from IntegrationResult( D1) if D1 has FIELD [3] (D,PositiveInteger) -> Union(D,0) from D if D has JBC [4] (D,D1) -> D from D if D has JBFC(D1) and D1 has JBC [5] (OutputForm,NonNegativeInteger) -> OutputForm from OutputForm
[6] (U32Vector,Integer) -> U32Vector from U32VectorPolynomialOperations [7] (U32Vector,NonNegativeInteger,Integer) -> U32Vector from U32VectorPolynomialOperations [8] (SparseUnivariateLaurentSeries(D2,D3,D4),Variable(D3)) -> SparseUnivariateLaurentSeries(D2,D3,D4) from SparseUnivariateLaurentSeries(D2,D3,D4) if D3: SYMBOL and D2 has RING and D4: D2 [9] (SparseUnivariatePuiseuxSeries(D2,D3,D4),Variable(D3)) -> SparseUnivariatePuiseuxSeries(D2,D3,D4) from SparseUnivariatePuiseuxSeries(D2,D3,D4) if D3: SYMBOL and D2 has RING and D4: D2 [10] (SparseUnivariateTaylorSeries(D2,D3,D4),Variable(D3)) -> SparseUnivariateTaylorSeries(D2,D3,D4) from SparseUnivariateTaylorSeries(D2,D3,D4) if D3: SYMBOL and D2 has RING and D4: D2
>> Error detected within library code: index out of range

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
differentiate(sin(x),x)
Function Selection for sin Arguments: VARIABLE(x) -> no appropriate sin found in Variable(x) -> no appropriate sin found in Symbol -> no appropriate sin found in Variable(x) -> no appropriate sin found in Symbol
Modemaps from Associated Packages no modemaps
Remaining General Modemaps [1] D -> D from D if D has TRIGCAT
[1] signature: EXPR(INT) -> EXPR(INT) implemented: slot $$ from EXPR(INT)
Function Selection for differentiate Arguments: (EXPR(INT),VARIABLE(x)) -> no appropriate differentiate found in Variable(x)
[1] signature: (EXPR(INT),SYMBOL) -> EXPR(INT) implemented: slot $$(Symbol) from EXPR(INT)

\label{eq10}\cos \left({x}\right)(10)
Type: Expression(Integer)

Notice that

fricas
EXPR INT has PDRING SYMBOL

\label{eq11} \mbox{\rm true} (11)
Type: Boolean
fricas
SYMBOL has SETCAT

\label{eq12} \mbox{\rm true} (12)
Type: Boolean

Embedding Axiom categories in Axiom domains. --Bill Page, Wed, 28 Sep 2005 21:50:23 -0500 reply
Issue report #209 however shows that perhaps it would be useful to flatten Axiom's two-level object model of categories and domains by embedding Categories into the domain called Domain. This would allow convenient things like evaluating the expression:
  (Integer,Float)

as type Tuple(Domain).

Bill also discussed use of Domain in Spad code. For details see SandBox Domains And Types.