4 ms·

I like your style but your definition doesn't hold — there's plenty of implicit downcasts that are still 'strong', like boolean tests on data bigger than 1 bit

by blasdel 16y ago

I like your style but your definition doesn't hold — there's plenty of implicit downcasts that are still 'strong', like boolean tests on data bigger than 1 bit or gt/lt comparisons between different numeric types — a type system that allows those is totally sound. It's not your fault though, the problem is really just that 'strong' and 'weak' are just fundamentally unsound nomenclature.

derefr 16y ago
> The problem is really just that 'strong' and 'weak' are just fundamentally unsound nomenclature. As I said, we all know, and agree upon, which languages are "strong" or "weak", whatever those terms mean. Thus, the two words really do partition the world in some way; they do real Bayesian work. We just have to figure out what that work is. > there's plenty of implicit downcasts that are still 'strong', like boolean tests on data bigger than 1 bit or gt/lt comparisons between different numeric types Notice, above, that I said that explicitness isn't a part of the definition, as much as people like to think it is. In fact, it could be completely explicit at all times that you're casting (int)s to (char)s—and that would still be weak typing. The real property a type-system has that tells you that it is "weak" is that it allows casts between types that do not have valid surjections. "(" has no number it maps to—and yet the type system pretends it does. IEEE754 Infinity has no integer it maps to—and yet the type system says that's alright. (Note that in this special case, the hardware notices this loss of information, and sets a hardware exception flag.) Operations retain strong-typing if they have well-defined one-way transformational characteristics, such as when casting (int) to (bool) using C's "!= 0" branching-requirement. "x % 6" compresses the field of integers into a set of six elements—but it does this in a way which maps every x to a valid new value on the "x % 6" ring. However, Infinity does not have a valid (int) representation—any value the computer does choose to represent it with will be "wrong." To sum up: if, in your language runtime, there exists at least one type-transformation-implementation that goes like this: try a_entropy = f( a ) B.construct( a_entropy ) catch( DomainError e ) # A is not a well-defined B B::SomeDefaultElement # who cares! end ...then you have weak typing.
- 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]

by blasdel 16y ago

derefr 16y ago

> The problem is really just that 'strong' and 'weak' are just fundamentally unsound nomenclature. As I said, we all know, and agree upon, which languages are "strong" or "weak", whatever those terms mean. Thus, the two words really do partition the world in some way; they do real Bayesian work. We just have to figure out what that work is. > there's plenty of implicit downcasts that are still 'strong', like boolean tests on data bigger than 1 bit or gt/lt comparisons between different numeric types Notice, above, that I said that explicitness isn't a part of the definition, as much as people like to think it is. In fact, it could be completely explicit at all times that you're casting (int)s to (char)s—and that would still be weak typing. The real property a type-system has that tells you that it is "weak" is that it allows casts between types that do not have valid surjections. "(" has no number it maps to—and yet the type system pretends it does. IEEE754 Infinity has no integer it maps to—and yet the type system says that's alright. (Note that in this special case, the hardware notices this loss of information, and sets a hardware exception flag.) Operations retain strong-typing if they have well-defined one-way transformational characteristics, such as when casting (int) to (bool) using C's "!= 0" branching-requirement. "x % 6" compresses the field of integers into a set of six elements—but it does this in a way which maps every x to a valid new value on the "x % 6" ring. However, Infinity does not have a valid (int) representation—any value the computer does choose to represent it with will be "wrong." To sum up: if, in your language runtime, there exists at least one type-transformation-implementation that goes like this: try a_entropy = f( a ) B.construct( a_entropy ) catch( DomainError e ) # A is not a well-defined B B::SomeDefaultElement # who cares! end ...then you have weak typing.

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]