Implementing type checking as another interpreter, with short, accessible examples: https://kubyshkin.name/posts/type-checking-as-evaluation/