//'Types.New' with property key syntax sugar. //Uses ambiguous matches - might change in future. //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 Zero[]. Succ[prev]. Add[a, b]. Fib[a]. Fib3[a]. //Types Nat[]. //Type signatures Add[Type[Nat[]], Type[Nat[]]]: Type[Nat[]] Fib[Type[Nat[]]]: Type[Nat[]] Fib3[Type[Nat[]]]: Type[Nat[]] //Untyped functions Add[Value[Zero[]], Value[a]]: Value[b>a] Add[Value[Succ[prev]], Value[a]]: Add[ Value[a>a>prev] Value[Succ[prev: baa>prev]] Fib[Value[a>a>prev>prev]] ] Fib3[Value[a]]: Fib[Fib[Fib[Value[a>a]]]] //Alternate number representation Add[Value[#Number[]], Value[#Number[]]]: Value[#Add[a>a, b>a]] Fib[Value[0]]: Value[1] Fib[Value[1]]: Value[1] Fib[Value[#Number[]]]: Add[ Fib[Value[#Add[a>a, -1]]] Fib[Value[#Add[a>a, -2]]] ] //Query Res[ rec: Fib3[Type[Nat[]] | Value[Succ[Succ[Succ[Succ[Zero[]]]]]]] prim: Fib3[Type[Nat[]] | Value[4]] ]?