The Ergonomics of Type Checking (2016)

https://michaelfeathers.silvrback.com/the-ergonomics-of-type-checking

by adamnemecek • 9 years ago

69 93 9 years ago

michaelfeathers.silvrback.com

zpr2• 9 years ago

Hate to be that guy but, Flow for JS is something like that. You can optionally enable it and even enable/disable it in certain files, functions, lines, etc.

hliyan8• 9 years ago

That is optional typing. The author is talking about gradual or progressive typing.

zpr2• 9 years ago

But he mentions he wishes he could start dynamically and end statically. By enabling Flow at the end, don't you basically achieve that? You can also enable it progressively for files as you move on, and still rapidly prototype without it. In fact, unless I'm mistaken I believe it's "opt-in" by default, ie. Flow won't scan the file unless you include the special comment keyword at the top of the file.

mercer2• 9 years ago

Could you explain the difference? I though TypeScript was a good example of gradual typing.

tuxracer• 9 years ago

The author's ideal language seems to also describe TypeScript https://eng.lyft.com/typescript-at-lyft-64f0702346ea

mebassett• 9 years ago

I can agree with the author's premise that types are essentially great, but it would be useful to have control over when (if ever) in the development stage I need to bring them, much like we do with testing. I guess there is an underlying analogy between TDD and strong static typing. I think this is one of the motivations for typed/racket, which is a lot of fun to use.

msl09• 9 years ago

I think that type hints are becoming like that in the python world. Almost all my code starts untyped and later I start adding types when they are not trivial

adrianratnapala• 9 years ago

The type checker has questions, and it is adamant about them, refusing to let you move forward until they are answered. Often, I’m ok with that. They are good questions, and most of the time they really should be answered. The question is: when?

This is a good point. The poster then proposes being able to nail down your types progressively -- which I think is fine as a long as you don't let the iteration cycle get too long.

Optionally typed languages are one way we approach this ideal. Another way is linters that are stricter than the compiler itself. You must run the compiler to have testable code, but you can run the linter later, perhaps only as part of CI.

It is possible that in future, both of these approaches will look like primitive exteremes of some richer process progressively nailing down the static safety of a program.

jryan492• 9 years ago

"Gradual typing" is one of the reasons I still love using Groovy :)

hliyan8• 9 years ago

I've recently come become aware of Groovy while looking for a programming language with Java's features _without_ the need for object orientation. How production ready is it? (I'm talking enterprise systems, not web based or consumer applications)

megaman22• 9 years ago

It's been around for a long time. Works pretty well as a scripting language to plug into Java enterprise systems. At least we've been using it for that for six or eight years.

pjmlp• 9 years ago

It was booming in JUG talks about 10 years ago, Sun was even doing talks about making it available as implementation language for JEE beans.

Nowadays if it wasn't for Gradle, I bet it would have been gone by now.

eikenberry• 9 years ago

It is good when used an an extension to Java. Sort of like TCL works with C. It is not so great if you try to use it as a stand alone language.

jryan492• 9 years ago

I really only use it as a glue code language or for automation. I thought that at least a few years ago there were a bunch of people using Grails? After using it extensively, I have found a few strange bugs that's killed some time but nothing show stopping. For what it's worth, the bugs were at least in their bug tracker. I would love to use it for everything but it seems to be losing popularity, which is really the only reason that makes me hesitant to do so. Maybe I should start contributing :)

dionian• 9 years ago

Kotlin and Scala are mostly superior choices to groovy for my purposes.

zmmmmm2• 9 years ago

There's no question it's production ready ... plenty of large companies are deploying it routinely in production for years. The real question is more the opposite of that - is it past its prime to the point where it will stop receiving enough fresh developer input to keep it up with modern trends? Groovy's lunch was mostly eaten by Ruby, unfortunately, and even that is looking old now.

For the other part of your question, it depends a bit what you mean by "without the need for object orientation". Groovy definitely relaxes a lot of the strict object orientation of Java. However, since it is based on the JVM it doesn't have platform support for core functional features like tail recursion and immutability. Groovy adds a number of features to add support for these, but as with all such features added after the fact, they aren't as good or reliable as if it was built into the core platform.

Groovy's forte is really in how it makes Java massively more developer friendly while staying within the original philosophy and maintaining full compatibility with Java. This is where I think it wins over Scala and other JVM languages which introduce their own types and radically different design philosophies. The integration of Groovy with Java is nearly completely seamless, and that's where I think it's actually really awesome for enterprise systems.

