Types.Fun.dscr

//Types by functions. Not "hacky".

//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.
Type[a]. //Get the type of a value.
TypeSucc[a].

//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).
Type[a: Zero[]]: Nat[]
Type[a: Succ[prev]]: TypeSucc[a: Type[a: a<Type>prev<Succ]]
TypeSucc[a: Nat[]]: Nat[]

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