Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What is type safety?

pl-enthusiast.net

Post reply on HN
Print view View original

61–70 of 71 posts

Re: What is type safety?

#61

Post by tel »

ionforce wrote: post #53
tel wrote: post #29

Earlier quoted context omitted.

In the context of this article that's just confusing the issue. "Type" is both well-defined and not the same as "type" in a Ruby context.

What is type in a Ruby context?

Usually in a Ruby context you'd refer to something like Fixnum or String as types when really that's their "class"

    irb(main):005:0> 3.class
    => Fixnum
Such a "type" doesn't have much to do with "types" as discussed when referring to static types. They're simply orthogonal concepts.

Re: What is type safety?

#62

Post by kazinator »

Article claims that, for Python and Ruby, "language semantics gives meaning to all programs, so the well defined and all circles of our diagram coincide".

How can that be so, if Python and Ruby provide escape hatches that allow C libraries to be called?

Perhaps what is meant that in the absence of using certain features, the core semantics is well-defined.

Re: What is type safety?

#63

Post by mnarayan01 »

tel wrote: post #61
ionforce wrote: post #53

Earlier quoted context omitted.

What is type in a Ruby context?

Usually in a Ruby context you'd refer to something like Fixnum or String as types when really that's their "class" irb(main):005:0> 3.class => Fixnum Such a "type" doesn't have much to do with "types" as discussed when referring to static types. They're simply orthogonal concepts.

The result of the #class method does not _fully_ encapsulate an object's type (e.g. #extend, #define_singleton_method, etc may have been used to modify the object's type) but every Ruby expression does have a type in exactly the sense as used when talking about static typing; the only difference is when you can (in general) determine that type. The #class method is not orthogonal to type, it is merely incomplete.

Re: What is type safety?

#64

Post by tel »

mnarayan01 wrote: post #63
tel wrote: post #61

Earlier quoted context omitted.

Usually in a Ruby context you'd refer to something like Fixnum or String as types when really that's their "class" irb(main):005:0> 3.class => Fixnum Such a "type" doesn't have much to do with "types" as discussed when referring to static types. They're simply orthogonal concepts.

The result of the #class method does not _fully_ encapsulate an object's type (e.g. #extend, #define_singleton_method, etc may have been used to modify the object's type) but every Ruby expression does have a type in exactly the sense as used when talking about static typing; the only difference is when you can (in general) determine that type. The #class method is not orthogonal to type, it is merely incomplete.

Sure, but that's not really relevant. All of your "typing" occurs at runtime and thus is entwined in the language dynamics and not its statics.

Re: What is type safety?

#65

Post by tel »

igravious wrote: post #8

> A classic English example is Chomsky’s “Colorless green ideals sleep furiously”—perfectly syntactically correct, but meaningless. Interesting. But is it meaningless? Isn't its very meaninglessness its meaning because it has come do be known due to it being bandied about far and wide as an example of meaninglessness. Maybe it's something more. Clearly, for all X, X cannot be at one and the same time both green and c…

These are dramatically philosophical, but also dispatched by epistemologists for a long time now.

1. "Isn't its very meaninglessness its meaning" is a confusion of reference and sense. The quoted sentence "Colorless green ideals sleep furiously" interpreted as an object in its own right holds meaning as a common example of syntax and semantics but if you "remove the quotes" and interpret its sense then we run into problems... and obviously that's what everyone is talking about when they bring it up.

2. "Is it in this way that it fails to have meaning and so will always continue to fail to have meaning?" Yep. If we assert that we're stating this sentence as an assertion or judgement of reality then we would like to evaluate its "truth". Even without getting too mystical it's a long established sense of the definition of truth that it ought to somehow correspond with reality and that any notion of truth which does not is hypothetical or meaningless. This is encapsulated in Dummett's C and discussed by Per Martin-Löf here: https://michaelt.github.io/martin-lof/Truth-and-Knowability-...

Re: What is type safety?

#66

Post by judk »

tel wrote: post #40
AnimalMuppet wrote: post #36

Earlier quoted context omitted.

It seems to me that you probably don't want to do arbitrary computation in types at compile time. Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid. That's not a good position to put your compiler in. It seems to me to…

Well, you'd probably have to introduce a type such that every time you subtracted n from m you must prove that m is at least as big as n. Which would be a pain. As usual, I really suggest playing with Agda or Idris to get a feel for what sophisticated types actually look and feel like.

https://hackage.haskell.org/package/type-level-numbers-0.1.1...

But it's not clear to me what happens when you try to compile and typecheck program that attempts to subtract numbers provided as input at runtime.

Re: What is type safety?

#67

Post by tel »

judk wrote: post #66
tel wrote: post #40

Earlier quoted context omitted.

Well, you'd probably have to introduce a type such that every time you subtracted n from m you must prove that m is at least as big as n. Which would be a pain. As usual, I really suggest playing with Agda or Idris to get a feel for what sophisticated types actually look and feel like.

https://hackage.haskell.org/package/type-level-numbers-0.1.1... But it's not clear to me what happens when you try to compile and typecheck program that attempts to subtract numbers provided as input at runtime.

That link only goes part way.

What you'd need to do is something like

    createProof : (n : Nat) -> (m : Nat) -> Maybe (n >= m)
which could either succeed or fail to produce the needed proof at runtime. Without the proof it'd be impossible to perform the subtraction, so that branch of your program is statically inaccessible.

Re: What is type safety?

#68

Post by JadeNB »

dragonwriter wrote: post #54
AnimalMuppet wrote: post #36

Earlier quoted context omitted.

It seems to me that you probably don't want to do arbitrary computation in types at compile time. Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid. That's not a good position to put your compiler in. It seems to me to…

> Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. 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 intege…

> 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?

#69

Post by kybernetikos »

igravious wrote: post #8

> A classic English example is Chomsky’s “Colorless green ideals sleep furiously”—perfectly syntactically correct, but meaningless. Interesting. But is it meaningless? Isn't its very meaninglessness its meaning because it has come do be known due to it being bandied about far and wide as an example of meaninglessness. Maybe it's something more. Clearly, for all X, X cannot be at one and the same time both green and c…

> But is it meaningless?

Well, the way I use words it is not meaningless. It has a pretty clear meaning. Admittedly, that meaning may not describe any possible state of the world (although I could perhaps argue that), but I can only spot that because I know what the phrase means.

Re: What is type safety?

#70

Post by dragonwriter »

JadeNB wrote: post #68
dragonwriter wrote: post #54

Earlier quoted context omitted.

> Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. 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 intege…

> 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…

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.
Post reply on HN