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

The Anti-Human Consequences of Static Typing

jeapostrophe.github.io

Post reply on HN
Print view View original

51–60 of 67 posts

Re: The Anti-Human Consequences of Static Typing

#51

Post by pdonis »

acomar wrote: post #29
pdonis wrote: post #24

Earlier quoted context omitted.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

Except most type systems can deal with that -- if you truly believe that mixing types isn't foolish in a particular case, just tell the compiler that you're doing it intentionally. The OP's example is trivially solved by using the Either type within the if statement to denote that the expression intentionally returns two different types. The compiler will then check for you that you actually deal with both cases. Bet…

a type system of sufficient power can express your program just fine so long as you declare to the type checker that you're not just making a silly mistake

Sure, if I know in advance what types I want to mix. But suppose I don't? Or suppose I start out with one type mix, and then discover I need to change it? With static typing, I have to do a custom type declaration for each mix, and keep it up to date.

Re: The Anti-Human Consequences of Static Typing

#52

Post by pdonis »

glennsl wrote: post #30
pdonis wrote: post #24

Earlier quoted context omitted.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

Statically typed mainstream languages would not allow you to do that, but languages with algebraic type systems, like Haskell, Scala and Rust, do. This is also how they get around not having null pointers. You just define a type that can be either a string, or the symbol "None". Or any other symbol that might be more fitting for the situation.

You just define a type that can be either a string, or the symbol "None"

And as long as I know in advance that that's the type mix I want, and as long as it never changes, that works. But one doesn't always know in advance, and the type spec you need often changes.

Also, the example I gave was easy because the mix was between built-in types. What about if I want to mix custom-defined type A from package P1, custom-defined type B from package P2, and custom-defined type C from package P3? And suppose I have a number of different such mixes needed for different places in my program?

If all of the types I'm mixing are duck-type compatible, Python lets me just mix them, no further action required. With static typing, I need to declare a new mixed type for each mix, and keep each declaration up to date. That looks like a programming and maintenance nightmare to me for a non-trivial program. But of course it depends on what kind of programming you are doing; there are probably plenty of applications where this kind of issue wouldn't arise.

Re: The Anti-Human Consequences of Static Typing

#53

Post by pdonis »

pogden wrote: post #28
pdonis wrote: post #24

Earlier quoted context omitted.

Static typing stopped the compile because the program does something foolish. But static typing would also stop the compile in situations where mixing types was not foolish. Static typing says you must give a definite type to every variable and every expression; but that's not always the best way to write your program. (To take a simple example from Python, there are plenty of cases where you want a function to retur…

But most statically typed languages let you represent that kind of code. C++ and Java have null. Haskell has Maybe. It doesn't prevent you from writing the code, but rather requires you to be explicit about what values a variable can take, which is the purpose of having a type system at all.

It doesn't prevent you from writing the code, but rather requires you to be explicit about what values a variable can take, which is the purpose of having a type system at all.

It's the purpose of having a static type system, yes. But the drawback is that you have to be explicit; you don't have a choice. There are situations where that is indeed a drawback; see my other posts in this thread.

Re: The Anti-Human Consequences of Static Typing

#54

Post by mahyarm »

bitwize wrote: post #46

Static typing is pro-human; I would call it even more humane than dynamic typing. Vastly more type errors (i.e., conditions which cause the program not to hold the property checked by the type system) are caused by programmer error than by deliberate design; a strong, static type system, checked at compile time, helps ensure that a whole class of relatively weak but trivially easy to write bugs do not find their way…

I mostly agree, but having the ability to use a dynamic type occasionally can be very useful. I like how objective-c handles it in practice.

Re: The Anti-Human Consequences of Static Typing

#55

Post by strager »

Kliment wrote: post #13

Are there any languages that have a type mismatch warning rather than a type mismatch error? Something like how gcc warns about incompatible pointer types when compiling C programs, but lets you use them if you insist, but for all types?

GHC (a Haskell compiler) can defer type errors until runtime:

http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime

http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/defer...

Re: The Anti-Human Consequences of Static Typing

#56

Post by jeapostrophe »

freyrs3 wrote: post #42
jeapostrophe wrote: post #39

Earlier quoted context omitted.

If you really believe this, you should try to translate any contemporary (published) mathematical proof into a real logic, like Coq. It is hard and people earn PhDs doing this because most proofs are so intuition heavy in the first place.

