一句话：展示如何用 λProlog/Makam 的高阶逻辑编程快速原型化带复杂类型系统的函数式语言实现。
本文是一篇函数式珍珠，论证高阶逻辑编程（以 λProlog 设计为代表）是快速原型化复杂类型系统语言实现的理想工具。作者以准文学化方式开发一个类型检查器，从若干复杂特性逐步扩展到带代数数据类型与类型泛化的 ML 风格核心，并加入可泛化于单独定义项语言的 staging 构造。每次新增特性几乎无需改动已有代码。为应对对象语言中的复杂变量绑定模式与通用结构遍历，他们在 λProlog 中引入 GADT 与泛型编程等新构造，并以教程风格介绍 Makam 这一 λProlog 新实现。
We demonstrate how the framework of higher-order logic programming , as exemplified in the λProlog language design, is a prime vehicle for rapid prototyping of implementations for programming languages with sophisticated type systems. We present the literate development of a type checker for a language with a number of complicated features, culminating in a standard ML-style core with algebraic datatypes and type generalization, extended with staging constructs that are generic over a separately defined language of terms. We add each new feature in sequence, with little to no changes to existing code. Scaling the higher-order logic programming approach to this setting required us to develop approaches to challenges like complex variable binding patterns in object languages and performing generic structural traversals of code, making use of novel constructions in the setting of λProlog, such as GADTs and generic programming. For our development, we make use of Makam, a new implementation of λProlog, which we introduce in tutorial style as part of our (quasi-)literate development.
@article{paperbot296,
title = {Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam},
author = {Antonis Stampoulis and Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236788}
}