etatoby2• 9 years ago

Nowadays I would look at Kotlin, if you really need Java's slowness—er, features—in a shinier package.

I still use Groovy to write quick scripts or cron jobs that need to use Java libraries. Basically the Bash or Python of the JVM. Otherwise there are much better choices.

I've never worked on an "enterprise system, not web based," so I'm not sure what it is, but it sounds important and large. I wouldn't write such a thing in Groovy, or any other dynamically typed language: one misspelled variable and you have a runtime error waiting for you. (I wouldn't write such things in Java either: one missing null check and you have a runtime NPE waiting for you. But alas, the industry thinks otherwise.)

PS. Whatever you do, stay away from Grails. I've never seen such a bug-ridden, slow and crappy piece of junk in my entire career. And when I say bug, I mean a running production system suddenly starting to omit all WHERE clauses from all SQL queries, out of the blue. The app still working properly, but customers seeing the data of all other customers. I'm not joking.

zmmmmm2• 9 years ago

Same here - working up an algorithm is so much more pleasant when you can take advantage of all the Groovy features to get the logic right interactively in a REPL, then you can bring it into your code and sprinkle in types afterwards.

I quite like the pattern of having fully typed interfaces and type signatures while letting the body of a function be dynamic where it makes a big difference to expressiveness. Like a hard shell with a soft inside.

SolarNet2• 9 years ago

Julia does gradual typing very well. I think it delivers what the user wants. It has a REPL, you can write code using no types, as types are added to existing code it improves in performance and safety.

spullara• 9 years ago

This is related to why all my companies use TypeScript rather than plain JavaScript for their frontends and sometimes their backends (vs other languages).

hliyan8• 9 years ago

Can't a compiler be created to traverse the AST, locate all operations performed on the variable and infer the narrowest type definition that allows for all of those operations, and then enforce at compile time?

