Basic.rename-add.dscr

//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.
Succ[prev]. //1 + prev - in other languages this would be an ADT, structure, or object.
Zero[a, b]. //a + b - in other languages this would be a function.

//Reducers. Reducers are like function implementations. These reducers "implement" Add.
Zero[a: Zero[], b]: b<Zero //Adding 0 to anything produces 0.
Zero[a: Succ[prev], b]: Zero[a: a<Zero>prev<Succ, b: Succ[prev: b<Zero]] //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.
Zero[
  a: Succ[prev: Succ[prev: Succ[prev: Zero[]]]]
  b: Succ[prev: Succ[prev: Zero[]]]
]? //This encodes (2 + 3). What does it reduce to?