2 ms·

https://hackage.haskell.org/package/type-level-numbers-0.1.1.1/docs/TypeLevel-Number-Nat.html https://hackage.haskell.org/package/type-level-numbers-0.1.1... B

by judk 12y ago

https://hackage.haskell.org/package/type-level-numbers-0.1.1.1/docs/TypeLevel-Number-Nat.html https://hackage.haskell.org/package/type-level-numbers-0.1.1... But it's not clear to me what happens when you try to compile and typecheck program that attempts to subtract numbers provided as input at runtime.

tel 12y ago
That link only goes part way. What you'd need to do is something like createProof : (n : Nat) -> (m : Nat) -> Maybe (n >= m) which could either succeed or fail to produce the needed proof at runtime. Without the proof it'd be impossible to perform the subtraction, so that branch of your program is statically inaccessible.