Sum

[ Application | sum.urp | sum.urs | sum.ur ]

Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.

Ur's support for analysis of types is based around extensible records, or row types. In the definition of the sum function, we see the type parameter fs assigned the kind {Unit}, which stands for records of types of kind Unit. The Unit kind has only one inhabitant, (). The kind Type is for "normal" types.

The sum function also takes an argument fl of type folder fs. Folders represent permutations of the elements of type-level records. We can use a folder to iterate over a type-level record in the order indicated by the permutation.

The unary $ operator is used to build a record Type from a {Type} (that is, the kind of records of types). The library function mapU takes in a type t of kind K and a {Unit} r, and it builds a {K} as long as r, where every field is assigned value t.

Another library function foldUR is defined at the level of expressions, while mapU is a type-level function. foldUR takes 7 arguments, some of them types and some values. Type arguments are distinguished by being written within brackets. The arguments to foldUR respectively tell us:

  1. The type we will assign to each record field
  2. The type of the final and all intermediate results of the fold, expressed as a function over the portion of the {Unit} that has been traversed so far
  3. A function that updates the accumulator based on the current record field name, the rest of the input record type, the current record field value, and the current accumulator
  4. The initial accumulator value
  5. The input record type
  6. A folder for that type
  7. The input record value
An unusual part of the third argument is the syntax [t1 ~ t2] within a multi-argument fn. This syntax denotes a proof that row types t1 and t2 have no field names in common. The proof is not named, because it is applied automatically as needed. Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of foldUR.

The general syntax for constant row types is [Name1 = t1, ..., NameN = tN], and there is a shorthand version [Name1, ..., NameN] for records of Units.

With sum defined, it is easy to make some sample calls. The form of the code for main does not make it apparent, but the compiler must "reverse engineer" the appropriate {Unit} from the {Type} available from the context at each call to sum. The compiler also infers a folder for each call, guessing at the desired permutations by examining the orders in which field names are written in the code.