//Records. These are data structures and function signatures.
//These records define natural numbers and addition.
Zero[]. //0 - in other languages this would be an ADT or singleton.
Next[prev]. //1 + prev - in other languages this would be an ADT, structure, or object.
Add[a, b]. //a + b - in other languages this would be a function.

//Reducers. Reducers are like function implementations. These reducers "implement" Add.
Add[a: Zero[], b]: b<Add //Adding 0 to anything produces 0.
Add[a: Next[prev], b]: Add[a: a<Add>prev<Next, b: Next[prev: b<Add]] //Adding 1 + n to anything produces n + (1 + anything).

//The main value. In other languages this would be the "main" function.
//When the program is run, it will apply the reducers to this value and output the result.
Add[
  a: Next[prev: Next[prev: Next[prev: Zero[]]]]
  b: Next[prev: Next[prev: Zero[]]]
]? //This encodes (2 + 3). What does it reduce to?