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

Why Type Systems Matter

matthias-endler.de

Post reply on HN
Print view View original

31–40 of 103 posts

Re: Why Type Systems Matter

#31

Post by willtim »

benhoyt wrote: post #18

Counterpoint I wrote a while back that focuses on compilation speed: http://benhoyt.com/writings/language-speed/ I've used Scala a fair bit recently, and the compiler is so dog slow it's painful. Maybe it's just my relative fluency with Python, but I find I'm much more productive with Python's almost instant edit-compile-run sequence. Edit: I do like many of the benefits of static typing, though. I think mypy is comi…

There's no reason why a statically typed language cannot also use an interpreter and avoid expensive optimisation and code generation upfront. For example, GHC Haskell has an interpreter, runHaskell, that will run a Haskell program straightaway with little delay (type checking is fast).

Re: Why Type Systems Matter

#32

Post by blauditore »

I thought this was quite clear, and it's what I've always been missing in languages like Python or JS. Yet I meet many devs, especially coming from such languages, making fun of Java for its verbosity and clumsiness.

On the other hand, it leads to some people abusing the static type system: They just randomly change types until it somehow compiles, without thinking about what their doing.

Re: Why Type Systems Matter

#33

Post by falcolas »

There is never a person more zealous (and vocal in their zealotry) than a new convert. You don't see the bad points, just the good.

That's how this post comes across: "Types are so awesome, let me show you how awesome types are!"

Come back in two years, show us how the types feel after the honeymoon is over.

Re: Why Type Systems Matter

#34

Post by wutbrodo »

rdtsc wrote: post #3

Good post, but note all those things you don't need a statically typed language. Erlang for example is a dynamically typed language but it has Dialyzer - a type checker. The more precisely you define the types the more discrepancies and issues it will find in the code, exactly the kind of stuff the author mentions. http://learnyousomeerlang.com/dialyzer That's technically called "success typing" http://www.it.uu.se/r…

> Good post, but note all those things you don't need a statically typed language.

> Python has that too with MyPy.

I don't know much about Erlang's typing, but this claim is definitely untrue. I run a code base with five engineers and I'm pretty disciplined about asking for type annotations wherever appropriate, and I still miss static typing every damn day. The grafted-on approach is definitely beneficial, and I frankly don't understand how people ran Python engineering projects of any significant size without it, but it has just enough holes in it that the type inference chain breaks often (ie just drops to type Any). It also gives false positive errors just often enough that it lowers your sensitivity to real errors.

Don't get me wrong, I'm happy it exists. But Python with types is a poor imitation of a proper engineering programming language.

Re: Why Type Systems Matter

#35

Post by dragonwriter »

thanatropism wrote: post #28
msla wrote: post #14

Earlier quoted context omitted.

The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point, but maybe I can do something to, at least, explain the position of the people who don't conflate those terms: Strong typing is about creating, expressing, and enforcing a contract which determines which operations are valid on which values. Not variables, values . Having the semantics of the value in the compil…

Honest question: Is Python-with-type-hinting-in-function-definitions (and maybe type assertions) equally as "strong" as common style Python? It's not static typing -- it's not Haskell -- but it's already a step further. Edit: I find myself doing a lot of "assert isinstance(x,foo)".

Haskell types don't exist at runtime. If you use a static analyzer like mypy, Python types are “static” in the same sense as Haskell (statically verified as correct in advance), though mypy’s type system is less robust than Haskell’s.

Re: Why Type Systems Matter

#36

Post by mcphage »

blauditore wrote: post #32

I thought this was quite clear, and it's what I've always been missing in languages like Python or JS. Yet I meet many devs, especially coming from such languages, making fun of Java for its verbosity and clumsiness. On the other hand, it leads to some people abusing the static type system: They just randomly change types until it somehow compiles, without thinking about what their doing.

> making fun of Java for its verbosity and clumsiness

Java has a particularly verbose and clumsy type system.

Re: Why Type Systems Matter

#37

Post by sk5t »

mixedCase wrote: post #13
rocky1138 wrote: post #2

