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

Types

gist.github.com

Post reply on HN
Print view View original

171–180 of 198 posts

Re: Types

#171

Post by catnaroek »

eli_gottlieb wrote: post #163
catnaroek wrote: post #149

Earlier quoted context omitted.

I offer this thread as evidence: https://news.ycombinator.com/item?id=12342583

Hey, it's not the fault of the programming masses that some evil motherfucker conflated implementation extension (inheritance) and subtyping. Subtyping = "A Inheritance = "A inherits B, if I try to actually use it as a B, it promises to work. However, it might actually blow up in my face, because it was keeping its extra details secret from me and promising they wouldn't blow up."

> programming masses, some evil (bleep)

Too harsh. Logic is hard for humans. Evolution has trained us to take lots of mental shortcuts, not to be perfect calculating machines. Even the most technically competent people rely on their intuition. What differentiates them from the rest of us is that they have trained their intuition to make it more reliable [0].

It's the job of a language designer to arrange things so that intuition doesn't mislead programmers regarding the meaning of language features. Before proposing a new feature, the designer must anticipate how programmers will think about code that uses this feature, and there better not be a mismatch between what programmers think the code means and what the code actually means.

> A inherits B, if I try to actually use it as a B, it promises to work.

There's nothing wrong with implementation inheritance per se [1]. It addresses a very common use case: you have a thing Foo, and you want to produce another thing Bar that's similar to Foo, with minor changes here and there. This describes accurately how many things work in real life. However, you can't assume that Bar can always be used where Foo is expected. Those “minor changes here and there” might have rendered Bar incompatible with Foo. Hence, “inheritance is not subtyping”. As stated above, it's the job of a language designer to anticipate this.

[0] https://terrytao.wordpress.com/career-advice/there%E2%80%99s...

[1] Other than the lack of mathematical elegance, but few things are mathematically elegant in life.

Re: Types

#172

Post by groovy2shoes »

marcosdumay wrote: post #144
tomp wrote: post #67

Earlier quoted context omitted.

> Proving F matches the type is arbitrary hard and is impossible to automated in general So what? Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...

The only time I remember using indexed list access in Haskell was on a dirty script that would break in 3 months anyhow. They are just ugly, and throw a huge amount of safety away, for no big gain at all. Mainstream languages will gain much more from better iterators than by a ton of effort that just proves your indexes are within bounds.

While I agree that better iterators are desirable, iteration is far from the only operation on arrays (or any other collection for that matter).

Re: Types

#173

Post by naasking »

acjohnson55 wrote: post #166
naasking wrote: post #87

Decent overview of many concepts, but the opening line isn't strictly true: > A type is a collection of possible values. A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. So a type is much more powerful than a simple set-based interpretation, even though this is how most people think about it. For instance, in Haskell you can encode a region calculus that…

Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value. The sidesteps the idea of type being something permanent and inherent to a value. In practice, the type might be metadata discoverable and actionable at run-time, it might be something that exists at compile-time to determine correctness of a program (based on how values are used), or both. Does thi…

> Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value.

That might be a simpler way of explaining it, since "proposition" is rather abstract. Or perhaps, a type defines the valid state transitions your program can undergo at any given point, ie. given the data in your program (the program state S0), the types of all of that data define a set of valid transitions to another data set (program state S1).

Re: Types

#174

Post by eli_gottlieb »

catnaroek wrote: post #171
eli_gottlieb wrote: post #163

Earlier quoted context omitted.

Hey, it's not the fault of the programming masses that some evil motherfucker conflated implementation extension (inheritance) and subtyping. Subtyping = "A Inheritance = "A inherits B, if I try to actually use it as a B, it promises to work. However, it might actually blow up in my face, because it was keeping its extra details secret from me and promising they wouldn't blow up."

> programming masses, some evil (bleep) Too harsh. Logic is hard for humans. Evolution has trained us to take lots of mental shortcuts, not to be perfect calculating machines. Even the most technically competent people rely on their intuition. What differentiates them from the rest of us is that they have trained their intuition to make it more reliable [0]. It's the job of a language designer to arrange things so th…

