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

61–70 of 103 posts

Re: Why Type Systems Matter

#61

Post by kmill »

naasking wrote: post #46
kmill wrote: post #24

Earlier quoted context omitted.

> What makes you think being able to run such half-specified programs for part of the problem will actually help with answering this question? Perhaps rocky1138 thinks this because they have experience answering this question by doing so? I've found it can be hard to find the right type before I've written partial solutions to a problem. Just to be clear, I'm talking about recognizing the monads or functors or what h…

> Perhaps rocky1138 thinks this because they have experience answering this question by doing so? They have experience with their problem solving style, they don't have experience with every problem solving style, or even necessarily with my problem solving style. You can't infer much from that, and certainly not that typing is "not great when prototyping". > Just to be clear, I'm talking about recognizing the monads…

> They have experience with their problem solving style, they don't have experience with every problem solving style, or even necessarily with my problem solving style. You can't infer much from that, and certainly not that typing is "not great when prototyping".

I tend to grant the first person who states their opinion in absolutes the nicety of automatic insertion of "it is my opinion/experience that," because this is what they usually mean. Countering absolutes with absolutes is just confusing to me, so sorry for any misunderstanding.

> but to think you've captured anything meaningful or coherent without type checking is bizarre

I want to say "speak for yourself" here---this is rather dogmatic. Sometimes I use a formal type system, sometimes I don't, and yet in both cases I somehow manage to produce working programs. Sure, a computer-checkable type system is nice to have and gives me peace of mind when I use one, but I believe formal type systems are a posteriori describing particular safe ways of manipulating data out of all the possible ways of manipulating data. Is in inconceivable that a programmer can check their types manually, using an ad hoc intuitive type system?

> but those partial solutions only come together in a coherent whole if they're typed. Otherwise they likely won't mesh well, and you're left with a mishmash of partial solutions, not a solution.

Check your types: "If they are not typed, they won't come together into a coherent whole because they likely won't mesh well."

Truthfully, it sounds to me like your argument is the Fred Brooks quote about how the data structures imply the code. This is not exactly the same as having machine-checkable type systems, though such systems do force the issue.

Re: Why Type Systems Matter

#62

Post by dozzie »

rocky1138 wrote: post #50
seanwilson wrote: post #11

Earlier quoted context omitted.

Can you give an example? I don't find this personally. I find static strong typing speeds me up because I don't have to restart the app, click some buttons etc. to figure out some code was wrong. This is true even for prototypes. Most of the time any type declarations you need are straightforward and once you know your code better you can start introducing more exotic types to capture more errors later.

A really basic example would be the "as GameObject" part of this statement in C#: `GameObject gameObject = GameObject.Instantiate(MyGameObject, Vector3.zero, Quaternion.Identity) as GameObject;". It's annoying to have to type "as GameObject" when very clearly I am creating a GameObject type (the first thing in the entire statement). Programming languages should be smart enough to figure out that's what I'm trying to…

First, this annoyance does not come from static typing, it comes from C#'s type system. There are statically typed languages where you just construct the value and assign it to a variable, and compiler infers variable's type for you (e.g. OCaml).

Then, typing the class name is a trivial matter. My editor offers me a generic text completion command, so I don't type full "GameObject", I just type "Ga" and hit ^P. Maybe you should try using a good text editor?

Re: Why Type Systems Matter

#63

Post by dozzie »

msla wrote: post #14
shalabhc wrote: post #5

Earlier quoted context omitted.

> Strong typing I think you mean 'static' typing, not strong? Python is already strongly typed. > 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 I completely agree here. I find it very useful when iterating to run the program and verify just the code path that gets executed, without worrying about whether the rest of the program is also correctly…

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…

> The conflation between 'strong' and 'static', and 'weak' and 'dynamic', is probably terminal at this point,

Type system of C is weak and static.

Type system of JavaScript is weak and dynamic.

Type system of Lisp is strong and dynamic.

Type system of OCaml is strong and static.

Type system of Python is dynamic. It may be strong or weak, depending on your opinion about duck typing (does it weaken the type system or not?).

Re: Why Type Systems Matter

#64

Post by dom0 »

wutbrodo wrote: post #34
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 fr…

> and I frankly don't understand how people ran Python engineering projects of any significant size without it

Pretty much the first thing the Zope folks made was port Java interfaces to Python.

