Overview

Because any Rosetta item whose value is a set can be used to create a type, creating new types is the same process as creating new sets. Rosetta provides three basic mechanisms for forming sets and types: (i) listing the elements explicitly, (ii) filtering or composing existing sets, or (iii) defining functions for constructing the elements of the set. Listing the elements of a set, referred to as extension, is the simplest mechanism for defining new types. The new type is formed by simply using the set former to list the elements of the type. Filtering existing sets, referred to as comprehension, involves using the sel operation or one of its derivatives to extract a set of items from an existing set. Finally, defining functions to construct type elements, referred to as constructive specification, involves defining functions that generate all elements of a type.

Types are specified using the expression language to define sets making Rosetta's type system dependent. Specifically, the same language used to define expressions that use declared items is used to define their types. Most programming languages use a distinct language subset for defining types that does not include anything requiring evaluation. Although this restriction makes type checking far simpler, Rosetta uses a dependent type system due to its expressive power.

An excellent example of Rosetta's type system's power is using comprehension to define item properties. Defining a set by comprehension is defining a property that each member of the new set...