//Implicit types by alternate representation. "Hacky" but easy.
//Infinitely recurses using the current interpreter - need a special
//interpreter which handles values which reduce to themselves.

//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.
Add[a, b]. //a + b - in other languages this would be a function.
Nat[]. //A natural number - in other languages this would be a type.

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

//More reducers. These reducers aren't really function implementations.
//In other languages, these would assign the types to the instances.
Zero[]: Zero[] | Nat[] //Zero is a natural.
Succ[prev: Nat[]]: Succ[prev: Nat[]] | Nat[] //1 + n is a natural if n is a natural.

//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: Succ[prev: Succ[prev: Succ[prev: Zero[]]]]
  b: Succ[prev: Succ[prev: Zero[]]]
]? //What does this reduce to?