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

31–40 of 134 posts

Re: Typing Is Hard

#31

Post by bottled_poe »

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

I like it, but try convincing the client that we don’t need to test the software :)

Re: Typing Is Hard

#32

Post by dtwhitney »

bottled_poe wrote: post #31
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 :)

I like it, but try convincing the client that we don’t need to test the software :)

Do you take me for a fool, sir? I know this can't be done.

Re: Typing Is Hard

#34

Post by rsrsrs86 »

Most comments here are asking guarantees from type checkers that actually belong to semantic analysis and static analysis in general but not necessarily related to type checking.

Re: Typing Is Hard

#35

Post by higerordermap »

username90 wrote: post #22
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 think that having a compromise between types and untyped is best. So first, have a type all other types can be cast to, call it object and allow it to perform generic operations. Then have a type that can be cast to all other types, call it null. These two gives you a lot of the nice parts of untyped languages while still allowing for tooling like quick refactoring or name completions. When I code in a system lacki…

so, interface{}

Re: Typing Is Hard

#37

Post by lmm »

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 amazing how much of a productivity drag it is when you can't quite trust your types, but you'd never know that if you've not used an ML-family language.

> So what if the type checker can infloop? It won't in practice.

It absolutely will, and it's a massive pain when it does. You type something in your IDE and your error squiggles don't update, maybe (if you're lucky) you get a warning that compilation is taking a long time. It's very hard to distinguish between "it's just being slow" and "it's gone into an infinite loop".

Re: Typing Is Hard

#38

Post by lmm »

rsrsrs86 wrote: post #34

Most comments here are asking guarantees from type checkers that actually belong to semantic analysis and static analysis in general but not necessarily related to type checking.

Type checking is not the only conceivable way of achieving those guarantees, but it's effective and at least somewhat understood by most working programmers, so why do something different for the sake of it?

Re: Typing Is Hard

#39

Post by lmm »

abeppu wrote: post #3

I guess, unsoundness sounds concerning. But is undecidability? When this is an issue, it's always because someone worked to do some really elaborate or general compile-time computation. It seems a lot (literally too much) to ask that you can do really unrestrained type-level computation and also still always have termination.

It might seem a lot, but Idris shows that it's possible.

Re: Typing Is Hard

#40

Post by darksaints »

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