COALGEBRAIC LOGIC PROGRAMMING FOR TYPE INFERENCE: Parallelism and Corecursion for New Generation of Programming Languages

输入的主要目的是防止在程序运行期间发生执行错误。米尔纳将这一想法形式化，表明“良好类型的程序不会出错”。实际上，类型结构提供了一种减少程序员错误的基本技术。在最强大的情况下，它们涵盖了验证社区感兴趣的大多数属性。函数式语言发展的一个主要趋势是改进底层类型系统的表达性，例如，依赖类型、类型类、广义代数类型（gadt）、依赖类型类和规范结构。米尔纳风格的可确定类型推断并不总是满足于这样的扩展（例如，主体类型可能不再存在），并且确定良好类型有时需要在编译时类型推断之外进行额外的计算。新型推理算法的实现包括各种一阶决策过程，特别是统一和逻辑规划（LP），约束LP，嵌入到交互策略中的LP (Coq的eauto)，以及通过重写补充的LP。最近，Gonthier等人提出了一个强有力的主张，即对于更丰富的类型系统，lp风格的类型推断比传统的策略驱动的证明开发更有效和自然。第二个主要趋势是并行性：没有副作用使得并行计算子表达式变得容易。函数组合和高阶函数的强大抽象机制在并行化中起着重要作用。三种主要的并行语言是Eden（显式并行）parallel ML（隐式并行）和Glasgow parallel Haskell（半显式并行）。控制并行性特别区别于函数式语言。在文献中，类型推理和并行性很少被同时考虑。随着类型推断变得越来越复杂，并在整个程序开发中发挥更大的作用，顺序类型推断必然成为语言并行化的瓶颈。我们的新共代数逻辑规划（CoALP）在一个算法中提供了额外的表达性（共递归）和并行性。我们建议使用CoALP来代替目前在类型推断中使用的LP工具。随着上面提到的共递、并行和类型（函数式）编程的主要发展，这些脱节的社区将他们的努力结合起来变得至关重要：丰富的类型理论越来越依赖于新一代的LP语言；协代数语义在语言设计中具有重要的影响；和并行语言的方言在跨FP/LP编程范式应用通用技术方面具有巨大的潜力。这个项目的独特之处在于，它汇集了在这三个社区工作的本地和国际合作者。该项目支持者的数量比我们议程的及时性更能说明问题。该项目将影响EPSRC战略计划的两个流：“编程语言和编译器”和“验证和正确性”。该项目在理论方面是新颖的（自动证明搜索中出现的（co）递归计算的共代数研究）；实践（新语言CoALP的实现及其在类型推断工具中的嵌入）和方法论（混合共递和并行）。

The main goal of typing is to prevent the occurrence of execution errors during the running of a program. Milner formalised the idea, showing that ``well-typed programs cannot go wrong''. In practice, type structures provide a fundamental technique of reducing programmer errors. At their strongest, they cover most of the properties of interest to the verification community.A major trend in the development of functional languages is improvement in expressiveness of the underlying type system, e.g., in terms of Dependent Types, Type Classes, Generalised Algebraic Types (GADTs), Dependent Type Classes and Canonical Structures. Milner-style decidable type inference does not always suffice for such extensions (e.g. the principal type may no longer exist), and deciding well-typedness sometimes requires computation additional to compile-time type inference.Implementations of new type inference algorithms include a variety of first-order decision procedures, notably Unification and Logic Programming (LP), Constraint LP, LP embedded into interactive tactics (Coq's eauto), and LP supplemented by rewriting.Recently, a strong claim has been made by Gonthier et al that, for richer type systems, LP-style type inference is more efficient and natural than traditional tactic-driven proof development.A second major trend is parallelism: the absence of side-effects makes it easy to evaluate sub-expressions in parallel. Powerful abstraction mechanisms of function composition and higher-order functions play important roles in parallelisation. Three major parallel languages are Eden (explicit parallelism) Parallel ML (implicit parallelism) and Glasgow parallel Haskell (semi-explicit parallelism). Control parallelism in particular distinguishes functional languages.Type inference and parallelism are rarely considered together in the literature. As type inference becomes more sophisticated and takes a bigger role in the overall program development, sequential type inference is bound to become a bottle-neck for language parallelisation.Our new Coalgebraic Logic Programming (CoALP) offers both extra expressiveness (corecursion) and parallelism in one algorithm. We propose to use CoALP in place of LP tools currently used in type inference.With the mentioned major developments in Corecursion, Parallelism, and Typeful (functional) programming it has become vital for these disjoint communities to combine their efforts: enriched type theories rely more and more on the new generation of LP languages; coalgebraic semantics has become influential in language design; and parallel dialects of languages have huge potential in applying common techniques across the FP/LP programming paradigm. This project is unique in bringing together local and international collaborators working in the three communities. The number ofsupporters the project has speaks better than words about the timeliness of our agenda.The project will impact on two streams of EPSRC's strategic plan: "Programming Languages and Compilers" and "Verification and Correctness". The project is novel in aspects of Theory (coalgebraic study of (co)recursive computations arising in automated proof-search); Practice (implementation of the new language CoALP and its embedding in type-inference tools); and Methodology (Mixed corecursion and parallelism).