Sort of along the lines above, is it possible that what people are looking for with static types is an additional alternative view of a function? I've found very little reason for types in my work from a compiler perspective, but it does often occur that I see a function name and argument list without knowing what to do with it. e.g. the following:

(map (fn [price-bracket]
       (let [groups (group-by :contract-type price-bracket)]
         (mc/map-vals (fn [contracts]
                        (dt/aggregate-table contracts
                          {:selected-keys      [:returns
                                                :revenue 
                                                :cost
                                                :market-price]}))
           groups)))
  individual)

This could alternatively be shown as

[[{whatever keys} ...] ...]
=> [{contract {:returns ... :revenue ... :cost ... :market-price ...} ...} ...]

Which, along with a name is far faster to grok and read past

I'd say that functions also usually entail a transformation of some kind - a type is useful to understand the pre-transformation state (and often a separate type for the post-transformation state - why it's helpful to spell these out as explicit function signatures)

Static types also help during refactor. Add a parameter to a function — compile errors show you all the places that you need to pass it. Convert parameter from string to aggregate structure — same thing, you have a list of places that you need to fix. This makes me quite comfortable doing large-scale refactorings. With dynamically-typed languages I'm much more cautious

The growing prevalence of pattern matching in modern languages seems to bear this out.

@Alexey Shmalko the refactor concern is a good one. I've long asked myself how to better manage refactoring from a dynamic perspective — as opposed to adding static features to a dynamic language. Since a refactor wants to be behaviorally invariant (to some degree), why not keep track of the behavior? Consider the case of changing a parameter type. If the normal brain dynamic way is to make the change and see what tests break, then the galaxy brain dynamic way would be to show all the places where code needs to change from having remembered (traced) all the times the function is called in practice. Using traces in this way feels a lot like static analysis and loops around when you switch from concrete traces to more symbolic/partial kind of evaluation. You find yourself back in familiar static typing territory when the symbolic evaluation is more limited.

@Kartik Agaram What do you mean by "The growing prevalence of pattern matching in modern languages seems to bear this out."? I'm trying to reach for examples of pattern matching in modern languages and am drawing a blank.

Approximately in chronological order: SML: https://courses.cs.washington.edu/courses/cse341/04wi/lectures/03-ml-functions.html Haskell: http://learnyouahaskell.com/syntax-in-functions Scheme: https://www.gnu.org/software/guile/manual/html_node/Syntax-Rules.html Scala: https://docs.scala-lang.org/tour/pattern-matching.html Rust: https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html Swift: https://docs.swift.org/swift-book/ReferenceManual/Patterns.html Etc.

Erlang/Elixir, too.

This is very close to what I am imagining: a gradual typechecker that can deal with holes. Sort of a combination between the Typescript compiler and Hazel. Except in addition to being "gradually typed", the language would be "gradually programmed": the user would initially provide only names with some (loose) type annotations and (later) maybe some implementation details attached to them (which is why I realize my use of the term "pseudocode" was probably more misleading than anything).

@crabl You may like something like this https://github.com/fulcrologic/guardrails

Sounds like assertions? Or Eiffel-style Design by Contract? https://en.wikipedia.org/wiki/Design_by_contract