gradual-typing.md

TL/DR Not every type hole is harmful.

[Disclaimer: The following code is typed with scriptum, a type validator for dynamically typed Javascript. It has its roots in Haskell's Hindley-Milner based type system.]

It helps to consider mutations to get a better intuition. Mutations are a side effect and thus harmful. However, if we manage to hedge side effects so that we don't lose track of them, then we can benefit from the flexibility they provide without having to suffer the consequences.

For mutations this merely essentially means ensuring they stay local. Local mutations are fine in most cases. The same applies to type holes.

Let's work through some code to see if this claim holds. Gradual typing is a trade-off. Good coding means to find the most promising trade-offs.

The following factorial function relies on BigInt and uses a trampoline to prevent stack overflows for tremendous factorial numbers. While the trampoline is untyped the based upon factorial function is fully typed:

const fact = fun(
  init => tailRec(
    fun(
      ([acc, x]) => {
        if (x === 1n) return base(new Tuple(acc, 0n));
//                                ^^^^^^^^^^^^^^^^^^ A
        else return loop(new Tuple(x * acc, x - 1n));
//                       ^^^^^^^^^^^^^^^^^^^^^^^^^^ B
      },
      "[BigInt, BigInt] => {tag: String, value: [BigInt, BigInt]}")
  ) (new Tuple(1n, init)) [0],
  "BigInt => BigInt");
  
fact(10000n); // 28462596809170545189064132121198688901480514017027992307941..

fact calculates the 10000th factorial number without blowing the stack. For the recursive case it needs a counter and the accumulated factorial value (B), because it mimics a tail recursive algorithm. It makes perfect sense to use a tuple for storing the current state. We shouldn't use a list or array, because those have to be homogeneous and falsely suggest a non-deterministic computation.

The base case, however, only needs to return the final result (A), i.e. the 10000th factorial number. We still have to return a pair tuple, because the type system imposes the same type for both cases. At this point gradual typing comes into play.

Since the underlying trampoline is untyped, we can drop the type of the inner lambda. Freed from the type system we can just return the final factorial number. fact's domain and codomain are still typed, hence the emerging type hole is local and manageable:

const fact = fun(
  init => tailRec(
    ([acc, x]) => {
      if (x === 1n) return base(acc);
      else return loop(new Tuple(x * acc, x - 1n));
    }
  ) (new Tuple(1n, init)),
  "BigInt => BigInt");
  
fact(10000n); // 28462596809170545189064132121198688901480514017027992307941..  

This level of flexibility entails a lot of responsibility, of course, but carefully used it can facilitate typed functional programming in Javascript.

You may object that we could have used a tagged union as return type and you are right but that is not the decisive point of this post.

Check it out: scriptum