See the official user manual for the most up-to-date version of the information on this page.
Name Parts
A name part is a string of printable characters not containing any of the following characters:
_;."(){}@
Furthermore, certain keywords may not be used as name parts.
(Unqualified) Names
A name is a sequence of one or more name parts separated by underscores (_).
A string like a≤b (without spaces) is a valid name, and is different from a ≤ b (with spaces). The latter actually refers to a type, whose terms are (roughly speaking) proofs that a is less than or equal to b. It is a standard convention to use a name like a≤b for a variable of type a ≤ b.
Similarly, strings like x:A and A->B are names. To declare x as a variable of type A we must write x : A (with spaces) rather than x:A. To refer to the type of functions from A to B, we must write A -> B rather than A->B.
The meaning of underscores in names is explained in the section on mixfix operators. For example, the addition function is officially named _+_ , and the placement of the underscores indicates that we can use the infix notation a + b to refer to the value of the function at a and b.
Qualified Names
A qualified name is a sequence of one or more unqualified names separated by dots (.).
Qualified names are used in naming modules and in referring to the contents of unopened modules.
For example, the proposition that a natural number n is prime can be written in qualified form as
Data.Nat.Primality.Prime n, referring to a definition given in the standard library module
Data.Nat.Primality. The abbreviated notation Prime n can be used after that module has
been imported and opened, as explained on the modules page.