CCF-SHF Small: Beyond Algebraic Data Types: Combinatorial Species and Mathematically-Structured Programming

点击翻译按钮获取中文摘要

At the heart of any computer program is the data that the program is designed to manipulate. Data, in turn, is only useful when organized into some sort of structure ---be it as simple as a list or as complex as a network or hierarchical tree. The mathematical theory of "combinatorial species" studies many variations of such structure, but it has not often been applied in a computer science context. The goal of this project is a new understanding of data structure through the abstractions of combinatorial species. This understanding will lead to new classes of data structures as well as practical tools for working with existing ones. Ultimately, this work will lead to more expressive programming languages, allowing computer programs to be written at a higher level and with fewer errors.More specifically, the project seeks to extend the existing computational theory of algebraic data types with constructs derived from the theory of combinatorial species. In particular, the project will explore the specification of data types with nontrivial symmetries and sharing, such as cycles, bags, and simple graphs. The project will develop libraries and language extensions to support the use of species data types in the Haskell programming language. As a significant test case, it will explore the application of species data types to property-based testing. Although the work is to be carried out in the context of the Haskell programming language, the results will be applicable to any language, including those with direct support for algebraic datatypes (such as OCaml, F#, Racket or Scala), and those without. All libraries and tools developed under this project will be made available as open source.