Strong typing is great when I've already made sense of how the logic should flow and I'm ready to solidify my work into something stable and extensible over time. It's not so great when I'm trying something new and am still trying to work out if what I want to do is even possible, since I find myself trying to identify the right type to use in a given situation rather than proving that I'm even able to do it. A lot o…

With a good type system, instead of writing algorithms first you would write data structures that convey the ideas behind the software's intent clearly. Then you start writing the algorithms that manipulate these data structures. If what you're trying to do is viable, then you'll be able to express it in the domain model.

Yes! I've found it quite effective to start new problems with some (mostly composition-based) types as a means of jotting down the core inputs and outputs, then work out towards the edges in both directions with deserializers/readers/parsers in one direction, and repositories and work-doing algorithms in the other direction. A little dependency injection to wire the pieces together in complex systems and you're in business.

Re: Why Type Systems Matter

#38

Post by thanatropism »

dragonwriter wrote: post #35
thanatropism wrote: post #28

Earlier quoted context omitted.

Honest question: Is Python-with-type-hinting-in-function-definitions (and maybe type assertions) equally as "strong" as common style Python? It's not static typing -- it's not Haskell -- but it's already a step further. Edit: I find myself doing a lot of "assert isinstance(x,foo)".

Haskell types don't exist at runtime. If you use a static analyzer like mypy, Python types are “static” in the same sense as Haskell (statically verified as correct in advance), though mypy’s type system is less robust than Haskell’s.

I'm not knowledgeable of this stuff, but I'll keep taxing your patience until you tell me to stop.

Haskell types don't exist at runtime... because Haskell code (like with any other compiled language) gets translated to a lower-level machine language that works with untyped memory addresses?

Or are you saying that (for example) Fortran types are closer to the metal somehow?

Re: Why Type Systems Matter

#39

Post by shakna »

gumby wrote: post #16

Some languages mix static and dynamic typing. For example MACLISP used this to great effect to make MACSYMA super fast. All the numeric code was statically typed and the compiler built code that was as fast as hand crafted assembly. Yet you could write conventional Lisp code that called this static code just like any other code. MACLISP derivatives like lisp machine lisp also implemented this stuff and used it for sy…

C++ is in this boat now.

Most of the time I'd recommend the new type-safe union std::variant, but std::any is there.

It is kinda a static type, but as a container-type of anything in the type system, it may as well be a dynamic type.

---

> All that survived into Common Lisp but I am not up on the current state of lisp implementations and have no idea if people bother to take advantage of it any more.

Typed Racket uses the early guard theories from CL [1], and it does have an optimiser [2], though it has some quirks.

And though I can't find it now, there was a fairly recent research paper on using a macro system to static type check at compile-time and optimise for Scheme. But, I should point out that Scheme doesn't need it for optimisation - compiling Scheme to C is easy, and easy to make the result fast. Its more about safety.

And there's always Shen which uses sequent calculus [3] for their optional static type system.

[0] https://docs.racket-lang.org/ts-guide/

[1] http://www.cs.utexas.edu/users/boyer/ftp/diss/akers.pdf

[2] https://docs.racket-lang.org/ts-guide/optimization.html

[3] http://shenlanguage.org/learn-shen/index.html#10%20Sequent%2...

Re: Why Type Systems Matter

#40

Post by msla »

thanatropism wrote: post #28
msla wrote: post #14

Earlier quoted context omitted.

The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point, but maybe I can do something to, at least, explain the position of the people who don't conflate those terms: Strong typing is about creating, expressing, and enforcing a contract which determines which operations are valid on which values. Not variables, values . Having the semantics of the value in the compil…

Honest question: Is Python-with-type-hinting-in-function-definitions (and maybe type assertions) equally as "strong" as common style Python? It's not static typing -- it's not Haskell -- but it's already a step further. Edit: I find myself doing a lot of "assert isinstance(x,foo)".

It seems like it's about as strong, in terms of what types it knows about, but it allows more error detection at "compile time" or, at least, the time at which you run the static type-checking code on the codebase. As Guido said, this is like a super-linter.

https://www.python.org/dev/peps/pep-0484/

(I remember C linters trying to expand the C type system by doing things like complaining if you used non-boolean expressions in a boolean context, well before C had an actual bool type.)

Post reply on HN