Types.New.Adv.dscr

//Separates values into 'Value[a] | Type[a]'.

Res[rec, prim].

//The type system
Value[a]. //An untyped value.
Type[a]. //A value's type.

//Values
None[].
Some[a].
Zero[].
Succ[prev].

//Functions
One[a]. // Interesting - returns '1' in the encoding of 'a'.
Add[a, b].
Sub1[a].
Sub2[a].
Sub_[a, sub, cmp].
Fib[a].
Fib_[a, sub1, sub2].
Fib3[a].

//Types
Maybe[a].
Nat[].

//Type signatures
One[a: Type[a: Nat[]]]: Type[a: Nat[]]
Add[a: Type[a: Nat[]], b: Type[a: Nat[]]]: Type[a: Nat[]]
Sub1[a: Type[a: Nat[]]]: Type[a: Maybe[a: Nat[]]]
Sub2[a: Type[a: Nat[]]]: Type[a: Maybe[a: Nat[]]]
Fib[a: Type[a: Nat[]]]: Type[a: Nat[]]
Fib_[
  a: Type[a: Nat[]]
  sub1: Type[a: Maybe[a: Nat[]]]
  sub2: Type[a: Maybe[a: Nat[]]]
]: Type[a: Nat[]]
Fib3[a: Type[a: Nat[]]]: Type[a: Nat[]]

//Untyped functions
One[a: Value[a: Zero[]]]: Value[a: Succ[prev: Zero[]]]
One[a: Value[a: Succ[prev]]]: Value[a: Succ[prev: Zero[]]]
Add[a: Value[a: Zero[]], b: Value[a]]: b<Add
Add[a: Value[a: Succ[prev]], b: Value[a]]: Add[
  a: Value[a: a<Add>a<Value>prev<Succ]
  b: Value[a: Succ[prev: b<Add>a<Value]]
]
Sub1[a: Value[a: Zero[]]]: Value[a: None[]]
Sub1[a: Value[a: Succ[prev]]]: Value[a: Some[a: a<Sub1>a<Value>prev<Succ]]
Sub2[a: Value[a: Zero[]]]: Value[a: None[]]
Sub2[a: Value[a: Succ[prev: Zero[]]]]: Value[a: None[]]
Sub2[a: Value[a: Succ[prev: Succ[prev]]]]:
  Value[a: Some[a: a<Sub2>a<Value>prev<Succ>prev<Succ]]
Fib[a: Value[a]]: Fib_[a: a<Fib, sub1: Sub1[a: a<Fib], sub2: Sub2[a: a<Fib]]
Fib_[a: Value[a], sub1: Value[a: None[]], sub2]: One[a: a<Fib_]
Fib_[a: Value[a], sub1: Value[a: Some[a]], sub2: Value[a: None[]]]: One[a: a<Fib_]
Fib_[a: Value[a], sub1: Value[a: Some[a]], sub2: Value[a: Some[a]]]: Add[
  a: Fib[a: Value[a: sub1<Fib_>a<Value>a<Some]]
  b: Fib[a: Value[a: sub2<Fib_>a<Value>a<Some]]
]
Fib3[a: Value[a]]: Fib[a: Fib[a: Fib[a: a<Fib3]]]

//Alternate number encoding
One[a: Value[a: #Number[]]]: Value[a: 1]
Add[a: Value[a: #Number[]], b: Value[a: #Number[]]]:
  Value[a: #Add[a: a<Add>a<Value, b: b<Add>a<Value]]
Sub1[a: Value[a: #Number[]]]:
  Sub_[a: a<Sub1, sub: 1, cmp: #Compare[a: a<Sub1>a<Value, b: 1]]
Sub2[a: Value[a: #Number[]]]:
  Sub_[a: a<Sub2, sub: 2, cmp: #Compare[a: a<Sub2>a<Value, b: 2]]
Sub_[a: Value[a], sub, cmp: 1]: Value[a: Some[a: #Subtract[a: a<Sub_>a<Value, b: sub<Sub_]]]
Sub_[a: Value[a], sub, cmp: 0]: Value[a: Some[a: #Subtract[a: a<Sub_>a<Value, b: sub<Sub_]]]
Sub_[a: Value[a], sub, cmp: -1]: Value[a: None[]]

//Query
Res[
  rec: Fib3[a: Type[a: Nat[]] | Value[a: Succ[prev: Succ[prev: Succ[prev: Succ[prev: Zero[]]]]]]]
  prim: Fib3[a: Type[a: Nat[]] | Value[a: 4]]
]?