News for hackers. Stuff that matters.

A comment on What is type safety?. Parent comment

Re:What is type safety? by tel on Tuesday August 05, 2014 @01:34PM (#8138160)
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.

[ Parent | on HN ]
Re:What is type safety? by judk on Tuesday August 05, 2014 @11:52PM (#8140914)
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.

[ Parent | on HN ]
Re:What is type safety? by tel on Wednesday August 06, 2014 @01:52AM (#8141204)
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.
[ Parent | on HN ]