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

Diminishing returns of static typing

blog.merovius.de

Post reply on HN
Print view View original

591–600 of 632 posts

Re: Diminishing returns of static typing

#591

Post by hota_mazi »

runT1ME wrote: post #584
hota_mazi wrote: post #475

Earlier quoted context omitted.

It's a pretty typical symptom I've seen a lot of hardcore FP developers exhibit: they forget how much time it took them to reach their level of mastery. It's like spending ten years learning to speak Russian and then criticizing anyone who says that learning Russian is difficult. Puzzling out scalaz code is difficult and requires an enormous investment in hours and practice, investment that a lot of people prefer to…

Yea, puzzling out some scalaz code takes investment. On the other hand, the library is used for web apps, network servers, database based applications, streaming libraries etc. It's incredibly multipurpose, more so than even Spring or Guava or LINQ, and these are things that developers regularly have to invest serious time in. The argument is just that FP libraries (like Scalaz) have a bigger payoff in the investment…

> The argument is just that FP libraries (like Scalaz) have a bigger payoff in the investment.

It depends on the people, not everybody has the inclination to dive so deep into hard core FP and they will be more productive using a different approach.

Don't make the mistake of thinking you've found the only software silver bullet that exists and that people who don't use it "don't get it", which is another attitude I've seen a lot of hardcore FP advocates embrace.

Re: Diminishing returns of static typing

#592

Post by tom_mellior »

naasking wrote: post #561
tom_mellior wrote: post #507

Earlier quoted context omitted.

> Dynamic type testing or introspection is not an essential feature of type systems. I didn't say so. An essential feature of type systems is being able to determine the types of (many) values, statically or dynamically. > You can not deference a floating point register as an address, for instance. So you'd agree that architectures that don't make a distinction between integer and floating point registers are untyped…

> It's just a very very weak one, so weak as to be almost entirely useless. Weak and strong aren't meaningful terms. A machine ISA might have an inexpressive type system and/or an unsound type system (because it conflates addresses and integers). > And the reason floating point registers are often separate from integer registers is not to provide this kind of "type safety", it's due to history and architecture. No, t…

>> It's for architectural reasons.

> No, it's for architectural reasons.

You win, I guess?

Re: Diminishing returns of static typing

#593

Post by igouy »

gnaritas wrote: post #571
igouy wrote: post #570

Earlier quoted context omitted.

Do you think having "the first commercial refactoring browser" is the same as "[a]utomated refactoring was invented in Smalltalk" ;-) Incidentally, what's your source for "Ralph Johnson… was the creator of the first Smalltalk refactoring browser" ?

Don't be a douche, obviously I don't think it's the same hence my comment. And I'm willing to bet, same as you, my source was Google to verify my memory of something I read long ago.

If I'd read it as obvious I wouldn't have made that comment: your name-calling is unhelpful.

We still don't know if you simply confabulated your other claim.

Re: Diminishing returns of static typing

#594

Post by seanwilson »

lisper wrote: post #578
seanwilson wrote: post #530

Earlier quoted context omitted.

> I'm pretty sure it would. Why do you think it would not? Languages like Coq require you to prove a function halts before it will compile. Yes, for an arbitrary function it can be arbitrarily difficult or impossible to prove termination. In most cases though, termination proofs aren't that complex (e.g. "it halts because the collection gets smaller each recursive call"). Besides, you're argument is basically soundin…

> Languages like Coq require you to prove a function halts before it will compile. Well, that's incredibly stupid. That means you can't write, for example, a web server in Coq unless you intentionally introduce undesirable behavior to satisfy the compiler. > because you can't prove all functions halt it's a waste of time proving any functions halt No. That's obviously a straw man. Can you please consider the possibil…

> Well, that's incredibly stupid. That means you can't write, for example, a web server in Coq unless you intentionally introduce undesirable behavior to satisfy the compiler.

There's ways around it (e.g. proving progress is always going to be made instead of termination) and there's a web server in Coq: http://coq-blog.clarus.me/pluto-a-first-concurrent-web-serve...

> 2. There are properties of interest that cannot be decided by static typing > > Which of those is the case is an empirical question but I submit that #2 is much more likely to be the case. Therefore, static typing cannot obviate the need to be prepared for your program to exhibit unexpected behavior at run time except in the most trivial cases.

Again, look at the sel4 project. It verifies the correctness of an entire OS showing that formal verification is powerful, practical and useful. Google for all the algorithms that have been formally verified with Coq, Isabelle and other proof assistants.

Why do you think it would be common properties of interest wouldn't be provable? Do you think mathematicians have this issue (there's not a lot of difference when you have expressive enough types)? You yourself must have an intuition about why the properties would be true so you should be able to write a formal proof of that although it can be very challenging currently.

