Hacker News Reader

Comment by kazinator | Hacker News Reader

> It’s hard to describe the experience of doing a major refactoring, having a really helpful and friendly compiler guide you along step by step and when finally everything compiles it just works.

A truly large refactoring is one that you want to try long before getting everything to compile.

"Hmm, I have 75 operations involving data structure A. I want it to be B. Let's try it with five operations; I know that such and such features of the program only use those. Let's build the inconsistent program and try it out with with the B structure to the extent that it is possible."

The dynamic world lets us have inconsistent code that partially works, rather than forcing us to follow up on all the places reached by the ripple effect of a change. Maybe the change turns out to be a bad idea in the end; then it was a waste of effort.

Psychologically, having to deal with a big ripple effect is discouraging; it creates an "activation potential barrier" which opposes change.

View on HN

This is why Haskell recently got a flag to turn type errors into warnings: now you came make a change, get a bunch of type errors (as warnings!) and fix them one at a time, loading and testing each part as you change it. You don't have to update everything to play around with your module.

This isn't dynamic typing though: if you tried to use an expression that did not typecheck, you will get a runtime value immediately. It's the moral equivalent of automatically replacing the broken expression with an `undefined` exception.

For anyone reading and interested in checking out the docs, the flag is -fdefer-type-errors: https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_gui...

Why don't they just add the dynamic typing when that happens. There could then be a class of Haskell programs that are statically ill-formed, yet actually free of errors.

Maybe adding dynamic typing to a thoroughbred static language could turn out more fruitful than efforts to go the other way.

> Why don't they just add the dynamic typing when that happens.

Haskell (at least, GHC Haskell) has support for dynamic typing, in three(ish) parts.

