[weavejester]

I don't see an asymmetry in the abstraction. Both vectors and maps are associative structures - you can assign a key to a value - the only difference is that vectors have a more constrained keyspace (i.e. ordered, consecutive integers starting from zero).

But that wasn't really my point. Even if we limit `assoc` solely to maps it would still be difficult to type effectively.

For instance, suppose we have some code like:

    (let [m* (assoc m :number 3)]
      (:number m*))

We can see that the return type of this expression is obviously an integer, but what is the type of m*? How do we type m* such that (:number m*) can be inferred to be an integer by the compiler?

Most statically typed languages sidestep this problem: instead of using an open data structure like a map, a closed structure like a record or class is used instead, and these structures must be explicitly typed by the user.

The problem with this approach is that now every record is specific and bespoke. You lose access to all the general-purpose functions that operate on generic data structures, and as records and classes are closed, you also lose the ability to extend them.

This is the ultimate problem with static type systems: you're trading capability for safety. If you're programming within a static type system, there are options that are simply not available or feasible to use.

[IceDane]

> I don't see an asymmetry in the abstraction. Both vectors and maps are associative structures - you can assign a key to a value - the only difference is that vectors have a more constrained keyspace (i.e. ordered, consecutive integers starting from zero).

The asymmetry lies in the fact that it's an overloaded function that's supposed to do the right things every time, but in some cases, it does what is arguably the wrong thing, silently, and in others, it refuses to do the wrong thing and fails loudly. It's better that it fails loudly, of course, but the point is that the ergonomics of the abstraction is lessened because you can't just assume it will work. You effectively have to keep the types of all the things involved in your head and/or trace them to ensure that you don't run into a crash.

> We can see that the return type of this expression is obviously an integer, but what is the type of m? How do we type m such that (:number m*) can be inferred to be an integer by the compiler?

This is trivial in TypeScript. You can see it in action here: https://www.typescriptlang.org/play/?#code/MYewdgzgLgBAtjAvD...

  const m = { name: "weavejester", active: true };

  const mStar = { ...m, number: 3 };
  //    ^? const mStar: { number: number, name: string, active: boolean }

  const x = mStar.number;
  //    ^? const x: number

> This is the ultimate problem with static type systems: you're trading capability for safety. If you're programming within a static type system, there are options that are simply not available or feasible to use.

This is just not true. It's true for some certain specific static type systems, but not true in general, and that brings me back to my original thesis: You just need a sufficiently capable type system with the right properties - structural/row polymorphism, ish, plus type inference. And also my Haskell point: it doesn't have to be an incredibly complicated type system that is beyond mortal ken. TypeScript is already doing this and it's arguably one of the most used programming languages on earth.

[weavejester]

> You effectively have to keep the types of all the things involved in your head and/or trace them to ensure that you don't run into a crash.

You make this sound difficult, but in practice type errors are rare in Clojure and generally caught in the REPL or by tests, since the moment you go down a branch with a type error an exception is thrown.

Contrast this to errors caused via mutable state, which are usually far harder to track down, because the failure condition is more specific.

> This is trivial in TypeScript.

In the example you give you're omitting assoc entirely, which defeats the point. I'm using assoc as a minimal example, but the same principle applies to more complex functions, so replacing assoc with the equivalent expression doesn't tell us whether or not we can effectively type a function that deals with maps.

So lets try doing this properly. At minimum we need something like this:

    type Assoc<M extends object, K extends string, V> =
        Omit<M, K> & Record<K, V>;

    function assoc<M extends object, K extends string, V>(
        m: M, k: K, v: V): Assoc<M, K, V> {
      return { ...m, [k]: v } as Assoc<M, K, V>;
    }

(Note that we need to perform an explicit cast in order to inform TypeScript of the type of the key.)

However, this produces some rather messy types consisting of nested Assocs. In order to get back to something a human can read, we can use an additional Simplify type to force the type system to reduce it back down into an typed object:

    type Simplify<T> = {[K in keyof T]: T[K]} & {};

    type Assoc<M extends object, K extends string, V> =
        Simplify<Omit<M, K> & Record<K, V>>;

    function assoc<M extends object, K extends string, V>(
        m: M, k: K, v: V): Assoc<M, K, V> {
      return { ...m, [k]: v } as Assoc<M, K, V>;
    }

(The empty `& {}` intersection forces normalization, providing a cleaner reported type.)

We're still not done, though, as if we want the same type checking that a class has, we need to ensure that a key cannot be overwritten with a value of a differing type. So we'll type the value argument as well to ensure it matches the type of an existing value within the map:

    type Simplify<T> = {[K in keyof T]: T[K]} & {};

    type Assoc<M extends object, K extends string, V> =
        Simplify<M & Record<K, V>>;

    type AssocValue<M extends object, K extends string, V> =
        K extends keyof M ? (V extends M[K] ? V : never) : V;

    function assoc<M extends object, K extends string, V>(
        m: M, k: K, v: AssocValue<M, K, V>): Assoc<M, K, V> {
      return { ...m, [k]: v } as Assoc<M, K, V>;
    }

So this is possible to type in TypeScript (to its credit), but is it "trivial"? And is this type signature significantly less complex than one might find in Haskell?