102 comments

[ 42.0 ms ] story [ 818 ms ] thread
> 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.

This is my experience in a nutshell, my "home language" has been Python since high school after trying to learn C/C++ and persisted through learning Java in college. It was easy to use and get started with, and didn't require a ton of extraneous typing in Vim or looking up class types and returns every time you tried to use something.

For simple projects as a beginner dynamic/implicit typing is wonderful because you need fewer references. Having gone the way of the IDE, however, having good autocomplete, safe refactoring, error flagging before compilation/runtime, and an easy reference for your libraries has made me incredibly efficient in explicitly typed languages. I'm not sure how much longer I'll be using Python as my home language...

To be fair, at least good autocomplete + easy reference is quite possible in an IDE with dynamic languages.

I have it for Common Lisp in emacs for example(it requires running a live repl and having the editor connect to it).

Pre compilation errors are harder, and I personally don't feel safe refactoring in any language unless there are good automated tests. Static typing makes it better, but nowhere near full proof.

It is, but it has a lot harder time deciding what type of object I'm working with in a function vs. being able to specify the object's class in the function arguments. You can get that with docstrings but it's not as straightforward as just saying "def frobozinator(FooBar thing):"
Either it's your code, in which case why don't you know what type of object you are passing, or it's a documented part of a framework or something.

With polymorphism and inheritance in the mainstream languages, the method signature still doesn't exactly tell you what you are going to get, so you have all of the pain of micromanaging type annotations and you still don't really get an invariant.

Also, Python has function annotations if your purpose is to document the signature without using docstrings. I'm unsure why you don't mention these because they are exactly analogous to what you say is straightforward.

Knowing in my head and having it tab out are two different things.

Interfaces will without a doubt tell you what you can do with a given object. With polymorphism you most assuredly know what types the arguments are inside each signature you write.

Function annotations look like shit[0] and are not guaranteed to mean the same thing across projects.

Don't get me wrong, I love Python and its idioms and have been using it for a rather long time. It pays the bills and I am productive in it. I just think that I've outgrown its implicit typing when I step into an explicitly typed language using modern tools and enjoy myself.

[0]: https://www.python.org/dev/peps/pep-3107/#syntax

> With polymorphism and inheritance in the mainstream languages, the method signature still doesn't exactly tell you what you are going to get, so you have all of the pain of micromanaging type annotations and you still don't really get an invariant.

This is exactly what is addressed by the Liskov substitution principle [0] -- the "L" in SOLID [1]. If your subtype does not have the same semantics as the type it extends, then it fails this criteria. It is violating the (implicit) contract of the type it is extending.

[0] https://en.wikipedia.org/wiki/Liskov_substitution_principle

[1] https://en.wikipedia.org/wiki/SOLID_%28object-oriented_desig...

What do you use now?
I haven't yet replaced Python, but I really enjoyed Dart using JetBrains' WebStorm IDE for a side project.

Python maps really well to a lot of the problems that I'm tackling right now professionally, but I'm considering trying to use Java for a number of them. C# may wind up being viable for me as well; it has a chance of being a little more cross-platform with Xamarin's purchase by MS and overtures toward OSS and Linux by integrating Ubuntu.

I used to be a huge Python fan until I found Scala. It can be as expressive as Python (slightly more so even), but as safe as Java (again, slightly more so).
Unfortunately Java is far from safe, NullPointerException and ClassCastException abound. Which isn't surprising given that Java was originally inspired by ObjectiveC, a mostly dynamic language. Scala has a sort of ML subset which mostly avoids these errors, but unless you need the JVM, why not try OCaml or Haskell?
Default-nullable types and thereby having to check for null in every non-primitive argument is definitely a thing in Java, but I don't think I've seen a ClassCastException in the wild for a very long time... Generics pretty much solved the problems that led to bad casts, such as a integer sneaking into your list of strings.
Yes true, Generics helped a lot (thanks to Odersky and Wadler). But the language does seem to encourage more dynamic frameworks like Spring, that IIRC do perform a lot of casting.
There are some Java libraries based on reflection, sure, including Spring. They're not widely used from Scala.
I agree that those are good languages - my reasons for using Scala rather than OCaml or Haskell are mostly boring practical ones (interop with Java, employment, tooling). That said I do think higher-kinded types are very valuable (which rules out OCaml until they finish the modular implicits feature), and that eager evaluation is very useful if there's a chance performance might become important at some point.
Python is apparently the first language you used in anger and now you want to use other things, but that simply doesn't mean that it is unsuitable for experienced people or complex projects.
> 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.

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.

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

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

"Compiled" and "dynamically typed" are not opposites.
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.)

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!

(comment deleted)
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.

I love compiler errors - because I'm the only one who sees them.
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 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.
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.
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.

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

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

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

(comment deleted)
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."

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

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

> 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

