Types¶
Introduction¶
The axis language is strongly and statically typed: the interpreter first
analyses the expressions and definitions given by the user to verify that
types can be attributed to all subexpressions, and all operations are defined
for the types they are applied to; only if the expression passes this test
does the system attempt to evaluate the expression. Thus many computations
that would produce problems on execution are signaled. For instance, after
loading “groups.at” which defined GL: (int->RootDatum)
, atlas will complain
about:
atlas> block_sizes (GL(5))
Type error:
Subexpression GL(5) at <standard input>:...
has wrong type: found RootDatum while InnerClass was needed.
Type check failed
because the built-in function block_sizes
requires an InnerClass
value but
GL
produces a value of type RootDatum
. In the following example:
atlas> Lie_type(Cartan_matrix(GL(5)))
Error in expression Lie_type(Cartan_matrix(GL(5))) at...
Failed to match 'Lie_type' with argument type mat
Type check failed
the message is somewhat different, because the name Lie_type
corresponds to
several functions, and atlas can only report that none of them applies for
the given expression. To find out which instances are known, one can enter:
atlas> whattype Lie_type ?
Overloaded instances of Lie_type
string->LieType
RootDatum->LieType
(int,int)->LieType
(note the question mark, which here means treat Lie_type
as possibly
overloaded function name rather than as a variable) showing that either a
string
or a RootDatum
value would have worked instead of a (Cartan) matrix
.
For instance:
atlas> Lie_type(GL(5))
Value: Lie type 'A4.T1'
atlas> Lie_type("E6.T1.D4")
Value: Lie type 'E6.T1.D4'
All built-in operators and functions, and normally also all user defined ones,
are defined as “overloaded” symbols (even if only one meaning is built-in, as
is the case for block_sizes
). This allows the user to add new definitions of
those symbols without overriding those built in. On the other hand, the values
of all identifiers that are not functions are stored in a different table,
allowing only one such value at a time to be associated to a given identifier.
Primitive Types¶
The interpreter knows about several “primitive” types, which it distinguishes but for which (in contrast to “composite” types discussed below) it usually does not provide specific language constructions (although it does know for instance that a Boolean value can be tested in a conditional expression). These basic types are:
Primitive Type | Represent |
---|---|
bool | truth values |
int | machine integers (32 or 64 bits) |
rat | rational numbers (quotient of two machine integers) |
string | string of characters |
vec | vector of machine integers |
mat | matrix of machine integers |
ratvec | rational vector (vector numerator with common denominator) |
LieType | Lie type |
RootDatum | root datum, specifying a connected complex reductive group |
InnerClass | inner class of real forms (based root datum with involution) |
RealForm | real form within an inner class |
CartanClass | all the conjugacy classes of Cartan subgroups of real groups in an inner class |
KGBElt | element of the set K\G/B associated to some RealForm value |
Block | block for a pair of RealForm values (at dual inner classes) |
Split | “split integer” a + b.s where s is “split unit” with s^2=1 |
Param | value representing a standard module or its irreducible quotient |
ParamPol | virtual module with signature (Param values with Split coefs) |
T | we use T to represent any type |
Note
If you want to check the data type of something, for example id_mat(3)
. You can do whattype id_mat(3)
in atlas and it will output type: mat
.
bool¶
bool
represents truth values. Values of bool are true
, false
:
atlas> whattype true
type: bool
atlas> whattype false
type: bool
string¶
string
represents string of characters. String values can be entered using a double quote:
atlas> set s = "atlas"
Variable s: string
Strings denotations contain newline characters (but a constant ‘new_line’ is provided, containing a string with a single newline character). Values of other basic types can only be obtained by using appropriate operators and functions (for instance 22/7 has type ‘rat’ and GL(5) has type ‘RootDatum’), or sometimes via implicit conversions.
int, rat, & vec¶
int
represents machine integers (32 or 64 bits);rat
represents rational numbers (quotient of two machine integers);vec
represents vector of machine integers.
As you might expect, the sum of a int
type and rat
type is a rat
type:
atlas> set a = 2
Variable a: int
atlas> set b = 1/2
Variable b: rat
atlas> whattype a+b
type: rat
Similarly, if you add a vec
type and an array of int
, whenever possible, the result is of type vec
:
atlas> set v = vec:[1,2,3]
Variable v: vec
atlas> set w = [3,4,5]
Variable w: [int]
atlas> whattype v+w
type: vec
mat¶
mat
represents matrix of machine integers.
If you directly enter [[1,2],[3,4]]
, the type would be set to [[int]]
. You need to specifically declare the type mat
if you want [[1,2],[3,4]]
to be a matrix:
atlas> set m = mat : [[1,2],[3,4]]
Variable m: mat
Identity matrix of dimension n is a build-in expression. Suppose \(n=3\):
atlas> id_mat(3)
Value:
| 1, 0, 0 |
| 0, 1, 0 |
| 0, 0, 1 |
ratvec¶
ratvec
represents rational vector (vector numerator with common denominator).
There are two basic ways to declare a rational vector:
atlas> set v = [1,2,3]/5
Variable v: ratvec
atlas> set w = ratvec:[1/2,3/5]
Variable w: ratvec
You can also make array of rational numbers [rat]
:
atlas> set w = [1/2,3/5]
Variable w: [rat]
Similar to int
, if you add a ratvec
to [rat]
, the result is ratvec
:
atlas> set v = [1,2,3]/5
Variable v: ratvec
atlas> set w = [1/2,3/5, 5/7]
Variable w: [rat]
atlas> whattype v+w
type: ratvec
LieType¶
LieType
represents Lie types.
An example of a valid Lie type is “A1.T1”:
atlas> set l = LieType : "A1.T1"
Variable l: LieType
RootDatum¶
RootDatum
represents root datum, specifying a connected complex reductive group.
In atlas, a root datum is a pair of \(m\times n\) (integral) matrices \((A,B)\) such that \(A^T*B\) is a Cartan matrix. The number m is rank (number of rows) and n is the semi-simple rank (number of columns). One way to define a RootDatum
is to use LieType
:
atlas> set rd = simply_connected(LieType:"A1.T1")
Variable rd: RootDatum
InnerClass¶
InnerClass
represents inner class of real forms (based root datum with involution).
One can think of an inner class as a set of real forms (of a certain complex Lie group) that share some properties. One can define an inner class in atlas as:
atlas> inner_class(SL(2,R))
Value: Complex reductive group of type A1, with involution defining
inner class of type 'c', with 2 real forms and 2 dual real forms
atlas> whattype inner_class(SL(2,R))
type: InnerClass
RealForm¶
RealForm
represents real form within an inner class.
A simple way of specifying a real form is:
atlas> set G = Sp(4,R)
Variable G: RealForm
This is enabled by the various user-defined scripts in “atlas-scripts” folder.
If furthermore you want to see all real forms that are in the same inner class as \(Sp(4,R)\), do:
atlas> real_forms(G)
Value: [compact connected real group with Lie algebra 'sp(2)',
connected real group with Lie algebra 'sp(1,1)',
connected split real group with Lie algebra 'sp(4,R)']
CartanClass¶
CartanClass
represents all the conjugacy classes of Cartan subgroups of real groups in an inner class.
For a specific real group \(G = Sp(4,R)\), one can ask atlas what are the Cartan classes that are in the same inner class:
atlas> set G = Sp(4,R)
Variable G: RealForm
atlas>
atlas> Cartan_classes(G)
Value: [Cartan class #0, occurring for 3 real forms and for 1 dual real form,
Cartan class #1, occurring for 2 real forms and for 1 dual real form,
Cartan class #2, occurring for 1 real form and for 2 dual real forms,
Cartan class #3, occurring for 1 real form and for 3 dual real forms]
atlas>
atlas> whattype Cartan_classes(G)[1]
type: CartanClass
The reference to ‘dual real forms’ concerns the various blocks of representations for which each Cartan class appears.
KGBElt¶
KGBElt
represents element of the set \(K\backslash G/B\) associated to some RealForm value.
Given a group \(G\), for example \(G = SL(2,R)\). One can ask atlas to print out the KGB elements associated to different Cartan involutions:
atlas> set G = SL(2,R)
Variable G: RealForm (overriding previous instance, which had type RealForm)
atlas> KGB(G)
Value: [KGB element #0,KGB element #1,KGB element #2]
atlas> KGB(G,0)
Value: KGB element #0
Block¶
Block
represents block for a pair of RealForm values (at dual inner classes).
atlas> set G = SL(2,R)
Variable G: RealForm (overriding previous instance, which had type RealForm)
atlas> blocks(G)
Value: [Block of 1 elements,Block of 1 elements,Block of 3 elements]
atlas> whattype blocks(G)[0]
type: Block
Split¶
Split
represents “split integer” \(a + b.s\) where \(s\) is “split unit” with \(s^2=1\).
Param¶
Param
represents value representing a standard module or its irreducible quotient.
ParamPol¶
ParamPol
represents virtual module with signature (Param values with Split coefs).
Composite Types¶
Composite types are either array (list) types, tuple types or function types. Array and tuple types both construct aggregates by combining a sequence of component values. The difference is:
- for array types all components must have the same type and there could be any number of them (including none at all);
- for tuple types the type explicitly enumerates the (may-be-different) types of the components, so in particular the number of components is determined by the type.
A function type specifies zero or more argument and result types; for either, unless exactly one such type is specified, the argument or result type is actually a tuple type. Thus if t0,t1,t2,t3 are types, one has composite types like:
Composite Types | Represents |
---|---|
[t0] |
array of elements all of which have type t0 |
[[t0]] |
array of elements all of which have type [t0] (a list of lists) |
… | etc |
(t0,t1) |
2-tuple formed of components of types t0 and t1 respectively |
(t0,t1,t2) |
3-tuple, with components of types t0,t1,t2 respectively |
(t0,t1,t2,t3) |
4-tuple, with components of types t0,t1,t2,t3 respectively |
… | etc |
void |
0-tuple (irrelevant value) |
(t0->t1) |
function with argument of type t0 and result of type t1 |
(t0,t1->t2) |
function with argument of type (t0,t1) and result of type t2 |
(t0->t1,t2) |
function with argument of type t0 and result of type (t1,t2) |
(t0,t1->t2,t3) |
function with argument of type (t0,t1), result of type (t2,t3) |
(t0,t1->) |
function with argument of type (t0,t1) and no useful result |
(->t0) |
function with 0 arguments with result of type t0 |
… | etc |
Often the user does not have to write any types, and the system will take care of deriving primitive and composite types as implicitly specified by the expression. However when writing user defined functions, the types of the arguments must be specified, so that types can be checked for the function body; once this check succeeds, a type is attributed to the function, and it will henceforth be treated just like a built-in function of that type would be (and one can in fact for instance form an array that contains both built-in and user-defined functions, provided they all have the same (function) type).