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

401–410 of 632 posts

Re: Diminishing returns of static typing

#401

Post by lisper »

voidmain wrote: post #394
lisper wrote: post #388

100% statically-type-checked code != 100% bug-free code. That would require solving the halting problem. So you have to test everything anyway if you need high reliability.

This argument is incorrect. The "halting problem" is the problem of determining if an arbitrary program halts. It is not impossible to prove, and verify mechanically, that a particular program halts. The state of the art is not up to proving every desirable property of every program that we would like to build. But that has nothing much to do with computability. And some extremely impressive things have been done, li…

> It is not impossible to prove, and verify mechanically, that a particular program halts.

OK, let's put that to the test. Here is a particular program:

    let x = 6
    let y = 3
    while true:
      if y>x then halt
      if is_prime(y) and is_prime(x-y) then
        x = x + 2
        y = 3
      else
        y = y + 2
      endif
Can you tell me if it halts or not?

> The state of the art is not up to proving every desirable property of every program that we would like to build.

Isn't that exactly the same as what I said?

> But that has nothing much to do with computability.

What does it have to do with then?

> some extremely impressive things have been done

Yes, in some very particular cases. But note that even a proof of correctness is not a guarantee that the code is bug-free.

http://spinroot.com/spin/Doc/rax.pdf

Re: Diminishing returns of static typing

#402

Post by sordina »

solatic wrote: post #122

OP draws a false one-dimensional relationship between types vs tests in terms of code quality. Writing expressive types instead of tests does much more than affect a quality curve - it changes the way you approach the problem you are trying to solve. The classic Haskell example is understanding how IO being a monad allows you to push impurity to the edge of your system. Start-ups decide not to write MVPs in languages…

Sorry to contradict you, but we wrote an mvp in rails even though we have 3.5 experienced Haskell programmers on staff. We did this because we knew we could build some web stack apps with all the trimmings much faster in ror. So there is at least one counter example.

Re: Diminishing returns of static typing

#403

Post by flavio81 »

boramalper wrote: post #390
flavio81 wrote: post #301

Earlier quoted context omitted.