>Hence, “inheritance is not subtyping”. As stated above, it's the job of a language designer to anticipate this.

Yes, it is their job, by not allowing subclasses to be used as subtypes.

Re: Types

#175

Post by catnaroek »

eli_gottlieb wrote: post #174
catnaroek wrote: post #171

Earlier quoted context omitted.

> programming masses, some evil (bleep) Too harsh. Logic is hard for humans. Evolution has trained us to take lots of mental shortcuts, not to be perfect calculating machines. Even the most technically competent people rely on their intuition. What differentiates them from the rest of us is that they have trained their intuition to make it more reliable [0]. It's the job of a language designer to arrange things so th…

>Hence, “inheritance is not subtyping”. As stated above, it's the job of a language designer to anticipate this. Yes, it is their job, by not allowing subclasses to be used as subtypes.

Some subclasses can be safely used as subtypes. For example, those that meet the following two conditions:

(0) Not directly mutating superclass fields. (Reading them is fine.)

(1) Not overriding non-abstract methods of the superclass.

Re: Types

#176

Post by naasking »

catnaroek wrote: post #168
tel wrote: post #164

Earlier quoted context omitted.

I disagree that it's a good idea to think of types as a "collection" (loosely) of values. It may be the case that you do not distinguish computation and value (here, I'm thinking of CBPV) but types only classify values as interpreted via their embedding into expressions.

If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Of course, induction on datatypes is unsound in Haskell, but it's sound in Standard ML.

> If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound.

Just because induction on some types is sound, does not entail that induction on all types is sound. Indeed it's not in general, even though it may be in specific languages.

Re: Types

#177

Post by naasking »

eli_gottlieb wrote: post #174
catnaroek wrote: post #171

Earlier quoted context omitted.

> programming masses, some evil (bleep) Too harsh. Logic is hard for humans. Evolution has trained us to take lots of mental shortcuts, not to be perfect calculating machines. Even the most technically competent people rely on their intuition. What differentiates them from the rest of us is that they have trained their intuition to make it more reliable [0]. It's the job of a language designer to arrange things so th…

>Hence, “inheritance is not subtyping”. As stated above, it's the job of a language designer to anticipate this. Yes, it is their job, by not allowing subclasses to be used as subtypes.

> Yes, it is their job, by not allowing subclasses to be used as subtypes.

That's probably too extreme. Subtyping should just be explicitly declared rather than implicit when subclassing.

Re: Types

#178

Post by rpazyaquian »

What types are and what they do is all well and good, but what I want to know is how they would help me write a larger application. Would it help it be more correct, be written faster, or be more flexible? Does it just help on a line-by-line programming basis, or can it have any ramifications on a higher level like product design?

Re: Types

#179

Post by catnaroek »

naasking wrote: post #176
catnaroek wrote: post #168

Earlier quoted context omitted.

If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Of course, induction on datatypes is unsound in Haskell, but it's sound in Standard ML.

> If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Just because induction on some types is sound, does not entail that induction on all types is sound. Indeed it's not in general, even though it may be in specific languages.

(0) I didn't say all types. I said datatypes.

(1) Induction on datatypes is a powerful tool for reasoning about programs in strict languages, and it's only possible when you regard datatypes as collections of values.

Re: Types

#180

Post by dragonwriter »

catnaroek wrote: post #175
eli_gottlieb wrote: post #174

Earlier quoted context omitted.

>Hence, “inheritance is not subtyping”. As stated above, it's the job of a language designer to anticipate this. Yes, it is their job, by not allowing subclasses to be used as subtypes.

Some subclasses can be safely used as subtypes. For example, those that meet the following two conditions: (0) Not directly mutating superclass fields. (Reading them is fine.) (1) Not overriding non-abstract methods of the superclass.

If classes are types, subsclasses should be subtypes -- so the above restrictions should just be applied to subclass relationships.

One could also have an non-subclassing mechanism of implementation sharing, that might be declared something like this:

  class Related does (method1, method2) like Base;
or

  class Related does all except (method3) like Base;
Post reply on HN