Magma is a dynamically typed language. In practice this means that:
> f := func< a, b | a+b >; > g := func< a, b | a+true >;First note that there are no declarations of the types of any of the identifiers.
Second consider the use of + in the definition of function f. Which addition function is meant by the + in a+b? Integer addition? Matrix addition? Group addition? ... Or in other words what is the type of the identifier + in function f? Is it integer addition, matrix addition, etc.? The answer to this question is that + here denotes all possible addition function values (+ is said to denote a family of function values), and Magma will automatically chose the appropriate function value to apply when it knows the type of a and b.
Say we now type,
> f(1,2);Magma now knows that a and b in f are both integers and thus + in f should be taken to mean the integer addition function. Hence it will produce the desired answer of 3.
Finally consider the definition of the function g. It is clear X+true for all X is a type error, so it might be expected that Magma would raise an error as soon as the definition of g is typed in. Magma does not however raise an error at this point. Rather it is only when g is applied and the line return a + true is actually executed that an error is raised.
In general the exact point at which type checking is done is not important. Sometimes however it is. Say we had typed the following definition for g,
> g := function(a,b) > if false then > return a+true; > else > return a+b; > end if; > end function;Now because the if false condition will never be true, the line return a+true will never be executed, and hence the type violation of adding a to true will never be raised!
One closing point: it should be clear now that where it was previously stated that the initial context "contains assignments of all the built-in Magma function values to the appropriate identifiers", in fact the initial context contains assignments of all the built-in Magma function families to the appropriate identifiers.