主要观点：通过一篇名为《Type Systems as Macros》的论文，介绍如何用未类型化的宿主语言和宏扩展来实现类型化语言。文中以 Racket 语言为例，详细阐述了实现过程及相关代码，包括各种宏（如checked-λ、checked-app等）的定义与作用，以及辅助函数（如comp+erase-τ、comp+erase-τ/ctx等）的功能，还讨论了函数与宏的依赖关系和阶段分离等问题。
关键信息：

• 用rename-out重命名#%app和λ，方便在代码中使用自定义的宏。
• checked-λ宏用于定义带类型的λ表达式，checked-app宏用于函数应用的类型检查。
• comp+erase-τ和comp+erase-τ/ctx辅助函数用于计算和删除类型信息，comp+erase-τ/ctx还需考虑上下文。
• 利用add-τ和get-τ函数处理类型信息，定义了简单的类型相等性检查函数τ=。
• 通过define-for-syntax调整函数和宏的阶段，确保正确的依赖关系。
  重要细节：
• checked-app中使用stx-map处理参数的类型计算，因为参数是模板变量。
• comp+erase-τ/ctx通过创建带类型信息的临时变量和let-syntax来处理上下文相关的类型检查。
• local-expand在宏扩展时用于展开语法中的宏，需在宏内部使用。
• 代码示例展示了简单类型化λ演算的实现及类型检查过程，包括各种函数和表达式的示例。
• 提及论文作者及相关参考文献，对 Ben Greenman 表示感谢。