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

Static Typing is not enough

blog.fogus.me

Post reply on HN
Print view View original

51–60 of 65 posts

Re: Static Typing is not enough

#51

Post by stonemetal »

nightski wrote: post #36

Doesn't anyone view static typing as done in a language like Haskell as a form of documentation? I am not saying ALL Haskell code can be deciphered by its types - hell no. But a useful technique is to express the semantics of the program into the type system (as much as possible anyways) to communicate intent. This is a huge benefit over dynamic languages imho. So there is more too it than just verification, even if…

In some way yes, but in general not really.

(+),(-), (*) all have the type (Num a) a -> a -> a

abs, signum both have the type (Num a) a-> a

In the first case it works as documentation because I already know what they do. In the second case I read signum as sig num instead of sign num, and was left scratching my head as to what a signature number was, until I read the actual documentation.

So I would say types make a good reference documentation but not a good learning documentation. Contrast this with python doc strings which can be both a good reference and a decent source of learning.

Re: Static Typing is not enough

#52

Post by skew »

lmm wrote: post #47
ternaryoperator wrote: post #7

Kind of a strawman argument, as no developer would argue that only unit tests and static typing are needed to guarantee quality.

It's a response to a previous article, which really did make the argument "unit testing does not guarantee quality, therefore you need static typing". So not a strawman.

The previous article really didn't make the argument "all you need is static typing". It was specifically refuting the idea that "all you need is unit testing" - or at least that unit testing is a complete replacement for static types.

The paper makes a point of reporting that most unit tests could not be replaced by static types.

What of that looks like a claim that you only need types?

Re: Static Typing is not enough

#53

Post by banister »

carsongross wrote: post #23
jshen wrote: post #18

Earlier quoted context omitted.

Pry for ruby gives me great dot completion and isn't batshit insane. Most diehard dynamic typists live in their repl. When I use java with IntelliJ I miss my repl. I do gain some things from the IDE, but I feel hamstrung compared to my repl.

Ah, f k man, another REPL? I don't want a repl for editing. I want to write code in a friggen editor and have dot completion work. I also want a repl for trying stuff out and debugging/light weight testing, but that's a different use case for me.

Pry knows its place, it doesn't pretend its a nice environment for writing real code - instead when you want to edit a method definition you type "edit-method my_method"[1] and pry will open the source file of that method in an editor and take you to the exact line where the method is found.

[1] https://github.com/pry/pry/wiki/Editor-integration

Re: Static Typing is not enough

#54

Post by gtani »

nightski wrote: post #36

Doesn't anyone view static typing as done in a language like Haskell as a form of documentation? I am not saying ALL Haskell code can be deciphered by its types - hell no. But a useful technique is to express the semantics of the program into the type system (as much as possible anyways) to communicate intent. This is a huge benefit over dynamic languages imho. So there is more too it than just verification, even if…

GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types:

http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier...

http://www.haskell.org/haskellwiki/Phantom_type

http://stackoverflow.com/questions/8600692/datatype-promotio...

For scala:

http://groups.google.com/group/scala-internals/browse_frm/th...

http://www.chuusai.com/2012/01/27/type-level-sorting-in-shap...

-------------

SAT and SMT solvers, e.g. in OCaml

http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706

-----------------

I could give a few dozen more examples in these 3 languages, incluindg Coq which is written in C and OCaml, and agda and idris and others, which are written in C and haskell, or compile down to some stage of haskell compilation.

Re: Static Typing is not enough

#55

Post by jules »

tomp wrote: post #4

Sometimes, I wish I could downvote stories... Accidentially, almost everything that the author suggests, except luck and user testing, can be provided by static type systems - e.g. Haskell's type system is Turing-complete, so you can make up any kind of contracts/tests and embed them into the type system...

Incorrect. Haskell's type system cannot ensure arbitrary correctness guarantees. Hence the research into dependently typed languages, like Agda and Coq.

Re: Static Typing is not enough

#56

Post by jules »

prodigal_erik wrote: post #24
derefr wrote: post #13

Earlier quoted context omitted.

> dot-completion involves static analysis of the code. Dot-completion involves having a living model of the program loaded in memory . You can do this with any language--static languages just partition the program model such that you get a certain phase of interpretation (compilation) past which you have a completed model of all of the code , without yet having seen any of the data . On the other hand, you can easily…

When you create a method which takes an argument in a dynamic language, there's no declaration of the type of that argument or which methods it will be known to support. So how does dot-completion work for any target other than "this"? The REPL isn't doing whole-program dataflow analysis to infer the only type(s) which could possibly be passed, is it?

FYI, PyTools for Visual Studio does dataflow analysis for intellisense.

Re: Static Typing is not enough

#57

Post by morsch »

gbog wrote: post #11

In a conference 15 years ago I heard a guy say The problem with software is we don't know what it is. He meant that: we know what is a car or a bridge, we know why and how they do their purpose, not so much with software, which is a strange beast our minds are not ready to grab yet.

There might be something to that. But maybe some construction and automobile engineers feel the same way about bridges and cars respectively. God, I hope not. :)

Re: Static Typing is not enough

#59

Post by fogus »

soc88 wrote: post #45
modarts wrote: post #10

Yet another attempt to diminish the value of statically typed languages and the benefits that go along with them.

Yes, exactly. The author didn't like the original article and decided to throw around some strawmen.

I disliked it so much that I called it "excellent".

Re: Static Typing is not enough

#60

Post by ajanuary »

skew wrote: post #52
lmm wrote: post #47

Earlier quoted context omitted.

It's a response to a previous article, which really did make the argument "unit testing does not guarantee quality, therefore you need static typing". So not a strawman.

The previous article really didn't make the argument "all you need is static typing". It was specifically refuting the idea that "all you need is unit testing" - or at least that unit testing is a complete replacement for static types. The paper makes a point of reporting that most unit tests could not be replaced by static types. What of that looks like a claim that you only need types?

The previous article said "unit testing isn't enough, you need static types /as well/". This article is extending that argument to "unit testing and static types aren't enough, you need xyz /as well/".

I believe the point is that there will always be something your current test strategy doesn't cover. At what point do you draw the line?

If unit tests and static types don't cover everything, what says that's enough? And can the justification for that, whatever it is, be applied to "unit tests are enough" also?

Post reply on HN