3 ms·
Well, you'd probably have to introduce a type such that every time you subtracted n from m you must prove that m is at least as big as n. Which would be a pain.
by tel 12y ago
Well, you'd probably have to introduce a type such that every time you subtracted n from m you must prove that m is at least as big as n. Which would be a pain.
As usual, I really suggest playing with Agda or Idris to get a feel for what sophisticated types actually look and feel like.
- judk 12y agohttps://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 agoThat 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.