I have spent several months doing proofs in Coq, as well as in Isabelle. I contest conflating Coq with "real logic", it is perfectly possible to do rigorous proofs without the aid of a computer-aided proof assistant, if that wasn't the case then there wouldn't be any reason to trust the authors of the proof assistant in the first place.

Certainly, but most math proofs aren't "rigorous proofs" by any stretch.

Re: The Anti-Human Consequences of Static Typing

#57

Post by jeapostrophe »

dragonwriter wrote: post #49
Permit wrote: post #20

>The logic goes that if you reject "bad" programs then only "good" programs remain, and who would want to run "bad" programs anyways? I thought the logic was: if you reject all bad programs and some good programs, only good programs remain, is it not?

I think the logic actually goes "if you reject upfront all programs with a certain type of badness as well as some programs that falsely appear to have that type of badness, you will reduce the costs associated with bad programs by catching many of them sooner, at the cost of having to rewrite some already-good programs in less-simple ways to avoid the appearance of badness."

Let's put that on a bumper sticker :)

Re: The Anti-Human Consequences of Static Typing

#58

Post by acomar »

pdonis wrote: post #51
acomar wrote: post #29

Earlier quoted context omitted.

Except most type systems can deal with that -- if you truly believe that mixing types isn't foolish in a particular case, just tell the compiler that you're doing it intentionally. The OP's example is trivially solved by using the Either type within the if statement to denote that the expression intentionally returns two different types. The compiler will then check for you that you actually deal with both cases. Bet…

a type system of sufficient power can express your program just fine so long as you declare to the type checker that you're not just making a silly mistake Sure, if I know in advance what types I want to mix. But suppose I don't? Or suppose I start out with one type mix, and then discover I need to change it? With static typing, I have to do a custom type declaration for each mix, and keep it up to date.

Your intentions changed, so of course you need to communicate that. In real programs (like the Haskell compiler), the programmers simply make the change they'd like to make at one point. The compiler then spits out a list of issues the change caused and provides a possible fix for each one. They continue the dialogue with the compiler by making the suggested fix, or by making one of their own devising. The end result is a program that's free of entire classes of stupid bugs.

Also, if you're just changing type mixtures, you probably just need to make the type more polymorphic. You rarely need to be very specific, and good type inference systems will automatically infer the most general type possible.

Re: The Anti-Human Consequences of Static Typing

#59

Post by acomar »

pdonis wrote: post #52
glennsl wrote: post #30

Earlier quoted context omitted.

Statically typed mainstream languages would not allow you to do that, but languages with algebraic type systems, like Haskell, Scala and Rust, do. This is also how they get around not having null pointers. You just define a type that can be either a string, or the symbol "None". Or any other symbol that might be more fitting for the situation.

You just define a type that can be either a string, or the symbol "None" And as long as I know in advance that that's the type mix I want, and as long as it never changes, that works. But one doesn't always know in advance, and the type spec you need often changes. Also, the example I gave was easy because the mix was between built-in types. What about if I want to mix custom-defined type A from package P1, custom-de…

> With static typing, I need to declare a new mixed type for each mix, and keep each declaration up to date. That looks like a programming and maintenance nightmare to me for a non-trivial program.

Sounds like you're thinking of Java/C# level type systems here. Type inference is a powerful feature that allows you to just not specify types (except where the program is ambiguous) in most cases.

Re: The Anti-Human Consequences of Static Typing

#60

Post by pdonis »

acomar wrote: post #58
pdonis wrote: post #51

Earlier quoted context omitted.

a type system of sufficient power can express your program just fine so long as you declare to the type checker that you're not just making a silly mistake Sure, if I know in advance what types I want to mix. But suppose I don't? Or suppose I start out with one type mix, and then discover I need to change it? With static typing, I have to do a custom type declaration for each mix, and keep it up to date.

Your intentions changed, so of course you need to communicate that. In real programs (like the Haskell compiler), the programmers simply make the change they'd like to make at one point. The compiler then spits out a list of issues the change caused and provides a possible fix for each one. They continue the dialogue with the compiler by making the suggested fix, or by making one of their own devising. The end result…

Your intentions changed, so of course you need to communicate that.

But in a dynamically typed language, I don't have to communicate anything; it all happens automatically.

The end result is a program that's free of entire classes of stupid bugs.

A good test suite achieves the same objective with a dynamically typed language. There are tradeoffs both ways; I'm not saying dynamic typing is always better. But I don't think static typing is always better either.

good type inference systems will automatically infer the most general type possible.

With dynamic typing, no inference is necessary at all.

Post reply on HN