Types.Exp.dscr

//Explicit type by alternate representation.

//Records. These are data structures and function signatures.
//These records define natural numbers and addition.
Nat[]. //A natural number - in other languages this would be a type.
Untyped[]. //Denotes that a value needs to be typed.
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.

//Reducers. Reducers are like function implementations. These reducers "implement" Add.
Add[a: Nat[], b: Nat[]] | Untyped[]: Nat[] //Adding naturals produces a natural.
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).

//More reducers. These reducers aren't really function implementations.
//In other languages, these would assign the types to the instances.
Zero[] | Untyped[]: Zero[] | Nat[] //Zero is a natural. Need `Zero[]` in RHS so it isn't consumed.
Succ[prev: Nat[]] | Untyped[]: Nat[] //1 + n is a natural if n is a natural. Don't need `Succ[...]` in RHS because the only part consumed is the type.

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