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

Typing Is Hard

3fx.ch

Post reply on HN
Print view View original

61–70 of 134 posts

Re: Typing Is Hard

#61

Post by adwn »

jbluepolarbear wrote: post #47
skrebbel wrote: post #5

I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cos…

Typescript taught me that I actually don’t care about types and all I care about is the shape of data. In most cases I think of types/interfaces in Typescript as strict data definitions. A function takes in a collection of data; as long as the data matches the shape I expect, don’t care what the data represents.

> Typescript taught me that I actually don’t care about types and all I care about is the shape of data.

Seconding leafario2 here, that's exactly what types do: They give guarantees about the shape of data.

Maybe what you meant was you don't care whether an object is of type Customer or Supplier, as long as it has an element/field named address. That's called "structural typing" (as opposed to "nominal typing").

Few static type systems have structural typing, probably because in practice, you actually do care whether the object is a Customer or a Supplier, even if their fields have the same names. Rust, for example, is nominally typed, but you can define a trait "HasAddress" with a trait function "fn address(&self) -> &str" and implement it for Customer and Supplier, to simulate structural typing where you need it.

Re: Typing Is Hard

#62

Post by derriz »

refenestrator wrote: post #45
lmm wrote: post #37

Earlier quoted context omitted.

> Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Only if that crowd has never used a good typed language, IME. I spent two weeks trying to get things done in TypeScript and then two days writing them in Scala.js. It's am…

Consider that you might be the weirdo here. Kotlin is eating scala's lunch by specifically jettisoning the advanced type stuff. If you can give 80% of the value with 20% of the confusion, that's a win for most devs.

Kotlin has lots of type anomalies if you peruse the official discussion fora. For example, you can write a pure Kotlin program, which compiles without (type) warning/error, that throws an NPE without using casting.

Overall I prefer Kotlin to Scala as I really disliked Scala's implicits.

But I'm not convinced that Kotlin's type system is that much simpler than Scala's when you think of the interactions between various features like smart casting.

It certainly doesn't seem to compile any faster - I have a 2020 quad-core i7 laptop and at best I'm seeing is compile times in the range of a few hundred lines of code per second - and I suspect this is due to type inference rather than byte code generation. Both Kotlin and Scala represent a significant regression in this regard for me.

Re: Typing Is Hard

#63

Post by lmm »

KMag wrote: post #60
lmm wrote: post #46

Earlier quoted context omitted.

Kotlin is eating Scala's hype by hyping how much better their ad-hoc informally-specified implementation of half the advanced type stuff is. Having had to actually debug errors from their "suspend functions", "platform types" and goodness knows what else, there's nothing simpler about it.

I think optimally, you have a powerful effect and dependent linear type system with adjustable strictness of checking. You'd use the very weakest level for a REPL : warn if there is no set of types that allows a function to execute without throwing a runtime type error. Most applications would be run/compiled with stricter checking. Libraries packed up for package managers would presumably be checked with full effect…

Sounds overcomplicated. I've seen any number of fancy not-exactly-type-systems and they always end up having crazy edge cases, whereas a plain type system does exactly what you expected (and, crucially, does it in an understandable way) and scales arbitrarily far. Having the type system work the same way in the REPL and the rest of the language is important for that.

Re: Typing Is Hard

#64

Post by seanmcdirmid »

dwhitney wrote: post #28
skrebbel wrote: post #5

I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cos…

I need to write a blog entry titled, "Your test suite is basically a sh*tty type system." -- I'm in the "totally anal" camp of type system aficionados :)

Or the converse “your type system is basically a very limited test suite.”

Seriously though, these two concepts have some overlap that should be explored more.

Re: Typing Is Hard

#65

Post by seanmcdirmid »

jbluepolarbear wrote: post #47
skrebbel wrote: post #5

I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cos…

Typescript taught me that I actually don’t care about types and all I care about is the shape of data. In most cases I think of types/interfaces in Typescript as strict data definitions. A function takes in a collection of data; as long as the data matches the shape I expect, don’t care what the data represents.

What you use the word “type” for is a nominal type and your shapes are structural types. The utility and different trade offs between nominal and structural types were explored a lot back in the 90s.

Re: Typing Is Hard

#66

Post by Sharlin »

seanmcdirmid wrote: post #65
jbluepolarbear wrote: post #47

Earlier quoted context omitted.

Typescript taught me that I actually don’t care about types and all I care about is the shape of data. In most cases I think of types/interfaces in Typescript as strict data definitions. A function takes in a collection of data; as long as the data matches the shape I expect, don’t care what the data represents.

What you use the word “type” for is a nominal type and your shapes are structural types. The utility and different trade offs between nominal and structural types were explored a lot back in the 90s.

Everything old is new again.

Re: Typing Is Hard

#68

Post by saurik »

dwhitney wrote: post #27

it drives me absolutely insane that this TypeScript compiles: const num: number = [][0]

FWIW, most (arguably any/all) non-dependently-typed languages would let that slide, as [] is of type "array of (at best) X (which could be inferred as number by working backwards from the declaration)" and one of the operations you can do on an array is to index it, by a (maybe unsigned) integer, with 0 (either way) thereby being a valid index. For this to fail, in addition to the type of the array being parameterized by its size (which is at least not too uncommon if not exactly common) the type of that index operator has to be (more notably) at least parameterized by the concrete value 0 if not the abstract expression 0 (which would let you use a proof assistant to verify it for non-constant cases).

Re: Typing Is Hard

#69

Post by uyt »

seanmcdirmid wrote: post #64
dwhitney wrote: post #28

Earlier quoted context omitted.

I need to write a blog entry titled, "Your test suite is basically a sh*tty type system." -- I'm in the "totally anal" camp of type system aficionados :)

Or the converse “your type system is basically a very limited test suite.” Seriously though, these two concepts have some overlap that should be explored more.

Whenever I do leetcode, I use python. This is because most of the constraints that are useful to check in an algorithm can't be encoded as types. Instead I sprinkle a lot of asserts (possibly using slower bruteforce version of the code) to check invariants and properties that I expect to be true.

I think dependent types is supposed to solve this problem (for example, rather than just a list of ints, it can encode that it's currently a sorted list of ints) but they don't seem practical to use at the moment.

Re: Typing Is Hard

#70

Post by yen223 »

mastrsushi wrote: post #54

> Completeness A type checker is complete if it can check every correctly typed program. Do they mean as opposed to the type check system failing with the wrong data type detected?

A typechecker that is "complete" will always accept correctly-typed programs, but it may accept some incorrectly-typed programs.

A typechecker that is "sound" will always reject incorrectly-typed programs, but it may reject some correctly-typed programs.

Post reply on HN