ExpandCollapsePrev Next Index


+ 5.1 Sums

In a category, given two objects \(T_0\) and \(T_1\) a sum is an object \(S\) together with two arrows: \[\inj_{S,0}: T_0 \rightarrow S\] \[\inj_{S,1}: T_1 \rightarrow S\] called injections , satisfying the condition that for any object \(Z\) and arrows \(f_0:T_0\rightarrow Z\) and \(f_1:T_1\rightarrow Z\) then there exists a unique arrow \(\alpha: S\rightarrow Z\) such that \[ \inj_{S,0} \cdot \alpha = f_0 \] and \[ \inj_{S,1} \cdot \alpha = f_1 \]

It can be shown sum are unique up to isomorphism. When there is a unique sum , or there is a canonical sum , we sometimes use the notation \[ T_0 + T_1 \] to denote it.

+ 5.1.1 Example: Sets

In \(\bf Sets\) the sum is the disjoint union. It is sometimes modelled by colouring or tagging elements: \[ T_0 + T_1 = T_0 \uplus T_1 = \lbrace (t_0, 0) \mid t_0 \in T_0 \rbrace \cup \lbrace (t_1, 1) \mid t_1 \in T_1 \rbrace \] where the injections are the maps \[ t_0 \mapsto (t_0,0) \] and \[ t_1 \mapsto (t_1,1) \]

The tags 0 and 1 are just added to ensure the elements of the disjoint union are unique, in case the argument sets overlap.

+ 5.1.2 Example: C

In C there is no native sum type, but we can model one:

enum tag {tag0, tag1};
struct V0 { tag v; T_0 t_0; };
struct V1 { tag v; T_1 t_1; };
union S { V0 v0; V1 v1; };
S make0 (T_0 t_0} { S s; S.v0.v = tag0; S.v0.t_0 = t_0; return s; }
S make1 (T_1 t_1} { S s; S.v1.v = tag0; S.v1.t_1 = t_1; return s; }

with the understanding that the variant tag v is set to tag0 or tag1 depending on whether a T_0 or T_1 is stored. This is common when modelling variant messages, in, for example X-Windows. The injection functions are shown.

+ 5.1.3 Example : Felix

Felix has native anonymous sum types. They're not used much because the notation is awkward.

  var x : int + long = case 0 of (int + long) 42;
  var y : int + long = case 1 of (int + long) 23L;
  match u with
    | case 0 (i) => println$ "int " + str i;
    | case 1 (l) => println$ "long " + str l;

Here, case 0 of (int + long) is the first injection function, and case 1 of (int + long) is the second injection function. The match shows how to decode the sum to extract the argument based on the discriminant index 0 or 1.

+ 5.1.4 Example: Felix

Felix also has a nominally typed sum which is more commonly used:

  union Number = Int of int | Long of long;
  var x = Int 42;
  var y = Long 23L;
  match u with
    | Int (i) => println$ "int " + str i;
    | Long (l) => println$ "long " + str l;

The implementation is the same, but we have names for the tags now.

Injections are not normally considered functions, rather they're called type constructors because they construct the sum type from an argument.

+ 5.2 N-ary Sums

Sum types can clearly be extended to more than 2 components. It is possible to identify a 1-ary sum with the component type. However Felix does not do this.

+ 5.3 Initial object

We have to ask what the sum of nothing is. It is called the an initial object. In \(\bf Sets\) the empty is set is initial. Initial objects are characterised by the fact that for any object \(Z\) there is a unique arrow from the initial object to that object. In \(\bf Sets\) the function from the empty set to any other set is unique because it maps no elements, since there are none to map! Note that such functions certainly exist, if you consider a function modelled as a set of ordered pairs, such a function is simply the empty set.

In Felix type system, the initial object is the type called void or 0. There are no values of this type!