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

71–80 of 134 posts

Re: Typing Is Hard

#71

Post by KMag »

lmm wrote: post #63
KMag wrote: post #60

Earlier quoted context omitted.

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.

I guess then you'd need another mechanism for dealing with re-defining APIs in incompatible ways within the REPL. It's a pretty common use case for REPLs to play around with APIs and temporarily break them.

The best alternative is to keep a map of all of the definitions with broken type checks, and refuse to generate new machine code/bytecode as long as that map is non-empty, and keep using the older definitions until again get back to a sound state of the world.

Re: Typing Is Hard

#72

Post by jcelerier »

lmm wrote: post #37
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…

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

> It absolutely will, and it's a massive pain when it does.

C++ compilers have solved that problem 20 years ago by putting (low) depth limits to type computations, why can't other environments do the same ?

Re: Typing Is Hard

#73

Post by jcelerier »

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.

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

the converse doesn't hold. You can write new code that will benefit from the guarantees of existing types. But you'd have to write new tests if you didn't have types.

Re: Typing Is Hard

#74

Post by arcturus17 »

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.

Slightly off-topic, but say I know Python and JavaScript and I wanted to add a multi-paradigm language with strong typing to my toolbelt. I'm looking for something with a strong functional programming core but with object-oriented facilities as an "escape hatch".

The languages I've been eye-balling are Scala, Kotlin and F# (I'm separately eyeing Elixir, but since it's dynamic, I'd leave it out of this particular discussion)

My main requirements are that it's a "builder's language" with a great ecosystem for web development and growing mainstream adoption. I'm a general-purpose product engineer building apps end-to-end, and I favor general ergonomics and ease of use over other characteristics (performance, functional purity, etc.)

I'm assuming from your comment you've tried both Scala and Kotlin and favor the later - would you bet on it knowing the above?

Others are welcome to join in the discussion.

Re: Typing Is Hard

#75

Post by ygra »

lmm wrote: post #37
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…

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

> and then two days writing them in Scala.js

But Scala is, according to that list, just as undecidable and unsound as TypeScript. Are the places where you can't trust your types just more esoteric there?

Re: Typing Is Hard

#76

Post by lmm »

ygra wrote: post #75
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…

> and then two days writing them in Scala.js But Scala is, according to that list, just as undecidable and unsound as TypeScript. Are the places where you can't trust your types just more esoteric there?

It's practical to restrict yourself to a sound subset of Scala (the soundness issue they mention applies to a specific usage pattern that you can ban with a linter), and the issue is outright fixed in Scala 3.

The undecidability is real but you at least get what you're paying for - a certain amount of type-level programming is practical and useful in Scala. I'm not sure it's the right tradeoff but it's on (or at least close to) the Pareto frontier in a way that many languages aren't.

Re: Typing Is Hard

#77

Post by adenozine »

darksaints wrote: post #40

I think I remember reading that Scala 3.0 introduced some backwards incompatibility in order to make the type system sound. Anybody aware of what had to change?

Check out Dotty and some of the papers on DOT calculus. Sorry, on mobile or I'd link you. Scala 3 has some different fundamentals. I don't think it's all the way sound like idris, but there's a lot of new rules underneath the hood to have types be much safer.

I hate Scala, but I gotta admit the future of it looks a little promising if they nail the transition

Re: Typing Is Hard

#79

Post by elwell »

augusto-moura wrote: post #17
whoisburbansky wrote: post #2

Clicked expecting a treatise about ergonomics and keyboard layouts, came away with slightly more appreciation for Rust’s long compile times.

Same Would benefit from a article about RSI though

Delivered: https://news.ycombinator.com/item?id=12986759

Re: Typing Is Hard

#80

Post by atoav »

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 :)

Rust made me realise the truth in this. Using a sound type system wisely removes a whole class of things that can go wrong.

It can be exhausting to use if you never learned how to use it, but if you got the hang of it, you can program more freely because reasoning about what is going wrong becomes easier.

Post reply on HN