Wouldn't that be a problem in most languages? Even Haskell allows for it through Data.Dynamic
If I can serialize to String, and then deserialize a String to any type of class, I can effectively "cast" anything to anything.
If I can serialize to String, and then deserialize a String to any type of class, I can effectively "cast" anything to anything.
In Haskell you can certainly achieve the same thing with various common extensions ( http://okmij.org/ftp/Haskell/impredicativity-bites.html ). Possibly not in vanilla Haskell '98, at the price of being not a very nice language to work in. (A total language like Idris should permit GADT-like functionality without allowing this kind of issue).
data EqualityProof a b where
Refl :: (a ~ b) => EqualityProof a b
-- compiler error because we don't check that the equality proof is actually Refl
coerce :: EqualityProof a b -> a -> b
coerce _ a = a
-- this works
coerce Refl a = a
-- here the Refl pattern match catches the undefined
-- this is like forcing the programmer to do a null check before the equality is in scope
-- and throwing a runtime exception when it's null
coerce undefinded 3 :: StringHaskell can be made to be unsound using 'unsafeCoerce', but as you'll note, there is a giant unsafe in front of it.
It's still safe, though, as it diverges at run time. Much like the ClassCastException coming from the JVM prevents the unsoundness in the original article from being a safety error.
'unsafeCoerce' (and things that can implement it, like creating a polymorphic mutable cell with 'unsafePerformIO') are worse than unsound - they are also unsafe.
null can be considered bottom (if it were not for primitives)