"Dynamic typing" in the sense of being able to ask the types at runtime is available in the Typeable typeclass. This is provided by the compiler automatically for known types; it must be visibly asked for for polymorphic types - partly for visibility and to preserve reasoning (https://www.reddit.com/r/haskell/comments/4mu30y/what_is_the...) and partly to clarify what dictionaries need to be passed where.

"Dynamic typing" in the sense of foregoing static checks in favor of runtime checks can, of course, usually be done in a constrained way simply by choosing looser types. That said, depending on language, that can often mean substantial boilerplate. GHC does provide Dynamic, which will wrap any value up with its type annotations and let you apply (possibly wrapped) functions to these wrapped values in a dynamically checked way.

Lastly, I'd kind of put "existential quantification" in play here. It's sometimes the case that you only need to show that some pieces of "the same type" are internally consistent, without knowing their precise shape.

As for why it's not added, I'm not 100% sure what you mean.

If you mean on every build, making that the only option, then I would say "because many of us who choose Haskell find static checks a huge help (particularly when refactoring) and wouldn't want to give that up".

If you mean in place of the current behavior of -fdefer-type-errors, I expect it's sometimes quite useful to know earlier when you're exercising magically untyped code (as compared to deliberately demarcated untyped code).

If you mean, "why don't they add -fdynamic-type-errors", an additional flag that subs in use of Dynamic in place of inconsistently typed code, that's certainly an interesting idea; given that terms are sometimes derived from types (typeclass polymorphism) it may not always be possible, and in any case may be a large engineering effort - I suspect Simon and company simply haven't gotten around to it.

I mean without any boiler plate whatsoever. Just "we can't determine what the type of some term x is, so let it be anything and check it at run time when it is used in a way that requires it to be of some specific type(s)".

That's what I had understood you to mean; what I was unsure of is whether you intended this to be the only mode of compilation - and addressed what seemed like each possibility in the second half of my post.

Sure, only mode. Inform me "this program is not known to be well-typed" or "this program is outright ill typed". Then, let me run it anyway, and correctly detect the consequence of the admonition with run-time info. Or I could choose not to run that program; I want mine well-typed.

In the presence of -Werror, this seems isomorphic to the notion of adding a '-fdynamic-type-errors' flag.

It can't be done in full generality because, as I mentioned, there are places where term-level values depend on types. If we don't know what type, we can't know what term.

We could certainly treat only those situations where behavior is ambiguous like '-fdefer-type-errors' currently treats any type mismatch, and add dynamic checks for the rest. It would be an interesting point in the space, though not one I would expect to use very often.

That's very, very nice. Is this exclusive to Haskell?

Well, Haskell got it from Agda [1], but Agda is even farther in the direction of Haskell than Haskell relative to mainstream programming languages, and beyond the "currently practical" language horizon.

[1]: https://wiki.haskell.org/GHC/Typed_holes

Typed holes are quite a different thing than deferred type errors. Does Agda actually have something like the latter? (Results seem negative from the tiny bit of searching I've just done, but that's awfully low confidence...)

Whoops, you're right! I was too hasty.

Eclipse does a similar thing with Java. It will replace methods that don't compile with a stub that throws an exception with the compilation error.

But is that transparent or they pollute the source code?

It's completely transparent, done only in the compiled class files. The signature of the method remains exactly the same, just the body is replaced.

> The dynamic world lets us have inconsistent code that partially works

This is precisely why I have nightmares about refactoring dynamic codebases.

If it's tested, you shouldn't.

Unit tests are essential, but they only cover the errors that the person writing the tests thought to write. Given that even the highest coverage code I've ever worked on could still be riddled with bugs, I submit that us humans can be pretty bad at thinking of all the tests we should write.

Static typing, by contrast, covers all type errors, which can take care of quite a bit if you know how to use the type system to your advantage. On top of that, if you don't rely on a refactoring tool (which I recommend avoiding for anything non-trivial) then the compiler will guide you to all the spots where that type is being used, which gives you an opportunity to re-evaluate the correctness of the code that uses it.

Is it more work? Yes. Is that a bad thing? Many would argue it's a good thing.

I get the benefit of static typing, my above comment was directed at the suggestion that refactoring dynamic code is something to be afraid of. You commonly hear this from people who primarily use static languages.

I personally don't feel that the benefits outweigh the cost; namely that I have to babysit a compiler and stop development while I fix compiler errors that are irrelevant to the thing I'm working (if I'm working on widget A and I broke widget B by changing a type, I don't want to fix widget B right now).

There might be another cultural difference there: I've never worked in a place that used a dynamic language for the majority of the code base, but from what you're saying it sounds like simultaneously refactoring and adding features is something you'd consider to be a normal task. I'm used to that being considered a big no-no, because it makes code reviews and source control history harder to understand.

You can can work on several things at once in your local repo and use "git commit --patch" to separate changes. Of course you never want unrelated changes (different "topics") in the same commit.

If a feature is better implemented after a certain refactoring, then you can do that at the same time locally but still separate it out into different commits.

Exactly this, in any language!

Generally I like refactoring. Essentially, it is the process of taking disjoint, complicated code and making simpler and logically consistent. I have never really though of refactoring as something to fear until I'd spent time working in a Node shop.

You don't want to stop and fix "unrelated" errors, but if B was broken by a type change in A then it is almost certain that B is affected by the changes in A. Right now, when you are making the changes in A, is the best time to address the fallout, because you have the reason for the change and all its subtleties in mind.

The vast majority of the bugs my team addressed after our last major refactor in our Node codebase were of this kind: either completely forgotten or unknown components affected, or fixes that were not fully aware of the changes made. Knowing at the time of the change all of the places that change affects is extremely powerful. Tests only get you this for the easy cases you've thought of. Static typing doesn't get you that entirely, but it gets you a lot closer than dynamic typing.

So I'd argue the opposite. Dynamic languages taught me to fear refactoring because they're is always the danger that you missed something buried somewhere that will come back to bite you in really subtle ways. I never get the satisfying feeling of unifying the code under a new logical consistency because there may still be these loose ends lurking around.

Survivor bias. Only a special breed of developer gets a job working in a functional language, except for JavaScript.

Normal Devs write mediocre tests on a good day. You will find a significant percent that assert nothing or are tautological. Then when your requirements change or you are refactoring you will find that we have tested the implementation and made really unfortunate assumptions.

If you invite everyone to join you, a lot of the things you hold dear will get lost. It's super frustrating to have to trust people who can't be.

I worked with static languages for a long time, and I have been doing test automation for a long time (10 years). There are many things I understand about writing good tests, many of them counterintuitive things, including some big mistakes everyone seems to have to experience to believe.

I can't articulate it yet, I'm still processing, but recently some of the classes of error I'm finding in my and other's tests have convinced me that tests can't practically and efficiently verify everything important, and that maybe testing in this way and to this extent isn't the solution we need.

Often what makes a good test is contrary to how we write production code. Testing well is pretty damned hard for people. And I now despair of ever convincing the hoi polloi not to eagerly paint us into corners.

I'm very curious to hear more of your thoughts on this. Might they ever show up on a blog at some point in the future?

I love compiler errors - because I'm the only one who sees them.

I prefer automatic tool followed by VCS "diff against head" myself. I get to replace a bunch of error prone typing with a small code review.

Luckily, my compiler writes large piles of tests for me. I call it the typechecker.

These tests only cover the type space, which is trivial. And doesn't vary at run time. Even under dynamic typing, it's by large immutable: short of special tricks like change-class in Common Lisp, objects are immutable, and most data flow paths carry the same types all the time.

For instance, consider a function which calculates the GCD of two integers. Everything in that function is an integer. Your compiler tests it for you: nope, no strings or floats in there: nothing but integers, check!

It's basically one test, and it has nothing to do with whether that function calculates the GCD correctly. It will pass even if that function calculates the LCM due to misunderstood requirements.

There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d.

[0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...

This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.

For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.

For all I know

Agreed.

> These tests only cover the type space, which is trivial.

Granted it's not enormous, but if you think it's trivial you'll probably be surprised by the range of things you can encode in the Haskell type system.

That encoding requires you to be a type system expert, and write reams of additional code surrounding the actual code. That additional code has to be well thought out and designed; proofs don't just pop out of thin air, all ready to go and represented as type via Curry-Howard!

Ordinary code does not encode very interesting things about itself via its typing. Well typed usually just means "there is no trivial mistake here", on about the same level as a missing semicolon in a C struct declaration.

That's just not true.

I have some interest in types (mostly practical, some theoretical) but I have no graduate degree, I still regularly encounter both theory and type voodoo I don't understand, and I wouldn't consider myself a "type system expert".

On a recent project I was able to use the type checker to help me catch things including 1) passing a bid price where I meant an ask price, 2) using an index into the wrong array, 3) calling a function not permitted to run on the thread in question (because of data access or deliberate marking).

