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

421–430 of 632 posts

Re: Diminishing returns of static typing

#421

Post by rbobrowicz »

yogthos wrote: post #351
cm2187 wrote: post #3

The benefit of static typing isn't just reliability. Tooling is another major argument. Won't appeal to certain hardcore programmers who think that even notepad has too many features. But it is great for refactoring, finding all references to a function or a property or navigating through the code at design time. Basically all the features visual studio excels at for .net languages. And I disagree with the barrier to…

A lot of the same refactoring is possible in dynamic languages as in static ones. I recommend reading up on Term to see what's possible to do with JavaScript http://marijnhaverbeke.nl/blog/tern.html I use Cursive https://cursive-ide.com/ for working with Clojure, and it can do safe refactoring for symbols by doing static analysis of the source. It can show all usages of a symbol, rename it, do automatic imports, and…

For someone only passingly familiar with Spec, what's the benefit of Spec over just using a property based testing framework like Haskell's QuickCheck (and I think Clojure's test.check)?

I can encode all those invariants as QuickCheck properties and have them automatically tested against random inputs on every test run. It's still all runtime verification, but with random inputs I actually have more confidence of hitting a corner case than with just asserting during regular program runs or hand written example tests.

Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1]. And while a machine checked proof of your sorting algorithm is nice, it might be hitting the diminishing returns point the article mentions over just using property tests.

[1] https://github.com/davidfstr/idris-insertion-sort

Re: Diminishing returns of static typing

#422

Post by dozzie »

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.

> The C compiler picks up on that, too.

Except when it's not. Just five days ago I was debugging an error in my Erlang port driver that was caused by me passing receiver (ErlDrvTerm, an int in disguise) in the place where I wanted number of iterations. The funnier thing was that the declaration of the function had the arguments in correct order (and that's what guided me), but definition had them swapped. The compiler did not catch that bug, because, well, both are ints, so apparently the declaration and definition match, don't they?

Re: Diminishing returns of static typing

#423

Post by mpartel »

xfer wrote: post #365
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,…

Rust doesn't have anyway to manage side-effects in types ..

Don't mutable and immutable references with lifetimes count? Sure, one could argue whether the borrow checker is really part of the type system, but it's a compile-time check either way.

Yes, in the standard library, an immutable object can hide mutable state in e.g. a 'Mutex', and effects to the external system aren't wired through anything like monads or unique objects.

I see those as compromises Rust makes in the name of pragmatism and being a system'ey language. I don't necessarily like all of them, but I find the general uniqueness typing based approach interesting.

See articles comparing Clean and Haskell for an interesting historical perspective, including how both approaches could be used to model side-effects in a purely functional language. Haskell "won", possibly because it was seen as more generic and composable. I always felt Clean's approach had merit too, so I was really glad to see Rust bring the idea, or a closely related idea, to prominence.

Re: Diminishing returns of static typing

#424

Post by fabioz »

danharaj wrote: post #28
agentultra wrote: post #10

I think what's often missing from these arguments is that statically checking (or inferring) homogenous lists is probably one of the most superficial uses of the type system in Haskell (and indeed not the interesting feature most power-users of Haskell are interested in as far as I can tell). What is interesting is using the type system to specify invariants about data structures and functions at the type level befor…

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 find that people doing these claims have seldomly really worked in large Python codebases...

Personally, I find it pretty workable in Python with a big codebase (but you have to respect the rules like having a good test suite -- you change the time from compiling to running your test suite -- which you should have anyways)...

I find that the current Python codebase I'm working on (which has 15 years and around 15k modules -- started back in Python 2.4, currently in Python 2.7 and going to 3.5) pretty good to work in -- there's a whole class of refactoring that you do on typed languages to satisfy the compiler that you don't even need to care about in the Python world (I also work on a reasonably big Java source codebase and refactorings are needed much more because of that).

