Slogans about Mainstream Dependent Types

I find it can be hard for programmers to talk about dependent types, since we don't always have the same idea of what they are and they have a reputation of being hard to understand and implement. I want to share these slogans to (hopefully) make the conversation easier.

I wrote this in a hurry and would welcome comments with examples of "mainstream dependent types" - and any relevant corrections and links.

Note: "mainstream" is a moving target

"A dependent type is a type whose definition depends on a value."

This is the first sentence of the Wikipedia article "Dependent Type". The lambda cube article has a similar definition. If you prefer non-Wikipedia sources, Why Dependent Types Matter defines them as ""... types expressed in terms of data, explicitly relating their inhabitants to that data", which sounds like the same thing to me.

Note that this is all and only what dependent types are. "Dependent types are what Idris and Agda have" is not a useful definition. Nor is "sigma and pi types", the latter being merely examples of dependent types.

"Mainstream dependent types are everywhere"

They are everywhere in our programming languages and in our code. I'll give several examples that use stringy singleton types, just because:

these are especially common
the examples are relatively easy to follow
you won't find any mention of them in most discussions of dependent types

MyPy/Pyre, TypeScript, and Flow all have dependent types. To take one example: function overloads with string literal types in TypeScript:

declare function foo(arg: "gimme_number"): number
declare function foo(arg: "gimme_string"): string

And to see a ton of dependent types in action, look no further than dynamically-typed code.

  req.on('connect', (res, socket, head) => {
    /* code that uses socket.write */

  ...
hal
  req.on('error', (e) =>
         /* code that handles e.message */

Adapted from the Node docs

This is well-typed code: the type-checker in people's heads doesn't have much trouble knowing the difference between the two strings 'connect' and 'error', and TypeScript and Flow don't have much trouble with this kind of code either.

Or Some Erlang:

handle_call(increment, _, State) ->
    {reply, ok, State#{total = State#state.total + 1}};
handle_call(get_total, _, State) ->
    {reply, State#state.total, State}.

This is also well-typed code, which the typechecker in people's heads also doesn't have much trouble with: the shape of the reply depends on whether the function is called with increment or with get_total.

Here's a function that returns the value for a given key in an object. Read the implementation first, then the signature: they do the same sort of thing. The return type depends on the particular object and particular string that are passed in:

function get<O, K extends keyof O>(object: O, key: K): O[K] {
    return object[key]
}

// inferred to be a number
const s = get({key1: 1, key2: "two"}, "key1")

The above examples is essentially the same as Python's getattr. Fun aside: the type system features involved in the tiny example above plus conditional and recursive types were sufficient to make TypeScript accidentally Turing-complete. So there is a grain of truth to some of the FUD around dependent types. They are indeed expressive. But is that a problem? How is an infinite loop in a type checker worse than an infinite loop at runtime?

Mainstreamish dependent types that go further than just stringy stuff:

In Java, overloaded methods can take classes as parameters, where classes play double-duty as both types and values. I think this is used for things like type-safe dependency injection and service discovery. Sorry I don't have an example.
Dhall is a configuration language that can generate Yaml and JSON. Dhall added dependent types in order to make it easy to import mixed bundles of types and values, leading to something like this being expressible: let f = \(b : Bool) -> if b == True then Natural else Integer. tiny spec change pr tiny implementation change pr. This kind of thing is useful in Dhall because its modules are plain values, and a typical way of exposing things from a module is for the module to be a record.
More examples needed, it's embarassing I mostly only have the stringy ones

Note that I haven't gone anywhere close to the common literature examples of dependent types. Plenty has been written about not-yet-mainstream dependent types. Here are some I (a programmer) found accessible:

Programming with dependent types (at the edge of mainsream practicality): https://www.manning.com/books/type-driven-development-with-idris
Proving with them: http://plfa.github.io/

I chose to say "mainstream" instead of "lightweight". That's because there is nothing "lightweight" about having an entirely separate mini-language at the type level of one's programming language. And nothing necessarily heavyweight about avoiding the two-language problem.

"Dependent types are not Haskell extensions"

"Number of Haskell extensions required" is not an accurate measure of how fancy a programming language feature is.

Here's a metaphor: imagine you are designing Scheme or Lua and want to add the ability to pass a function as an argument. Someone replies, "No way! That requires implementing a Java-style class system with anonymous inner classes." No, the Java class system does not shed much light on the nature of funargs. It is a hack that obscures more about functions-as-args than it reveals.

Similarly, seeing what is possible with Haskell is delightful, but type-safe generic programming has nothing to do with Peano numbering or undecidable instances.

"GADTs are dependent types, but dependent types are not GADTs"

Here's what a GADT is: an algebraic data type where the constuctors can have different return types. No more, no less. That's probably not illuminating, this practical article on GADTs in OCaml explains them well.

GADTs are dependent types: the type of a GADT value depends on which constructor was used. When pattern-matching on any algebraic data type (including GADTs), one is doing a runtime check on the value and gains more type information in doing so.

Dependent types are not GADTs. Understanding the examples under slogan 2 above will not be enhanced by thinking of anything as a GADT. GADTs are a munging-together of features which can all be used separately:

"GADT" stands for "generalized algebraic data type" but they aren't especially general. And it's odd terminology: we don't call dependent function types "generalized functions" or dependent pairs "generalized pairs."

"Type Inference is not Everything"

The literature on GADTs (for example) has a strong focus on making types as inferrable as possible. This is for historical reasons (diagnosed here). One solution when a programming language feature complicates type inference is to do less type inference.

Type annotations are not all bad, they can:

be useful documentation for the reader: that's probably why in practice Haskell and OCaml devs annotate their public functions.
improve the dev experience by making type errors more local
much more discussion of this: in the same talk linked above

mheiber/slogans-about-mainstream-dependent-types.md

Slogans about Mainstream Dependent Types