This tutorial gives an advanced introduction to string diagrams and graph languages for higher-order computation. The subject matter develops in a principled way, starting from the two dimensional syntax of key categorical concepts such as functors, adjunctions, and strictification, and leading up to Cartesian Closed Categories, the core mathematical model of the lambda calculus and of functional programming languages. This methodology inverts the usual approach of proceeding from syntax to a categorical interpretation, by rationally reconstructing a syntax from the categorical model. The result is a graph syntax -- more precisely, a hierarchical hypergraph syntax -- which in many ways is shown to be an improvement over the conventional linear term syntax. The rest of the tutorial focuses on applications of interest to programming languages: operational semantics, general frameworks for type inference, and complex whole-program transformations such as closure conversion and automatic differentiation.
翻译:本教程深入介绍用于高阶计算的弦图与图语言。内容以系统化方式展开,从函子、伴随和严格化等关键范畴概念的二维修辞开始,逐步推进到笛卡尔闭范畴——λ演算与函数式编程语言的核心数学模型。该方法论通过从范畴模型理性重构语法,颠覆了传统上从语法到范畴解释的研究路径。其成果是一种图语法——更精确地说,是一种分层超图语法——研究显示其在诸多方面优于传统的线性项语法。教程后续部分聚焦于编程语言领域的重要应用:操作语义学、类型推断的通用框架,以及闭包转换与自动微分等复杂的全程序变换。