I must say I'm usually happier on the Python realm, although, we do use some patterns for types such as the adapter protocol quite a bit (so, you ask for a type and expect to get it regardless of needing a compiler to tell you it's correct and I remember very few cases of errors related to having a wrong type -- I definitely had much more null pointer exceptions on java than typing errors on Python) and we do have some utilities to specify an interface and check that another class implements all the needed methods (so, you can do light type checking on Python without a full static checking language and I don't really miss a compiler for doing that type checking...).

I do think about things such immutability, etc, but feel like the 'we're all responsible grown ups' stance of Python easier to work with... i.e.: if I prefix something with '_' you should not access it, the compiler doesn't have to scream that it's private and I don't need to clutter my code -- you do need good/responsible developers though (I see that as an advantage).

Re: Diminishing returns of static typing

#425

Post by emodendroket »

19873287234 wrote: post #43
cle wrote: post #13

Earlier quoted context omitted.

IMO the autocomplete argument is rather unconvincing. Every dynamic language I've worked deeply with has powerful and simple introspection capabilities, and they generally come with much more interactive development environments (shell/REPL), so I've never found API discoverability to be any worse than statically typed languages, just different. In general though, the more you can formally reason about the program, t…

The thing about magical refactoring though is that it often isn't a good idea. You usually don't just change the name of something, but you change it conceptually. If you just let the ide go and change the name everywhere, you create bugs because you never actually went and made sure the old code was updated for the new concept, rather than just the name.

That's not really true.

Re: Diminishing returns of static typing

#426

Post by flukus »

mikeash wrote: post #405
Sir_Cmpwn wrote: post #268

Earlier quoted context omitted.

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

> 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 and code generation. Code gen in particular can give you more options than generics without sacrificing any type safety.

Re: Diminishing returns of static typing

#427

Post by mpartel »

runT1ME wrote: post #418
mpartel wrote: post #417

Earlier quoted context omitted.

Not sure about LINQ, I thought that was "just" syntactic sugar for a bunch of collection methods. Are you refering to extension methods as an unfortunate prerequisite? But I think I get your general point: things like 'Control.Concurrent.Async' ('async'/'await') and 'Control.Monad.Coroutine' ('yield') are libraries that implement some and very generic type classes: 'Functor', 'Applicative', 'Monad'. This then lets yo…

>They seem to have huge potential for hard to follow code as you need to mentally unpack and remember more layers of abstraction That's the beauty of abstraction without side effects, you don't need to unpack anything. If you know what the inputs are and the outputs are, you don't need to know how it works or what type classes are even used to transform certain things. People use sequence all the time in Scala, not r…

Fair point about 'sequence'. There are probably a bunch of these I use regularly in Scala without realizing it. Though as a counterpoint, 'Future.sequence' wouldn't really lose _that_ much if it didn't return a collection of the same type. And I haven't yet felt the need for a generic `sequence`, which I'm sure scalaz has.

I don't buy your point about not needing to unpack side-effectless code, however. There are _always_ reasons to dig into code, be it bugs, surprising edge cases, poor documentation, insufficient performance, or even just curiosity. And those high-level abstractions tend to be visible in module interfaces too. I remember some Haskell libraries being very hard to figure out how to use if you didn't know your category theory :)

Re: Diminishing returns of static typing

#428

Post by breatheoften »

metaphorm wrote: post #176
macspoofing wrote: post #60

Earlier quoted context omitted.

I'm so happy to see the pendulum swing the other way, because when JavaScript was becoming popular, and Ruby and Python had a popularity renaissance (around mid to late 2000s), I had a lot of online arguments about the value of static typing. People were complaining about static typing for the dumbest reasons (it's too 'wordy'). It started as a backlash against old-school enterprise Java development (which was fair,…

The type systems of Java and C/C++ are the most commonly encountered ones and by far the most widespread in industry programming (as opposed to academia/research) and they are actually awful and really add a lot of friction and inertia to developing. Being free of that kind of type system when using a language like Python really does feel like a big upgrade. There is a different problem with the more powerful and use…

I think Typescript is significantly easier to learn than JavaScript.

Re: Diminishing returns of static typing

#429

Post by oldandtired »

It has been interesting to see the to and froing of arguments for and against static typing in the discussions here.

Though I am not a type theorist (I only dabble in compilers and language design), I have noted that many people conflate static typing and dynamic typing with other additional ideas.

Static typing has certain benefits but also has certain disadvantages, dynamic typing has certain benefits but also has certain disadvantages.

What I find interesting is that few people fall into the soft typing arena, using static typing where applicable and advantageous and using dynamic typing where applicable and advantageous.

Static typing has a tendency in many languages to explode the amount of code required to get anything done, dynamic typing has a tendency to produce somewhat brittle code that will only be discovered at runtime. The implementation of static typing in many languages requires extensive type annotation which can be problematic.

But what is forgotten by most is that static typing is a dynamic runtime typing situation for the compiler even when the compiler is written in a static typed language.

Instead of falling into either camp, we need to develop languages that give us the beast of both world. Many of the features people here have raised as being a part of the static typing framework have been rightly pointed out as being of part of the language editors being used and are not specifically part of the static typing regime.

Many years ago a similar discussion was held on Lambda-the-Ultimate, and the sensible heads came to the conclusion that soft typing was the best goal to head for. Yet, in the intervening years,when watching language design aficionados at work, they head towards full static typing or full dynamic typing and rarely head in the direction of soft typing (taking advantage of both worlds).

S, the upshot, this discussion will continue to repeat itself for the foreseeable future and there will continue to NOT be a meeting of minds over the subject.

Re: Diminishing returns of static typing

#430

Post by voidmain »

lisper wrote: post #401
voidmain wrote: post #394

Earlier quoted context omitted.

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…

I think you have missed my point. I am not saying that humans are able to solve the halting problem! Nor am I saying that static verification is always better than testing. I am saying that you don't need a halting oracle to express and verify arbitrary properties in a static type system, because a static type system can and will reject programs that would not have type errors dynamically.

If you write this program in a statically checked language:

    let x : int = 6
    let y : int = 3
    while true:
      if y>x then break
      if is_prime(y) and is_prime(x-y) then
        x = x + 2
        y = 3
      else
        y = y + 2
      endif
    x = "foobar"
I can tell you that it will not type check. And for the same reason, if you write the same program in a language that can express termination and claim that it terminates, the program will not type check until you have supplied a proof of (edit: the negation of!) Goldbach's conjecture in a form that the type system understands.
Post reply on HN