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

Evolutionary couplings between files reveal poor software design choices

ergoso.me

Post reply on HN
Print view View original

71–80 of 85 posts

Re: Evolutionary couplings between files reveal poor software design choices

#71

Post by pfortuny »

rwallace wrote: post #68
evincarofautumn wrote: post #66

Earlier quoted context omitted.

I have found that the best papers are hard to read because they’re informationally dense, so you have to slow down to really process every sentence and unpack the author’s thinking in your head—but once you do, you get a lot of knowledge from just a few pages. So it ends up being worthwhile. Average papers are hard to read because they’re trying to emulate the style of the good papers, but without having enough actua…

True, but it is also true that the best papers would be even better if they were written in less terse and cryptic style so that the same information could be obtained more easily.

There is an editorial problem with that (which nowadays, with electronic publishing should not be an issue): space is (used to be) a scant resource. Hence density of content was more important than clarity of exposition.

Nowadays I guess everything boils down to a custom of which we (yes, I am part of the problem) have not been weaned. It looks more scientific to write things densely and more or less cryptically.

Also, we scientists are a bit afraid of publicly (I mean, to the general public) explaining our way of understanding things, because we know it is somewhat blurry, informal, possibly even comical to a lot of people. And we tend to be introverts.

I guess things like arxiv.org etc. are going to create a new way of explaining scientific discoveries much more interesting and enlightening.

Re: Evolutionary couplings between files reveal poor software design choices

#72

Post by buss »

paulsutter wrote: post #63

> I was thinking about writing up a small application paper for this project, but I am really terrible at reading papers from the Computer Science field, let alone writing them. Thank goodness for that. This blog post was so much easier to read then a formal paper. Why are formal papers so tedious to read? Imagine how much time we'd waste as a group if he written this as a paper. Many of us would give up before findi…

> Why are formal papers so tedious to read? Imagine how much time we'd waste as a group if he written this as a paper.

This is a huge problem in the academic field. Papers are written in academese, not because it's a particularly good way of distributing information, but because it's expected. I absolutely agree that less formal language is both good for the discipline, the technical non-academic audience, and for the lay audience.

Steven Pinker recently wrote a book called "The Sense of Style" which talks about academese and writing well about complex subjects (something which he, indeed, has a lot of experience in!). I haven't read it yet, but I've heard it's quite good.

Re: Evolutionary couplings between files reveal poor software design choices

#73

Post by rwallace »

evincarofautumn wrote: post #70
rwallace wrote: post #68

Earlier quoted context omitted.

True, but it is also true that the best papers would be even better if they were written in less terse and cryptic style so that the same information could be obtained more easily.

I’m not sure about that. For example, the first time I read them, each of these statements in the declarative specification of Hindley–Milner type inference took me a long time to unpack. x : σ ∈ Γ --------- [Var] Γ ⊢ x : σ Γ ⊢ e₀ : τ → τ′ Γ ⊢ e₁ : τ --------------------------- [App] Γ ⊢ e₀ e₁ : τ′ Γ, x : τ ⊢ e : τ′ ------------------ [Abs] Γ ⊢ λx. e : τ → τ′ Γ ⊢ e₀ : σ Γ, x : σ ⊢ e₁ : τ -----------------------------…

Ah, serendipity! As it happens I'm working on a variant of HM type inference right now, so my first step was to look up the explanation on Wikipedia and have my eyes glaze over. (As the saying goes, 'Which part of [above equations] do you not understand?' Answer: all of it! And it's not even the first time I've looked at it, though I don't remember anything much from the previous time.)

So I rummaged around a bit more and found http://akgupta.ca/blog/2013/05/14/so-you-still-dont-understa... which explains the notation in much more readable English text. It's a pure win.

Yes, I find typical Java style too verbose for optimal readability; but I find typical Perl style too terse for optimal readability. The sweet spot is somewhere in the middle.

Re: Evolutionary couplings between files reveal poor software design choices

#74

Post by chongli »

vertex-four wrote: post #69
chongli wrote: post #30

Earlier quoted context omitted.

Instead of writing tests in a separate file, why not express the same logic in the form of types in the lines directly above the code which implements that logic? This has the added benefit of making your code self-documenting and giving rise to powerful tools such as type-guided implementation inference and search.

How do you write a type which fully describes, for example, "given a user, some content, and various bits of metadata, this function transforms them into a blog post with all the data in the right places"?

You don't write just one type, you write many. The problem you described is pretty straightforward. There are actually lots of examples of how to do this with existing Haskell libraries. What specifically do you want to know about?

Re: Evolutionary couplings between files reveal poor software design choices

#75

Post by vertex-four »

chongli wrote: post #74
vertex-four wrote: post #69

Earlier quoted context omitted.

How do you write a type which fully describes, for example, "given a user, some content, and various bits of metadata, this function transforms them into a blog post with all the data in the right places"?

You don't write just one type, you write many. The problem you described is pretty straightforward. There are actually lots of examples of how to do this with existing Haskell libraries. What specifically do you want to know about?

OK, let's put it this way. I have an entirely arbitrary calculation, taking input A and outputting B. I want to ensure that this calculation is implemented according to specification.

How on earth do you write a type, or set of types, for that that actually bear some resemblance to the spec and don't simply reflect the details of the implementation?

