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

21–30 of 103 posts

Re: Why Type Systems Matter

#21

Post by MrRadar »

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…

Check out D (https://dlang.org/). It has a reasonably powerful static type system and the dmd compiler is lighting fast.

Re: Why Type Systems Matter

#22

Post by napsterbr »

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 opposite way ("you are wrong until you prove me otherwise ").

It's a tradeoff, as everything else in computer science, and one that has worked for us. Can't recommend both erlang and dialyzer enough :)

Re: Why Type Systems Matter

#23

Post by Veedrac »

naasking wrote: post #12
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…

> 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. Finding the right type is solving most of the problem. If you can find the right type, you can solve the problem. If you're having trouble finding the right type, then…

> If you can find the right type, you can solve the problem.

Do you actually believe this?

Re: Why Type Systems Matter

#24

Post by kmill »

naasking wrote: post #12
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…

> 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. Finding the right type is solving most of the problem. If you can find the right type, you can solve the problem. If you're having trouble finding the right type, then…

> 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 have you. Even the general mathematician doesn't start by drawing the right diagram. (Though some do.) For me, "the right type" comes from abstracting partial solutions.

I think part of it is preference for certain thinking styles, like how some people like puzzles based on group theory and some on topology. If finding the right types ahead of time works for you, great! But don't be surprised that people manage to solve problems by other means.

(It could also be that the type systems in programming languages don't capture the intuitive types[1], and perhaps rocky1138 keeps them in his head while prototyping. Just because the types aren't written down doesn't mean they aren't there --- i.e., there is no need to obsess over making things real. But, it is nice to make them real so you don't have to keep them in your head anymore, or to communicate them to others more effectively.)

[1] I sort of mean intuitive in the sense of intuitionism.

Re: Why Type Systems Matter

#25

Post by jerf »

zem wrote: post #20
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…

that's one of the things go got right - they had fast compilation speed as a first-class goal right from the beginning.

They also have a really, really simple type system that can't play very many of the games that type system experts would like to play, so it doesn't cost them a lot of runtime at compile time.

I'm sort of curious what the abstract minimum penalty is for the very advanced type systems. Are GHC (Haskell) and rustc already within, say, 5x of the optimal possible speed, or might we be able to have a very advanced type system and faster compiling? Time shall tell, I suppose.

Re: Why Type Systems Matter

#26

Post by gertef »

willtim wrote: post #4
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…

There's no reason why static type errors can't be deferred until runtime, GHC Haskell can do this. Personally I find types invaluable when prototyping. I often fill in the implementations after I work out the types.

> I often fill in the implementations after I work out the types.

OK, but that's the opposite of deffering type errors until runtime.

Using "undefined"/bottom as the implemenation of a function is how we wrote Haskell before GHC added support for deferring type-errors.

Re: Why Type Systems Matter

#27

Post by zsd »

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…

Success typing really seems both ideal for me and the only sane way to do optional, progressive typing. I wonder if Ruby could do it? I think there are too many ways for an expression to be invoked from friggin anywhere in Ruby to make that possible.

Re: Why Type Systems Matter

#28

Post by thanatropism »

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…

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)".

Re: Why Type Systems Matter

#29

Post by jerf »

Veedrac wrote: post #23
naasking wrote: post #12

Earlier quoted context omitted.

> 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. Finding the right type is solving most of the problem. If you can find the right type, you can solve the problem. If you're having trouble finding the right type, then…

> If you can find the right type, you can solve the problem. Do you actually believe this?

What's the most advanced type system you've used?

It's quite difficult to explain how much work a very strong type system can do for you if you're used to something like C as your definition of "static typing". I mean this comment comment completely straight and polite, and I'm trying to help people answer your very reasonable question by asking you for some details that will help calibrate the answer.

Re: Why Type Systems Matter

#30

Post by mahyarm »

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…

I would prefer mandatory typing with a dev mode that makes it optional for speed. With optional typing, you end up with the third party ecosystem not having typing, which makes it hard to enforce type safety with a codebase that is fully type safe itself.
Post reply on HN