3 ms·

Except that now you're no longer talking about something that requires the fuzzy handwaving of 'strong' vs. 'weak', which lack the well-defined one-way transfor

by blasdel 16y ago

Except that now you're no longer talking about something that requires the fuzzy handwaving of 'strong' vs. 'weak', which lack the well-defined one-way transformational characteristics of which you speak :) The type-system property you're dancing around is soundness. A well-defined term that you'd know if you'd read the fucking article, which was written explicitly to teach it to you. As for your example of what you consider 'weak' type-checking, I can see only two ways to make it 'strong'. The normal thing to do is a dynamic type-check resulting in a runtime exception if there's an invariant — in Python int(float("Inf")) raises OverflowError and int(float("NaN")) raises ValueError — would that satisfy you as 'strong'? The other option would be to use BigFloats and a fancy static type checker to ensure that you can never construct a zero value that could be processed as a float. Hilariously, GHC takes neither of these approaches: http://hackage.haskell.org/trac/ghc/ticket/3070 http://hackage.haskell.org/trac/ghc/ticket/3070 http://hackage.haskell.org/trac/ghc/wiki/Commentary/CmmExceptions http://hackage.haskell.org/trac/ghc/wiki/Commentary/CmmExcep...

derefr 16y ago
> Except that now you're no longer talking about something that requires the fuzzy handwaving of 'strong' vs. 'weak', which lack the well-defined one-way transformational characteristics of which you speak :) You missed a (perhaps subtle) point: the thing that has "well-defined one-way transformational characteristics" is an operation (an algorithm), not a type-system. A type-system can be thought of as a set of operations, a digraph specifying all the ways to go from each type to each other type in your system. This set has the property of being strong by default—but becomes weak if any of the operations is non-surjective. This is separate from a sound system, which is one that does not permit non-surjective operations. For an example of the crucial difference: I can program in "a strong subset of C" (C with all the non-surjective functions/casts removed.) I cannot program in "a sound subset of C." There is no such thing.
- blasdel 16y ago
  There is still an even more subtle point that you are absurdly close to understanding, and that the article touches on a bit — there really is no such thing as a type system, only a set of times and places where types are(n't) checked — operations. You even say so yourself! You'll find programming language theorists using the phrase "a sound subset" with no qualms.
  - deleted 16y ago
    [deleted]
  - derefr 16y ago
    Saying that there is no such thing as a type system is like saying there is no such thing as an integer. Sure, your machine can only represent an integer (and not very well), but that doesn't mean they don't exist—they're simply mathematical constructs. Mathematical constructs can have properties, such as being prime or composite, real or transfinite, countable or uncountable, or, in this case, strong or weak. > You'll find programming language theorists using the phrase "a sound subset" with no qualms. It makes no sense, though. There is no sound subset of C, because C isn't checked anywhere. There is no amount of pruning you could do that would allow you to call the result "sound": only by adding checks could you assert that. The usefulness of the term "strong" is that a strong system (pure surjective digraph) is able to be made sound, while a weak system (impure digraph) is not.
deleted 16y ago
[deleted]

by blasdel 16y ago

derefr 16y ago

> Except that now you're no longer talking about something that requires the fuzzy handwaving of 'strong' vs. 'weak', which lack the well-defined one-way transformational characteristics of which you speak :) You missed a (perhaps subtle) point: the thing that has "well-defined one-way transformational characteristics" is an operation (an algorithm), not a type-system. A type-system can be thought of as a set of operations, a digraph specifying all the ways to go from each type to each other type in your system. This set has the property of being strong by default—but becomes weak if any of the operations is non-surjective. This is separate from a sound system, which is one that does not permit non-surjective operations. For an example of the crucial difference: I can program in "a strong subset of C" (C with all the non-surjective functions/casts removed.) I cannot program in "a sound subset of C." There is no such thing.

blasdel 16y ago
There is still an even more subtle point that you are absurdly close to understanding, and that the article touches on a bit — there really is no such thing as a type system, only a set of times and places where types are(n't) checked — operations. You even say so yourself! You'll find programming language theorists using the phrase "a sound subset" with no qualms.
- deleted 16y ago
  [deleted]
- derefr 16y ago
  Saying that there is no such thing as a type system is like saying there is no such thing as an integer. Sure, your machine can only represent an integer (and not very well), but that doesn't mean they don't exist—they're simply mathematical constructs. Mathematical constructs can have properties, such as being prime or composite, real or transfinite, countable or uncountable, or, in this case, strong or weak. > You'll find programming language theorists using the phrase "a sound subset" with no qualms. It makes no sense, though. There is no sound subset of C, because C isn't checked anywhere. There is no amount of pruning you could do that would allow you to call the result "sound": only by adding checks could you assert that. The usefulness of the term "strong" is that a strong system (pure surjective digraph) is able to be made sound, while a weak system (impure digraph) is not.

deleted 16y ago

[deleted]