Kinds classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.
Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
Constructors are the main class of compile-time-only data. They include proper types and are classified by kinds.
We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. Also, in the ``known-length type-level record'' form, in terms, the parser currently only allows to be of the forms (as a shorthand for ) or , or a natural number to stand for the corresponding field name (e.g., for tuples).
Modules of the module system are described by signatures.
Patterns are used to describe structural conditions on expressions, such that expressions may be tested against patterns, generating assignments to pattern variables if successful.
Expressions are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
Declarations primarily bring new symbols into context.
There are two kinds of Ur files. A file named is an implementation file, and it should contain a sequence of declarations . A file named is an interface file; it must always have a matching and should contain a sequence of signature items . When both files are present, the overall effect is the same as a monolithic declaration . When no interface file is included, the overall effect is similar, with a signature for module being inferred rather than just checked against an interface.
We omit some extra possibilities in syntax, deferring them to Section 9.1.1. The concrete syntax of declarations is also more complex than shown in the table above, with details deferred to Section 9.1.1.