Built-in types

The universe

Currently there is only one universe Type that contains all types, including itself, making the type theory inconsistent. In the future it is planned to incorporate universe levels using mugen.

Functions and function-types

Apart from the universe, the only predefined type is a dependent function-type, written (x:A) → B x as in NuPRL and Agda. As usual, if B does not depend on x one can simplify this to A → B, and iterated function-types can be combined, including combining multiple variables with the same type, as in (x y : A) (z : B x y) → C x y z. Also as usual, this notation is right-associative, so A → B → C means A → (B → C). The unicode → appearing here is interchangeable with the ASCII ->.

Again as usual, functions are applied by juxtaposition; if f : (x:A) → B x and a : A then f a : B a. And this is left-associative, so if f : A → B → C then f a b : C.

Functions are introduced by abstraction, which in Narya is written (somewhat unusually) as x ↦ M, or x y z ↦ M to abstract multiple variables at once. The unicode ↦ is interchangeable with the ASCII |->. If desired, the type of the variable can be indicated explicitly with (x : A) ↦ M.

The variable in a function-type or an abstraction can be replaced by an underscore _, indicating that that variable is not used and thus needs no name. For types this is equivalent to a non-dependent function-type: (_ : A) → B means the same as A → B. For abstractions, _ ↦ M defines a constant function, whose value doesn’t depend on its input.