Learning Elm has gotten me confused about static vs. dynamic typing
rundis.github.io
rundis.github.io
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 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.
Maybe adding dynamic typing to a thoroughbred static language could turn out more fruitful than efforts to go the other way.
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.
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.
This is precisely why I have nightmares about refactoring dynamic codebases.
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.
So generally, the more invariants you manage to capture in your types, the more categories of bugs you can statically prove will never happen.
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.
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.
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."
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.)
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".
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.
You certainly don't need to write tests that Math.floor will return NaN when you pass it something that's not a number...
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!
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 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).
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.
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.
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.
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.
[0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
Agreed.
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.
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.
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.
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.
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!
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.
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!)
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?
> 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.)
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.
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."
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.)
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.
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.
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
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 :)
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.
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
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.
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.
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...
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.
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.
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.
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...
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.
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).