高阶类型（Higher Kinded Types）对我这个 PL 爱好者来说，几乎是必备的语言特性了。Typescript 是我主要使用的语言之一，它虽然不直接支持高阶类型，但利用它本身已经比较强大的类型系统，是可以模拟出高阶类型的。

从寒假开始，断断续续地玩了两个月 Idris。最开始让我决定开 Idris 这个坑的还是 这篇文章 中的这句话：

Idris 是极少几种可以实现强类型 printf 的语言。

那么下面就开始利用依赖类型构造一个强类型的 printf 函数吧！