Considering that Zope projects were both relatively early and big in Python's life time, that might answer your question. (Plus, projects not using anything like it usually either have very large test suites, or are broken more frequently than working).

Re: Why Type Systems Matter

#65

Post by rifung »

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.

Sorry if dumb question. If Haskell types don't exist at runtime how do type class functions work? I'd think the type needs to get inspected to choose the implementation to call?

Re: Why Type Systems Matter

#66

Post by dom0 »

napsterbr wrote: post #22
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…

Erlang with dialyzer is a great "mix", it allows you to move as quickly you would with a dynamic language and, as long as you define the type specs, have a reassuring type safety. Of course it's nowhere near haskell's or elms type safety because, as you said, dialyzer follows the success typing model, sort of like an optimistic one ("you are correct until I prove you otherwise"), and haskell and elm follow the opposi…

The funny thing about "moving quickly in dynamic languages" is that it doesn't last. Refactoring code in a dynamic language gets difficult fast and is an entirely hopeless endeavour without a huge test suite (you obviously need tests on every level, because you can't refactor an interface and its test at the same time and still think it's working as intended).

Typed code may be slower and more cumbersome (to some) to write in the first place, but is usually much easier to maintain in my experience.

Re: Why Type Systems Matter

#67

Post by lliamander »

wutbrodo wrote: post #34
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 fr…

I've worked in an modest Erlang codebase (~30k LOC) with a couple other people, and we used dialyzer pervasively with pretty good success. I would actually say that in some ways it was an improvement over Java's approach to types:

* there is no implicit 'null'. I.e., if your type signature doesn't explicitly include the value "none", then it's not allowed

* you have union and intersection types

* it's super easy to create new records (and types from those records)

* even if your type signature is structural, you can optionally give more meaningful names to arguments and return values in the signature itself

* success typing is still good enough to catch many "uninteresting" bugs (which I consider to be a significant advantage of static typing. When I fix bugs, I want it to be bugs with my understanding of the requirements, not bugs with my understanding about the values returned/expected by a function)

pattern matching also helps clarify the expected values of a function.

Re: Why Type Systems Matter

#68

Post by dvlsg »

zaphar wrote: post #57
falcolas wrote: post #33

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.

7 years after I first learned to love type systems and the honeymoon hasn't worn off. They definitely have some tradeoffs. Depending on the type system sometimes something I think should be expressible in a particular way isn't and I have to do it differently. There is some extra cognitive load forced on me when reading the code. But the upside is huge. Refactoring is easier and safer. The production launch of the ap…

I think recognizing that there are tradeoffs is the best way to get me to consider your stance. It says you've used it long enough to be honest about its flaws. Anything else just feels disingenuous to me.

I totally agree with you, though. The ease of refactoring alone is a big enough win to get me on board.

Re: Why Type Systems Matter

#69

Post by tmstieff »

mcphage wrote: post #56
shock wrote: post #51

Earlier quoted context omitted.

What do you mean it has a verbose type system?

Person myPerson = new Person("My", "Name") You need to specify the class twice on the same line, because Java can't figure it out on its own.

The left hand side only reserves the memory, the right hand side actually initializes the object. A bit redundant I agree, but to the compiler it is two atomic operations.

Re: Why Type Systems Matter

#70

Post by lliamander »

dom0 wrote: post #66
napsterbr wrote: post #22

Earlier quoted context omitted.

Erlang with dialyzer is a great "mix", it allows you to move as quickly you would with a dynamic language and, as long as you define the type specs, have a reassuring type safety. Of course it's nowhere near haskell's or elms type safety because, as you said, dialyzer follows the success typing model, sort of like an optimistic one ("you are correct until I prove you otherwise"), and haskell and elm follow the opposi…

The funny thing about "moving quickly in dynamic languages" is that it doesn't last. Refactoring code in a dynamic language gets difficult fast and is an entirely hopeless endeavour without a huge test suite (you obviously need tests on every level, because you can't refactor an interface and its test at the same time and still think it's working as intended). Typed code may be slower and more cumbersome (to some) to…

I find that anything beyond a very small program is faster to do with sort of manifest typing (with static analysis/type checking).

Now, I think that type inference for local variables can be nice (especially if you have good IDE that allows you to see the inferred type).

I once wrote a 600-700 line application in PowerShell. I found myself adding a few type annotations, and I expect that a program any bigger than that (especially if more than one person started working on it) would benefit from a policy of always adding type annotations.

Post reply on HN