>What exactly does it mean to have "good dynamic typing facilities"? Picking Common Lisp as an example: (NOTE: Some of the features are also present in good statically typed languages as well, so what I advocate is to use good, well-featured languages, not really static vs dynamic.) (NOTE 2: I'm sorry for being such a fanboy, but that thing is addictive like a hard drug...) 0. Code is a first class citizen, and it ca…

> 3. The error handling system is exemplary: Not only designed to "catch" errors, but also to apply a potential correction and try running the function again. This is known as "condition and restarts", and sadly is not present in many programming languages. I found this extremely weird and (or hence ) interesting at the same time. Where can I read more about this?

You are welcome, sir! How about this chapter of the famous book "Practical Common Lisp", available online for free?

http://www.gigamonkeys.com/book/beyond-exception-handling-co...

Re: Diminishing returns of static typing

#404

Post by jackmott »

alkonaut wrote: post #265

There are 3 main areas of interest in the discussion of benefits of static vs dynamic typing. - Quality (How many bugs) - Dev time (How fast to develop) - Maintainability (how easy to maintain and adapt for years, by others than the authors) The argument is often that there is no formal evidence for static typing one way or the other. Proponents of dynamic typing often argue that Quality is not demonstrably worse, wh…

performance at runtime is usually factor in type systems as well.

Re: Diminishing returns of static typing

#405

Post by mikeash »

Sir_Cmpwn wrote: post #268
danharaj wrote: post #28

Earlier quoted context omitted.

List typing isn't as superficial as it seems. The following has happened to me multiple times, perhaps in the last month : I have a large code base. I want to replace a fundamental data structure to support more operations/invariants/performance guarantees. I change the type at the roots of the code base. My instance of ghcid notifies me of the first type error. I fix it. This repeats until the program compiles again…

I don't really the lumping of C in with Python and Ruby here. The C compiler picks up on that, too. All over this comment section people are calling C weakly typed, I don't get it. Is it because void* exists? Every language has something like that.

It's not just that void * exists, but that it's basically mandatory.

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.

Re: Diminishing returns of static typing

#406

Post by flavio81 »

passivepinetree wrote: post #381
flavio81 wrote: post #312

Earlier quoted context omitted.

>There is dynamic and then there is crap dynamic. (...) There is crap static too. Excellent. My point exactly. I have no fear of using a static or dynamic language, as long as it is a good implementation of a statically (or dynamically) typed language.

What would you consider good implementations of either?

Good "statics": Haskell, ML family, maybe Rust.

Good "dynamics": All the Lisp-family languages. Smalltalk. Julia. Lua. Tcl.

Re: Diminishing returns of static typing

#407

Post by yorwba »

underwater wrote: post #392
DubiousPusher wrote: post #73

Earlier quoted context omitted.

Yup, love that about statically typed languages. This happens all the time for me in C#. I have several libraries I like that do a lot of code generation. When the project is young, directly handling the generated classes works well but as the project grows, I inevitably want to wrap the handling of the generated classes. It's awesome to be like, welp... it's time to handle this one type differently. Change the retur…

I’d argue that code generation is an anti—pattern that is only necessary because of static typing. A dynamic language would let you change the implementation of all generated objects simultaneously.

Code generation by macros is an important feature of Lisps, which tend to be dynamically typed. Maybe it feels less like code generation when you don't also have to produce the correct type annotations, but a good inference engine can eliminate most of those from statically typed languages as well.

Re: Diminishing returns of static typing

#408

Post by AndrewBissell »

willtim wrote: post #363
mpartel wrote: post #158

Earlier quoted context omitted.

In my subjective opinion, Haskell has taken abstraction way past the point of diminishing returns, at least for the problems I tend to work on. A large portion of advanced Haskell type system features seem to be about emulating things you could do with side-effects. I guess I prefer Rust's approach to managing side-effects, or even just Scala's implied convention of: use 'var' very sparingly, and mostly locally. Yes,…

As a counterexample, C# needed expensive language extensions to accommodate both LINQ and Async/await. Both can be implemented in Haskell purely as a library, thanks to HKTs. Both Java and C# tend to rely heavily on frameworks such as Spring to workaround issues with the expressivity of the languages. This causes problems when one needs two frameworks (they don't in general compose). In Haskell, HKTs allow one to wri…

I'm not sure what Java expressivity problem Spring is meant to solve. XML configs are basically just a duplication of what would be done in a static initializer, except you lose type-checking and get to find your wiring mistakes at startup time instead of compile time. Autowiring annotations can be nice when you first use them, but become inscrutable magic once some other poor sap has to come along and make changes to the original project setup.

I just don't understand what is so horrible and inexpressive about a static initialization block.

The only possible purpose I see to Spring is if for some reason you really need to be able to change how your dependencies are injected at runtime. (90% of Spring apologists point to this, and 99% of them never use it in practice.) Even then, I don't see how a Spring XML config file (which I have seen run to 4000+ lines, to my horror) is better than just reading some settings out of a properties file to pick an implementation in your static initializer.

Re: Diminishing returns of static typing

#409

Post by s17n »

zbobet2012 wrote: post #281
pdonis wrote: post #127

Earlier quoted context omitted.

> Static typing prevents bugs in code to the degree that the programmer can correctly encode the desired behavior of the program into the type system. Exactly. The author of the article implicitly equates "statically verified code" with "bug-free code". But that's not correct. It's quite possible (and even, dare I say it, fairly common) to have code that expresses, in perfectly type-correct fashion, an algorithm that…

It depends on your type system. In new languages like Idris or F* you can encode in the type the correctness of an algorithm and it will not compile if the compiler can not prove that correctness. For example I can prove my my string reverse works in Idris ( https://www.stackbuilders.com/news/reverse-reverse-theorem-p... ). Or I could prove that my function squares all elements in a list. Etc. Now a big part of the p…

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 the algorithm you want to prove are. For example for string reverse I may want to show more than that `reverse (reverse s) = s`. Since after all if reverse does nothing that would still be true. I would probably want to express that the first and last chars swap when I just call reverse xs.

This is no different from writing tests in a dynamic language.

Re: Diminishing returns of static typing

#410

Post by katastic »

This site has a strange fascination with hatred of static languages. I really don't get it. My only guess is that modern colleges teach dynamic languages to students and so they're more familiar with it. Perhaps their teachers even stress that static languages are inferior.

To me, it's right tool for the right job. I have no problem spinning up a static language for performance and outsourcing the scripting to a dynamic language like Python for the best of both worlds in terms of speed, and rapid development.

Post reply on HN