Re: Diminishing returns of static typing

#595

Post by lomnakkus »

kazinator wrote: post #447
lomnakkus wrote: post #320

Earlier quoted context omitted.

It seems to me that you've just invented a static type checker. (Combined with a run-time type checker.) Am I mistaken? I mean, we can argue the semantics of what, exactly "static type checker" means, but...

Static checking doesn't make a "static language". A "static language" occurs when we have a model of program execution that involves erasing all of the type info before run-time. Or most of it. (Some static languages support OOP, and so stuff some minimal type info into objects for dispatch.) Note how above, my expression executes anyway; the checks produce only warnings. The warning for the lack of a binding for the…

This really sounds like "semantics" to me (not PL semantics! :).

For example, these days it's quite possible to ask GHC to defer type errors to runtime. Does that mean that the GHC dialect of Haskell is dynamically typed? This is basically a command line switch away, btw.

Retention of type information does not "dynamic typing" make. As a trivial example, consider C++ RTTI.

You really have just reinvented static (type) checking and a good runtime. There's no shame in that, but let's not pretend that these are opposing forces.

Re: Diminishing returns of static typing

#596

Post by lomnakkus »

naedish wrote: post #368
Guthur wrote: post #355

Earlier quoted context omitted.

Not sure it's really an invention, it's been around for awhile. Check any decent common lisp implementation.

I'm pretty sure he doesn't mean invented in a literal sense. The phrasing implies a meaning of reinvented.

Correct, I was being a little bit facetious. All in good fun, obviously :).

Re: Diminishing returns of static typing

#597

Post by zbobet2012 »

naasking wrote: post #480
s17n wrote: post #409

Earlier quoted context omitted.

There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. You can prove a program does what the types say it should do but that is not what "correctness" means. >Now a big part of the problem is expressing with sufficient accuracy what the properties of t…

> This is no different from writing tests in a dynamic language. Types and tests are not equivalent. This is a prevalent myth among dynamic typing enthusiasts. There is no unit test that can ensure, eg. race and deadlock freedom, but there are type systems that can do so. There are many such properties, and tests can't help you there. Types verify stronger properties than tests will ever be able to, full stop. You do…

To add some color here on the difference between a type proof and a test: consider that you can never test all possible strings for reverse.

However, a type proof can show that reverse, reverses all possible strings.

It is possible to test that a function on 16 bit integers returns the correct value for all inputs. Doing so would be a proof by exhaustion.

Type based proofs let us prove things using other methods than exhaustion, which is the only possible way to prove things with tests. That is an important property.

Re: Diminishing returns of static typing

#598

Post by girvo »

emodendroket wrote: post #376
girvo wrote: post #367

Earlier quoted context omitted.

To be fair, PHP 7.1 with Composer is a very different language to PHP 4, for the better of course.

Yeah, sure, and I was able to avoid the painful years. But C# pre-generics and pre-Linq is a way less appealing language too, you know? Most languages that are popular now look kind of rough to work in several versions ago.

Oh definitely. I think that’s the case for nearly any language that’s worth the code it’s written in. C++ is an interesting case study in how to do it both right and wrong; we’re spoilt for choice and it keeps getting better every day

Re: Diminishing returns of static typing

#599

Post by flukus »

mobiletelephone wrote: post #548
flukus wrote: post #426

Earlier quoted context omitted.

> C's built-in arrays are super weak, so you need some library to do proper resizable arrays. Since C doesn't have generics, such a library will use void * as the type for putting values into the array and getting them back out again. You'll be casting at every point of use, and nothing will check to make sure you got the cast right, other than running the code and crashing. There are other options though like macros…

I use a code generator. It has a great type system, it's composable, mature and it can even compile pretty fast with the right tooling. It's called C++!

Templates are good for some things but they only do a fraction of what code generators can do. With code generation you can generate types from database tables, web APIs, etc. You can do things like declaratively declaring database views and generate huge chunks of an application. It can handle all sorts of boiler plate code that you can't do with templates alone.

Re: Diminishing returns of static typing

#600

Post by yawaramin »

hellofunk wrote: post #505
yawaramin wrote: post #497

Earlier quoted context omitted.

May I ask what your experience of statically-typed languages has been? I find that most people have had a common experience where they didn't get to work in tandem with a fast compiler and a succinct language which inferred most or all types for them, and so their perceptions are coloured by that.

Swift, C++, Haskell (a little), Elm (more than a little)

May I recommend giving ReasonML a try? Trust me when I say, you've never seen a faster compiler (except maybe C). Try writing a little experiment in ReasonReact and seeing the speed for yourself: https://reasonml.github.io/reason-react/
Post reply on HN