Type holes in TypeScript

gcanti

Giulio Canti

Posted on June 27, 2019

Type holes in TypeScript

Sandy Maguire recently wrote a nice article about type holes (Implement With Types, Not Your Brain!), this blog post is a porting to TypeScript.

What's a type hole?

The idea is to implement the tiny part of a function that you know how to do, and then ask the compiler for help on the rest of it. It's an iterative process. It's a discussion with the compiler. Each step of the way, you get a little closer to the right answer, and after enough iterations your function has written itself — even if you're not entirely sure how.

TypeScript doesn't support type holes but they can be kind of simulated.

A first example

Let's see the first example from the article

declare function jonk<A, B>(
  ab: (a: A) => B,
  ann: (an: (a: A) => number) => number
): (bn: (b: B) => number) => number
Enter fullscreen mode Exit fullscreen mode

In order to simulate a type hole I'm going to use the following function declaration

declare function _<T>(): T
Enter fullscreen mode Exit fullscreen mode

Let's put it into the jonk's body

function jonk<A, B>(
  ab: (a: A) => B,
  ann: (an: (a: A) => number) => number
): (bn: (b: B) => number) => number {
  return _()
}
Enter fullscreen mode Exit fullscreen mode

If you move the mouse over the "type hole" _ you can see what TypeScript infers for its type parameter T

(bn: (b: B) => number) => number
Enter fullscreen mode Exit fullscreen mode

So what is the type checker telling us? Two things

  • The expression we want to replace _() with must have type (bn: (b: B) => number) => number.
  • We have some local binds (ab, ann, jonk, and their types) that we can use to help with the implementation.

Since our hole has type (bn: (b: B) => number) => number we should bind the bn in a lambda (I'll just write the function body from now on)

return bn => _() // inferred type: number
Enter fullscreen mode Exit fullscreen mode

What's the new inferred type? number. How can we produce a number? We can use ab, ann or bn. Since both ann and bn return a number let's choose ann as a guess

return bn => ann(_()) // inferred type: (a: A) => number
Enter fullscreen mode Exit fullscreen mode

Our new hole has a function type, so let's introduce a lambda

return bn => ann(a => _()) // inferred type: number
Enter fullscreen mode Exit fullscreen mode

We need to produce a number again, let's choose bn this time

return bn => ann(a => bn(_())) // inferred type: B
Enter fullscreen mode Exit fullscreen mode

Now we need to produce a B. We have a function that can do that, ab: (a: A) => B

return bn => ann(a => bn(ab(_()))) // inferred type: A
Enter fullscreen mode Exit fullscreen mode

Finally, we have a hole whose type is A. Since we have an A (the a parameter) let's just use that

function jonk<A, B>(
  ab: (a: A) => B,
  ann: (an: (a: A) => number) => number
): (bnn: (b: B) => number) => number {
  return bn => ann(a => bn(ab(a)))
}
Enter fullscreen mode Exit fullscreen mode

Now we have a complete implementation, almost driven by the type checker.

The second example

Let's tackle the second example of the blog post: zoop

declare function zoop<A, B>(abb: (a: A) => (b: B) => B, b: B, as: Array<A>): B
Enter fullscreen mode Exit fullscreen mode

We notice that as has type Array<A>, let's "pattern match" on that using foldLeft

import { foldLeft } from 'fp-ts/lib/Array'
import { pipe } from 'fp-ts/lib/pipeable'

function zoop<A, B>(abb: (a: A) => (b: B) => B, b: B, as: Array<A>): B {
  return pipe(
    as,
    foldLeft(
      () => _(), // inferred type: B
      (head, tail) => _() // inferred type: B
    )
  )
}
Enter fullscreen mode Exit fullscreen mode

We need to produce a B for the "nil" case (i.e. when the array is empty). Since we have a B let's just use that (I'll just write the function body from now on)

return pipe(
  as,
  foldLeft(
    () => b,
    (head, tail) => _() // inferred type: B
  )
)
Enter fullscreen mode Exit fullscreen mode

Again we want to produce a B for the other case and we want to call abb. Since it takes two arguments, let's give it two holes

return pipe(
  as,
  foldLeft(
    () => b,
    (head, tail) =>
      abb(
        _() // inferred type: A
      )(
        _() // inferred type: B
      )
  )
)
Enter fullscreen mode Exit fullscreen mode

head has type A so let's use it

return pipe(
  as,
  foldLeft(
    () => b,
    (head, tail) =>
      abb(head)(
        _() // inferred type: B
      )
  )
)
Enter fullscreen mode Exit fullscreen mode

Now we must to produce a B and we want to use tail which has type Array<A>. Our only option is using zoop itself

function zoop<A, B>(abb: (a: A) => (b: B) => B, b: B, as: Array<A>): B {
  return pipe(
    as,
    foldLeft(() => b, (head, tail) => abb(head)(zoop(abb, b, tail)))
  )
}

// p.s. `zoop` is `reduceRight`
Enter fullscreen mode Exit fullscreen mode

The reason why this works is known as theorems for free, which roughly states that we can infer lots of facts about a type signature (assuming it's correct.)

💖 💪 🙅 🚩
gcanti
Giulio Canti

Posted on June 27, 2019

Join Our Newsletter. No Spam, Only the good stuff.

Sign up to receive the latest update from our blog.

Related