> I’m convinced that functional programming vs imperative programming is a much more important concern...

Except that you can be functional and imperative, like Clojure, Erlang and even OCaml. Those are functional-imperative languages (you can even be pure and imperative yet not functional, like Esterel and maybe Céu).

> Does this mean I’m a static typing zealot now ?

That part made me chuckle, because it made me realize that a typing zealot is exactly what I've become! I used to be a huge fan of Ruby and I was using it for everything, and now 10 years later I'm a huge fan of Haskell instead, I give talks about how JavaScript is horribly error-prone and how Elm is so much better because not only is it statically-typed, it's also purely-functional, and yadi-yadi-ya.

The transition occurred so smoothly that I didn't notice it. Beware! You might not be a zealot now, but if you continue on this path, you might unintentionally become one too :)

As you said, this is slowly happening to me. I love being able to prototype systems in languages like python and matlab, but at the same time it feels like building on sand, especially when other developers get involved.

Recently while writing some matlab found a great example of the sort of trouble a decent type checking system will save you. The predict method takes a machine learning model, and applies it to some data. The output however, is up to the model, and not all models return the same data type (e.g. column vector of doubles, or cell array of strings), making it a pain in the butt to do any abstraction over models.

I am excited for languages like lbstanza that let you have your cake and eat it too.

Whatever Scala devotees may believe, I think FP and OOP are irreconcilable opposites which means if you really get into FP you're going to hate doing what the industry demands of you in your day job, ie. OOP. Maybe FP will one day become the dominant paradigm but until then treat it like alcohol - too much and you cease to function in the "real" world. I exposed myself to Rich Hickey's Sermons From The Hammock a few years ago and Clojure just blew my mind. Since then I get a churning feeling in the stomach when I have to dealt with OOP, ie. Ruby, PHP, Python. The effects are irreversible so beware - immutable data mixed with pure functions is a potent drug.
FP and OOP are totally not irreconcilable. Most modern languages offer both, including the most highly used dynamic languages. Javascript really cracked this nut with its function expressions. Scala's main contribution here is applying static typing to that mixture in a largely coherent way.
As soon as you create a class you're binding data and methods inside a black box. It's the very antithesis of FP. Of course you can freeze and fiddle with your class to make it "more functional" but it doesn't wash because in FP functions are supposed to be "free", ie. unboxed.
I wouldn't necessarily agree with this. Many functional programmers actually prefer some of the advantages of black boxes. Even methods as a calling interface vs functions are more a stylistic difference (when you aren't factoring in subtype polymorphism). OO languages tend to have the convention of not keeping effectful operations in methods referentially transparent (with effectful values), but there's nothing inherent to the idea of OO that says this must be the case. Scala could just as easily have something like haskell's IORefs instead of vars and make use of an IO monad to achieve a similar effect.

I'd argue the bigger difference between the two styles is with methods of polymorphism, but even functional programmers in different camps probably don't agree on the reasons for why they prefer not to have subtype polymorphism.

Your opinions about encapsulation probably have more to do with your preferences wrt typing discipline. Functional programmers who prefer static types often view black boxes as an asset. In fact black boxes form the basis of the free theorems, which can provide some nice assurances about the behavior of code that has few assumptions about the data it receives: https://bartoszmilewski.com/2014/09/22/parametricity-money-f...

Similarly, data without exposed constructors can be used to enforce strong invariants about code using techniques like smart constructors: https://wiki.haskell.org/Smart_constructors

Black boxed data also conveys advantages for library maintainers. It makes it much easier to change implementation details, because you're only required to preserve the semantics of functions operating over data rather than its exact innards. Not doing this for the String data type in haskell is arguably the largest reason why it won't be phased out to the superior Text type: http://dev.stephendiehl.com/hask/#string

It might be the particular OOP languages you're used to. Ruby, PHP and Python all have pretty strong cultures of relying on mutation and side effects. Part of this might be that the languages are so focused on dynamicism that you really have to go out of your way to even suggest that a type should be immutable. And even then it's only a matter of time until someone mucks it up by applying a mutable mixin to the type.

In other languages, though, it's perfectly possible to create immutable classes that can only be interacted with using pure functions. You could argue that it's questionable that these do anything you can't do better with records and algebraic data types, and there's something to that. But there's also something to taking the pragmatic approach and not letting the (presumably) remote odds of your employer adopting a niche language prevent you from writing better code.

> Whatever Scala devotees may believe [...]

It's not just Scala devotees. You should read [this post][1] by Alan Kay (Turing Award winner, designer of Smalltalk). He arrives at a conclusion that might surprise you:

> I think of "objects" and "functions" as being complementary ideas and not at odds at all.

Largely what you may be referring to is the idea of purity and mutation being at odds, but these are orthogonal from the ideas of OOP and FP.

A very interesting read.

[1]: https://news.ycombinator.com/item?id=11808551