Type Theory exploration
Type Theory My understanding of Type theory. Defining natural numbers: zero: Nat succ(n: Nat ): Nat So for example defining the number 2: succ(succ(zero)): Nat same as??? isNat(zero) ForAll(n) : isNat(n)=>isNat(succ(n)) We can define operations like plus and times and equals //define proofs that n==n equals(zero,zero): Equals< zero,zero > equals(succ(n: Nat ),succ(n: Nat )): Equals< succ ( n :Nat ) , succ ( n :Nat ) > Proofs and Dependent types Define a dependent type Even <n: Nat > which is a proof that n is even. {a: Nat, p: Equals <times(2,a),n>}: Even <n: Nat > So that for example the following is a proof that 6 is even: {3, equals(times(2,3),6)}: Even <6> which becomes {3: Nat ,equals(6,6): Equals <6,6>} : Even <6> {a: Nat , p: Equals <times(2,a),n>}: Even <n: Nat > isEven(n) = n => (a => (isNat(a) & equals(times(2,a),n))) isEven(6) (3) In C syntax typedef Even < Nat n> { Nat a, Equals <ti