This wasn't Haskell - it was C.

Testing shows the presence, not the absence of bugs. Dijkstra (1969).

Same can be said of static type checking so what is your point? Are you suggesting that those working in static languages don't need to write tests?

Static type checking generally represents an even lower form of error detection than functional and unit testing does. Sure, it can be convenient to have it, but lately I see a lot of static language novices around here talking about their recent and limited experience with type checking as if they are suddenly experts in the tradeoffs between static and dynamic languages.

But, as you surely know, types prove something about a piece of code. This means they can very well prove the absence of (certain) bugs.

So generally, the more invariants you manage to capture in your types, the more categories of bugs you can statically prove will never happen.

This is all true, but is it not a problem that most static languages don't let you (easily) specify the kind of invariants people include in unit-tests.

Sure. But you write unit tests for those.

> Same can be said of static type checking so what is your point?

That isn't true. Static typing offers machine checked proofs of the absence of a whole class of trivial errors; and potentially any invariants you've managed to teach it.

My point was that testing does not negate the need for static types, as implied by the previous poster.

Although "class" sounds big, in fact there is only a countable number of places (nodes in the program's tree) where you can have a type error. The space in which any error whatsoever can occur is astronomical.

Let me give an analogy:

Claim: "Getting vaccinated stops a whole class of diseases which might kill you"

Your rebuttal: Although "class" sounds big, in fact there are only a countable number of viruses that vaccines save you from. The number of ways in which you can die is astronomical.

In the above analogy, as in your original statement, you're completely missing the point that the class of errors / class of diseases is an important class and easily preventable, therefore you should do it.

In fact, I think what you've said is the reverse of true. Static typing means that there's a chance of an error at each node in the program's tree because a statically typed and statically compiled language ensures that the program can be rendered as an AST before you ship it to your user.

A dynamically typed interpreted language can have an error at literally any character in the entire thing, and you don't have "compile-time" to tell you it's not an error.

The class of errors that you're saving yourself from is "every single character of this program could be wrong in a way that results in it not even being representable as an AST; there are astronomically many ways that can occur".

In addition, it now goes wrong much later. You have to ensure that you've hit every path with testing before you can be even somewhat confident it's valid code, let alone logically correct and bug-free in other ways. A compiled statically-typed language you waste no more time than a compile-cycle to get that minimal assurance.

Let me give an analogy:

Claim: "Using a plastic liner stops urine from getting into the mattress".

My rebuttal: "That's well and good, but I'm sure I didn't wet my bed past the age of three."

But then you find yourself sharing a bed with an infant.

Source: I'm typing this from a bed I'm sharing with an infant.

(I don't actually mean this to be an argument, just fun. "Other people will make type errors" is not the argument I'd make.)

"Compiled" and "dynamically typed" are not opposites.

It seems like the reasoning here is exactly the wrong way round.

The number of possible programs is astronomical (though still countable!). The number of possible programs with the correct type is substantially smaller. If we can construct our types and type checking such that the errors we are likely to make are likely to result in ill-typed programs, then we can substantially reduce the number of uncaught errors.

More generally, in your comparison you seem to be expecting that a unique error be detected in a unique place. There is no particular reason multiple (or manifold) errors should not be expected to produce an error in the same "nodes in the program's tree".

I'm looking at it as a search problem. I don't care about the likelihood of a randomly generated program with correct syntax being correctly typed because people don't program that way. But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course). If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs.

> I don't care about the likelihood of a randomly generated program with correct syntax being correctly typed because people don't program that way.

Agreed!

> But rather this: let's take a correct program of size N (N nodes in the syntax tree) and insert a single error into it and give the modified program to someone to find the error (without giving them the original, of course).

I think that's a good approximation. There is some additional structure it discards; I care most about errors that people are likely to make, and about surfacing changes required in likely refactoring. But I expect something that does well at the one is likely to do well enough at the other.

> If it's a type error, it can be found by searching the space of N nodes. If it can be any defect whatsoever, the search space is the entire state space of the program emanating from all combinations of all possible inputs.

Which is exactly why we want to make as many errors "type errors" as possible (modulo tradeoffs). We'd much, much rather search that smaller space.

> Are you suggesting that those working in static languages don't need to write tests?

You certainly don't need to write tests that Math.floor will return NaN when you pass it something that's not a number...

What? NaN is actually a number in the sense of being in the domain of the floating-point type. You seem to be mixing up "not a number" (as in character string or list) versus "not a number" as in a special IEEE representation that has special uses in numeric code.

A floor function that returns NaN when given a string, instead of throwing a type mismatch exception, is crap design, and a strawman example of that type of checking. It's not an appropriate use of NaN!

I agree with you [0], but that's what JavaScript gives us to work with.

[0] https://news.ycombinator.com/item?id=11898046

When my typechecker writes most of my tests for me, I have time to write features.

If so, I'd say you were writing the wrong kinds of tests before. I work in JavaScript and almost never write type verification tests.

Types in JavaScript aren't very expressive. When you encode your business logic in the type system, even business logic can be "tested" via the type checker.

> A truly large refactoring is one that you want to try long before getting everything to compile.

So I thought this for a good long while - and then I started coding in Rust on a major project. Turns out that once I'd written my serialization/deserialization functions on the boundaries of my program, it's remarkably difficult to get the rest of my code to compile and not do what I was intending it to do.

It's not magic - the compiler doesn't guess at what I want - but it's close enough that I'm comfortable making larger changes than with Python.

I've had the same feeling. I have often though to myself "I do not know how to break this code. Even if I purposely tried to get this code to throw a run time error, I could not."

> A truly large refactoring is one that you want to try long before getting everything to compile.

That's a luxury that may not be available :-)

Here's a case study of industrial use of a refactoring tool provided with a dynamically typed language:

…

"A very large Smalltalk application was developed at Cargill to support the operation of grain elevators and the associated commodity trading activities. The Smalltalk client application has 385 windows and over 5,000 classes. About 2,000 classes in this application interacted with an early (circa 1993) data access framework. The framework dynamically performed a mapping of object attributes to data table columns.

…

Analysis showed that although dynamic look up consumed 40% of the client execution time, it was unnecessary.

…

A new data layer interface was developed that required the business class to provide the object attribute to column mapping in an explicitly coded method. Testing showed that this interface was orders of magnitude faster. The issue was how to change the 2,100 business class users of the data layer.

…

A large application under development cannot freeze code while a transformation of an interface is constructed and tested. We had to construct and test the transformations in a parallel branch of the code repository from the main development stream. When the transformation was fully tested, then it was applied to the main code stream in a single operation.

…

Less than 35 bugs were found in the 17,100 changes. All of the bugs were quickly resolved in a three-week period.

…

If the changes were done manually we estimate that it would have taken 8,500 hours, compared with 235 hours to develop the transformation rules.

…

The task was completed in 3% of the expected time by using Rewrite Rules. This is an improvement by a factor of 36."

…

from “Transformation of an application data layer” Will Loew-Blosser OOPSLA 2002

> A truly large refactoring is one that you want to try long before getting everything to compile.

For me, from experience, this is a sign that I or my coworker is creating an unreviewable tarball of a diff that will break something, can't be incrementally rolled back, and may not be easily fixed.

A truly large refactoring is one that I want to break up into individual smaller refactorings, each with a more reviewable diff, aided by automatic refactoring tools that help offload my workload. While it's possible to perform enough static analysis of dynamically typed source code for such tools to exist and aid the programmer, they're less likely to be as rock solid as statically typed source code refactoring tools, for something as simple as a method rename.

You can still do experiments with some adjustment to your work habits: create the new data structure with a different name, try it it out in some places via renames, and if necessary comment things out. Delete the old one and rename back again when you're done.

The one that still annoys me, though, is having to comment out unused imports in Go. I agree they should always be removed before submit, but in the meantime it's annoying. (Tools that automatic remove unused imports are also annoying in their own way.)

`goimports` both adds and removes imports. It has been excellent to run on save in emacs for me.

Leaving Haskell's deferred type errors aside for a moment; after you are done with your partially working code, what then? Relying on (the surely preexisting) 100% test coverage?

Say you have 65% test coverage over the refactored code. You have that before the refactoring and you have it after.

What does it mean? It means 35% of the code is being refactored without coverage. Its status is "unknown" before refactoring and "unknown" after.

Oh, but it compiles!

But if it compiles its status is not unknown. It means it is well typed, proving the absence of a whole lot of bugs.

Generally, refactoring in dynamic languages without tests or something like Clojure's schema is madness. Usually not a problem in strongly typed languages, even without much test coverage.

Well typed means nothing. Complete garbage can be well typed. Well typed proves the absence of a tiny, tiny subset of the possible bugs.

A subset which has nothing to do with, for instance, the corretness of loops. Because type checking doesn't verify those. Well typed doesn't even tell you whether a program terminates or not and on what inputs.

A program that is supposed to calculate pi could calculate e instead, yet be well typed (everything is a double-precision float, or a function from several of them to one, check!)

> Well typed doesn't even tell you whether a program terminates or not and on what inputs.

On the contrary, knowing that a piece of lambda calculus can be simply typed tells me for certain that the program halts for all inputs.

If you demand it work for arbitrary programs, then sure, well typed doesn't "even" tell you that. But no procedure can "even" tell you that (including, probably, anything that can be done by our brains), so it's a rather odd choice as a low-bar.

As I said above, you can verify/prove the invariants you capture in the types. I don't know what you mean by "correctness of loops", but if you capture whatever it means in a particular type, yes you can.

If you really wanted, you could derive a proof that pi is equivalent to some sort of corecursive series, which you can then evaluate in a dependently typed language, I guess. A proof is a type.

On the other hand, how would you write a unit test that checks whether something calculates pi without comparing its result to pi itself?

If I really wanted to waste my time, yes.

> A proof is a type.

Yes, Curry-Howard and all that.

If I just write a well-typed function which supposedly calculates pi, the rather trivial well-typedness is not informative by itself.

You're talking about adding reams of verbiage requiring expertise in using an advanced type system for executing a proof.

This isn't how static type systems are actually used and advocated in the field, and it is not feasible in general, only for toy, academic examples.

The proof code, which will exceed the size of the original function by at least an order of magnitude, could also be buggy. At the end of the day, it's just more code.

It reminds me of the argument fropm the Lisp camp: "Well, I could just write (supermacro ...) which implements any syntax and semantics whatsoever". (No, in fact you can't, and the proof is that you never actually will.)

> The dynamic world lets us have inconsistent code that partially works, rather than forcing us to follow up on all the places reached by the ripple effect of a change. Maybe the change turns out to be a bad idea in the end; then it was a waste of effort.

Except you can mostly do this reasoning just using the types. So you're rarely updating everything, you're just updating a few type definitions to see if your idea meshes well, and then you have to do the large refactoring.

I find, when I'm refactoring, that well designed types often lets the compiler help me think ahead of my code, and spot subtle contradiction before I've "reached" them in terms.

If lots of things change though... Couldn't that be a smell of bad boundaries? Like the change would not have been so drastic with the right abstractions?

It could be the smell of bad boundaries. But sometimes a data type can have many functions that work with its internals. The 75 functions might not sounds so bad if there is a good justification for their existence, and there are 7500 other functions which don't have to change which rely those functions.

At some level we need to actually implement things; we can't have abstraction all the way down!

I'm also reminded of Alan Perlis Epigram #9: "It is better to have 100 functions operate on one data structure than 10 functions on 10 data structures."

Reply on news.ycombinator.com