Edit: example to further clarify what I meant (it's a bit more than type inference at initial assignment)

    var x = readUserInput(); // narrow down: string, int, double
    x += y; // if y is also a user input, no change
    x += 1; // narrow down to int, double
    p = x % 2; // narrow down to int

llimllib• 9 years ago

My understanding is that Julia does something like this? But I'm far from an expert.

dnautics• 9 years ago

Yep. Julia is a great language and I think other languages could learn from it, especially it's typing model and the excellent implementation of the REPL. but I wouldn't say Julia is good for everything (I wouldn't want to write a web service in it).

bastawhiz• 9 years ago

Many languages do this (type inference), to some extent. The moment you have any expression that can evaluate to more than one type, though, it requires annotations.

hliyan8• 9 years ago

Are there any languages that do it beyond the first value assignment, or outside the current scope? Also, any languages that subsequently revise the type definition?

bitwalker3• 9 years ago

That's not always true, rank-1 polymorphic functions (i.e. functions polymorphic in their argument) don't usually require type annotations. Higher-rank polymorphic functions though do generally require them, because without the annotations type inference is undecidable in the general case for such functions. For example:

    pair x y = (x, y)

This function creates a pair for any two types, and doesn't require any annotations.

kreetx• 9 years ago

Depending on how versed you are in typed languages, but it looks like you're describing type inference, which exists in Haskell and in some other languages as well. I.e you don't need to add type signatures everywhere.

But gradual typing means avoiding typing alltogether in some parts of the program and in some sense going against the inferred type. This is probably most relevant in Haskell where IO is typed, and less so in others, e.g Clojure.

hliyan8• 9 years ago

I come from a C++ background, with a recent interest in JavaScript and Go. I'm trying to envision something a little more than simple inference. I'm imagining how I would take an untyped codebase and how I will infer the data type of a variable or a parameter by studying all its usages within the code.

pizza234• 9 years ago

You're describing type inference.

An example is Crystal; [edited] example from the website:

  if rand(2) > 0
    my_string = "hello world"
  end
  puts my_string.upcase

  Execution:

  $ crystal hello_world.cr
  Error in hello_world.cr:4: undefined method 'upcase' for Nil (compile-time type is (String | Nil))

hliyan8• 9 years ago

I edited my comment to explain further -- I'm talking about going beyond the initial assignment...

emodendroket5• 9 years ago

What do you do about two types with methods that have the same signature?

hliyan8• 9 years ago

It will need to be a language without method overloading.

seanmcdirmid3• 9 years ago

Yes. It works well as long as you have all the pieces and don’t have to worry about nominal subtypes.

hliyan8• 9 years ago

Could you explain a little more about the complications of nominal subtypes?

shados• 9 years ago

Call site analysis and such are ways to do that. That's for example the difference between TypeScript and Flow. The later does stuff like that (which is both a boon and a bane. Its amazingly powerful, but you can get into states where figuring out why you're getting a compile time error is a mind fuck. Languages Elm handle it beautifully though.

SolarNet2• 9 years ago

Julia does exactly this.

neilparikh• 9 years ago

Haskell has a flag called -fdefer-type-errors (https://downloads.haskell.org/~ghc/7.6.1/docs/html/users_gui...) that gets you pretty close to the experience of ignoring errors you don't care about right now.

twic2• 9 years ago

You can do something similar with Eclipse's compiler for Java, JDT, which features [1]:

An incremental Java compiler. Implemented as an Eclipse builder, it is based on technology evolved from VisualAge for Java compiler. In particular, it allows to run and debug code which still contains unresolved errors.

That means that you can write something like:

    private void describe(String string) {
        if (string.isEmpty()) empty();
        else nonempty(string);
    }
    
    private void empty() {
        System.out.println("empty");
    }
    
    private void nonempty(String string) {
        System.out.println("contains " + string.size() + " characters");
    }

Then you can still run the code and call describe, but if execution reaches nonempty, you get a runtime error telling you about the compilation problem.

It's one of the few things from Eclipse i miss when using IntelliJ.

[1] http://www.eclipse.org/jdt/core/

_pmf_• 9 years ago

And this has been working for a decade. It's one of the reasons I laugh in their face when a JS developer tries to sell his babel reload crap as progressive.

exceptione• 9 years ago

I can't see a problem with nonempty, am I stupid?

toolz• 9 years ago

I imagine the author would appreciate the static analysis/success type checking that erlang/elixirs dialyzer provides.

jingwen• 9 years ago

If you're interested in learning more about gradual type systems, check out Jeremy Siek's work [0, 1]. He's one of the early researchers in this area.

[0] https://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typin... [1] https://github.com/samth/gradual-typing-bib

emodendroket5• 9 years ago

The biggest value of static types is when you go to edit some code written years and years ago and you can tell what the hell the intended usage was without digging through the method

Guthur• 9 years ago

Not even remotely universally true. I've seen plenty of static code that is as obtuse as any dynamic code. Authorship holds far more sway than dynamic vs static.

emodendroket5• 9 years ago

It is 100% less likely that you'll run into out-of-date docs wrongly describing the types of the input arguments and return types. Of course the code might still be obtuse but the type declarations are a form of documentation that the compiler ensures is still up-to-date.

krylon• 9 years ago

Now that it is finally there, I can say this without the usual jokes we have grown so accustomed to:

Perl 6 does this.

Granted, (almost) nobody is using it, but it does exist (finally!).

hinkley• 9 years ago

Right on time too!

Back in like 2006 they were estimating that all of the stuff they wanted to put in 6 would require until 2016 or 2017 to complete. I figured that was a comment meant to negotiate down the scope to something reasonable.

Turns out, no...

nearmuse2• 9 years ago

So PEP 484? You can write out whatever and then add annotations (at least to the API).

zero_iq• 9 years ago

Also Cython: start with pure Python and add types and other annotations to get the performance gains of static compilation (to C Python extension).

pleasecalllater• 9 years ago

So you spend time writing the things, which then are totally ignored by the compiler/interpreter. Seems like a waste of time, except for documentation purpose.

dec0dedab0de• 9 years ago

Documentation is never a waste of time. Especially if your IDE is aware of it, and pointing out errors for you.

nearmuse2• 9 years ago

Those are actually enforceable by IDE or interpreter/compiler if implemented. Even if this wasn't the case, it is better than some arbitrary variable naming convention or comments format.

tedmiston5• 9 years ago

You can check them at runtime with mypy.

http://mypy-lang.org/index.html

quickben• 9 years ago

"I often wish I worked in a language where I could start dynamic and end statically."

C++ 'auto' type. Workflow:

1. Write 'auto =', see what the compiler picks up (iterator of a vector of a set of classes that points to a list of structs, etc).

2. Potentially copy/paste that (unless the line is bigger than 350 characters :) )

jeremyjh• 9 years ago

Type inference or deduction is not the same as dynamic typing. An auto variable resolves to exactly one type, which is determined by the expression it is bound to. If you pass that variable to a method expecting a different type, the compiler will stop you. If it were dynamically typed, it would let you proceed and fail at runtime.

nicoburns• 9 years ago

As much as it gets a bad rep, I think PHP is actually the language that comes closest to this. It's not quite there yet, as although newer versions of PHP have been adding optional type annotations, they are enforced at runtime rather than compile time. It seems not too much of a leap to imagine that some compile time checks might be added at some point though once type-annotated code becomes more universal.

viperscape• 9 years ago

“I often wish I worked in a language where I could start dynamic and end statically. There are a number of languages with optional type systems, but they aren’t the ones that I use.“

That’s a shame because typescript is basically this. Typing is optional, and you can become more granular as you want.

tedmiston5• 9 years ago

I often wish I worked in a language where I could start dynamic and end statically... I can imagine writing the core of an algorithm and then gradually tightening the conditions as it comes into focus. More than a tool, this would be a practice: progressive type elaboration.

Bingo. I love this idea. I haven't tried it yet myself, but I think mypy [1] from Dropbox makes this a reality today in the Python world.

[1] http://mypy-lang.org/

tylerjwilk00• 9 years ago

I know it's not a favorite lang around here but this is exactly what modern php is.

kod• 9 years ago

How exactly does modern php (not Hack or another vm) let you "start dynamic and end statically"?

declare(strict_types=1);

is checking and throwing type errors at runtime, not compile time.

ACow_Adonis• 9 years ago

I believe it's called Common Lisp, specifically SBCL :)

Live the dream :P

sitkack2• 9 years ago

Came here to mention MyPy and optional typing, the preferable term Gradual Typing means something distinctly different.

http://mypy-lang.org/about.html

Dropbox employs the creator of MyPy but it isn't a creation of dropbox.

Type Systems as Macros http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf

Pluggable Type Systems http://bracha.org/pluggableTypesPosition.pdf

Propositions as Types http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...

https://www.youtube.com/watch?v=IOiZatlZtGU

tedmiston5• 9 years ago

Came here to mention MyPy and optional typing, the preferable term Gradual Typing means something distinctly different.

Are you sure that gradual typing is different than what Mypy supports?

The Wikipedia page for gradual typing cites mypy as an example.

https://en.wikipedia.org/wiki/Gradual_typing

The Mypy docstrings specifically state:

Mypy has a powerful type system with features such as type inference, gradual typing, generics and union types.

https://github.com/python/mypy/blob/272d0c4c50918a36b57e7c0c...

The section on gradual typing in PEP 483 seems consistent with this as well.

https://www.python.org/dev/peps/pep-0483/#summary-of-gradual...

newen• 9 years ago

That's how I write in Julia. Start with an algorithm with no types and eventually introduce type contraints everywhere, and even adding new types.

mercer2• 9 years ago

General question for those more experienced than I am with statically typed languages: would Clojure's 'spec' or Elixir's 'dialyzer', or perhaps TypeScript, fit the bill? If not, what's the downside between these what appear to me 'gradually typed' languages/approaches?

To provide some context: my first experience with static (or rather explicit?) typing was TypeScript, and I really liked what I saw.

z3t43• 9 years ago

in JavaScript I pepper each function with if(...) throw, eg the program will throw if something is wrong. Doing this catches a lot of errors and bad state. - Without having to babysit a compiler (Typescript) and I can enjoy all the dynamic features. Sometimes I miss the type annotation as documentation, but then I just rename the variable to make it more clear what it is and does.

bitwalker3• 9 years ago

Instead of "babysitting" your compiler, you're "babysitting" your application at runtime - I fail to see the difference.

z3t43• 9 years ago

Good point. Think of it as hand-holding your peers instead of hand-holding the compiler. if(x==y) throw "friendly error" // avoids eternal loop ... The compiler doesn't care if you get an eternal loop at runtime, and static types wont prevent it.

iitalics• 9 years ago

I wish I had a language that did optional typing
they exist, but I don't use them.

The author's thoughts (I want to write dynamically to get the code working, but then make it static afterwards) are nearly the exact thing I've heard from Matthias Felleisen when he talks about the motivation behind Typed Racket.

The Ergonomics of Type Checking (2016)

Related Stories