> data Nat = Zero | Succ Nat
> data Neg = Neg Nat
> subtract :: Nat -> Nat -> Either Nat Neg
I think that this is one example where the types don't speak completely for themselves. Is `Neg Zero` meant to stand for the integer `0` (as one might naïvely expect) or the integer `-1` (as one might expect from the pseudocode `Neg n = -(n + 1)`)? If the former, then what is `subtract Zero Zero`? (I.e., is it `Zero` or `Neg Zero`? I hope that we don't get into IEEE 754 (http://en.wikipedia.org/wiki/Signed_zero) territory here!) If the latter, then there's no ambiguity, but I think that it's fair to say that that meaning isn't clear just from the type!
Re:What is type safety?
by dragonwriter on Wednesday August 06, 2014 @07:09PM
(#8145386)
For minimum insanity, I think you'd have to assume that I meant Neg Zero to represent -1, Neg (Succ Zero) to be -2, etc., with an appropriate definition of subtract.
Well, no.
Its a problem if you assert that the result of subtraction is the same type, because the non-negative integers are not closed under subtraction--if the definition of your data type relies on something that is internally incoherent, you have a problem; but you can define subtraction of non-negative integers in a way that is general, not problematic, and doesn't require compile time knowledge of specific values, e.g.:
But, yeah, attaching arbitrary predicates as restrictions to types brings the halting problem into your compiler implementation.