To simplify it to the point of near-nonsense, how would you write a type which says `append "foo" "bar"` will always result in "foobar", and never "barfoo" or "fboaor"? Or that a theoretical celsiusToFahrenheit always works correctly and implements the correct calculation? If you can't do that, how can you do it for more complex data transforms?

Re: Evolutionary couplings between files reveal poor software design choices

#76

Post by chongli »

vertex-four wrote: post #75
chongli wrote: post #74

Earlier quoted context omitted.

You don't write just one type, you write many. The problem you described is pretty straightforward. There are actually lots of examples of how to do this with existing Haskell libraries. What specifically do you want to know about?

OK, let's put it this way. I have an entirely arbitrary calculation, taking input A and outputting B. I want to ensure that this calculation is implemented according to specification. How on earth do you write a type, or set of types, for that that actually bear some resemblance to the spec and don't simply reflect the details of the implementation? To simplify it to the point of near-nonsense, how would you write a…

This is where dependent types come in. They allow you to write an implementation of append that is correct by construction. Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`.

A simpler example is that of lists and the head operation. In most languages, if you try to take the head of an empty list you get a runtime exception. In a language with dependent types you are able to express the length of the list in its type and thus it becomes a type error (caught at compile time) to take the head of an empty list.

Re: Evolutionary couplings between files reveal poor software design choices

#77

Post by vertex-four »

chongli wrote: post #76
vertex-four wrote: post #75

Earlier quoted context omitted.

OK, let's put it this way. I have an entirely arbitrary calculation, taking input A and outputting B. I want to ensure that this calculation is implemented according to specification. How on earth do you write a type, or set of types, for that that actually bear some resemblance to the spec and don't simply reflect the details of the implementation? To simplify it to the point of near-nonsense, how would you write a…

This is where dependent types come in. They allow you to write an implementation of append that is correct by construction. Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`. A simpler example is that of lists and the head operation. In most languages, if you try to take the head of an empty list you get a runtime exception. In a language with dependent types you are able t…

> Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`.

Isn't that literally just implementing the program, though? The point of tests is that they're simple enough that you can't really fuck up, and they describe the specification, not the implementation.

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation?

Re: Evolutionary couplings between files reveal poor software design choices

#78

Post by emmelaich »

tracker1 wrote: post #22
dkarapetyan wrote: post #20

Hold on. I have an interface file "interface.d.ts" and a whole bunch of other files reference it. Whenever I make changes to any files that depend-on/reference that file I of course also make changes to that file. This means that every file in my project is coupled to that file. How is that indicative of good or bad design?

Tight coupling is generally considered bad practice, it leads to more accidental variance and complexity. In general adding either polymorphism, or additional methods to a class are considered safer. I'm not saying in your case it was the wrong choice, or that cleaning up design is bad. Generally if you have to change a whole bunch of related files when you change one, it's an issue with the design.

Not sure you can know that without knowing the problem domain.

There's a tension there with one-and-one-place-only otherwise known as Don't-Repeat-Yourself.

Re: Evolutionary couplings between files reveal poor software design choices

#79

Post by chongli »

vertex-four wrote: post #77
chongli wrote: post #76

Earlier quoted context omitted.

This is where dependent types come in. They allow you to write an implementation of append that is correct by construction. Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`. A simpler example is that of lists and the head operation. In most languages, if you try to take the head of an empty list you get a runtime exception. In a language with dependent types you are able t…

> Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`. Isn't that literally just implementing the program, though? The point of tests is that they're simple enough that you can't really fuck up, and they describe the specification, not the implementation. If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actu…

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation?

The formal proof is the implementation. It is the code you run in production. The proposition is your types. Instead of writing tests, you write types. It's the exact same process you would use with "red-green-refactor" TDD except it's the compiler checking your implementation instead of the test suite. The advantage of doing it with types is that the compiler can actually infer significant parts of the implementation for you! Types also happen to be a lot more water-tight than tests due to the way you specify a type for a top-level function and everything inside of the body can generally be inferred.

If you're interested, here is a series of lectures demoing dependently-typed programming in Agda by Conor McBride:

https://www.youtube.com/playlist?list=PL_shDsyy0xhKhsBUaVXTJ...

Re: Evolutionary couplings between files reveal poor software design choices

#80

Post by vertex-four »

chongli wrote: post #79
vertex-four wrote: post #77

Earlier quoted context omitted.

> Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`. Isn't that literally just implementing the program, though? The point of tests is that they're simple enough that you can't really fuck up, and they describe the specification, not the implementation. If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actu…

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation? The formal proof is the implementation. It is the code you run in production. The proposition is your types. Instead of writing tests, you write types. It's the exact same process you would use with "red-green-refactor" TDD except it's the c…

I will certainly watch those - but for the moment, I see no obvious way to immediately see that a proof is proving what you intended it to prove, whereas `assert (append "foo" "bar") == "foobar"` immediately shows what you expect and can be read and checked by somebody with the slightest programming knowledge.

The point of tests is that they're supposed to be simple enough that it should be near-impossible for them to contain bugs - they're incomplete, sure, but what they're testing should always be correct - whereas it seems that it would be easy for a proof to prove something subtly different from the spec without anybody being able to tell. If we could write complex programs to spec without error, we wouldn't have tests in the first place.

Post reply on HN