3 ms·

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 an

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.

TazeTSchnitzel 8y ago
By “convert” here I mean convince the compiler that any thing of type A is any type B, when it definitely isn't, without using an explicit cast.
lmm 8y ago
The point is not that you can do explicit casts, it's that because you can form a (fake) instance for impossible types you can do invalid type conversions without doing anything that looks unsafe. In Haskell you can certainly achieve the same thing with various common extensions ( http://okmij.org/ftp/Haskell/impredicativity-bites.html 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).
J-Kuhn 8y ago
Read about Bottom (⊥). null can be considered bottom (if it were not for primitives)
tathougies 8y ago
Data.Dynamic is type safe. It performs a run-time type check. Haskell can be made to be unsound using 'unsafeCoerce', but as you'll note, there is a giant unsafe in front of it.
- chowells 8y ago
  Haskell is unsound because of 'undefined :: a'. There you go - a proof of every proposition by the Curry-Howard isomorphism. 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.
Tarean 8y ago
The actual correspondence in haskell are GADTs: 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 :: String

TazeTSchnitzel 8y ago

By “convert” here I mean convince the compiler that any thing of type A is any type B, when it definitely isn't, without using an explicit cast.

lmm 8y ago

The point is not that you can do explicit casts, it's that because you can form a (fake) instance for impossible types you can do invalid type conversions without doing anything that looks unsafe. In Haskell you can certainly achieve the same thing with various common extensions ( http://okmij.org/ftp/Haskell/impredicativity-bites.html 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).

J-Kuhn 8y ago

Read about Bottom (⊥). null can be considered bottom (if it were not for primitives)

tathougies 8y ago

Data.Dynamic is type safe. It performs a run-time type check. Haskell can be made to be unsound using 'unsafeCoerce', but as you'll note, there is a giant unsafe in front of it.

chowells 8y ago
Haskell is unsound because of 'undefined :: a'. There you go - a proof of every proposition by the Curry-Howard isomorphism. 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.

Tarean 8y ago

The actual correspondence in haskell are GADTs: 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 :: String