CPU: Intel Core i5-7500 @ 4x 3.8GHz（支持 SSE2、MMX、FPU、VME）
GPU: NVIDIA GeForce GTX 750 Ti（支持 CUDA）
RAM: 2048M DDR4

/*
 * title: type safe printf
 * author: nicekingwei
 * related knowledge:
 *  - value and type
 *      value->value: function
 *      type->value: parametric polymorphism
 *      type->type: generic
 *      value->type: dependent type
 *  - auto
 *  - if constexpr
 */

参数多态在程序设计语言与类型论中是指声明与定义函数、复合类型、变量时不指定其具体的类型，而把这部分类型作为参数使用，使得该定义对各种具体类型都适用。参数化多态使得语言更具表达力，同时保持了完全的静态类型安全。[1] 这被称为泛型函数、泛型数据类型、泛型变量，形成了泛型编程的基础。

参数多态名字来源于其发明人克里斯托弗·斯特雷奇，[2]与特设多态（ad hoc polymorphism）相对。特设多态是指一个多态函数有多个不同的实现，依赖于其实参而调用相应版本的函数。因此，特设多态仅支持有限数量的不同类型。

在计算机科学和逻辑中，依赖类型（或依存类型，dependent type）是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依赖类型可对应于谓词逻辑中的全称量词和存在量词；在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中，依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误。