Reusability and Dependent Types

Robin Milner创造了一句口号：好类型的程序不能Gowrong，宣传了像Mland Haskell这样的类型函数式语言在使用类型捕获运行时错误方面的优势。如今，我们可以而且想要走得更远：依赖类型编程利用了非常有表现力的类型系统的能力来提供更强有力的保证，同时也为软件开发提供了额外的支持，使用类型来指导开发过程。最近，一大批旨在利用依赖类型的语言提案证明了这一点，例如Haskell with GADT，AGDA，Coq，Omega，Concoqtion，Guru，YNot，Eigram等等。然而，表达类型系统是有代价的：更具体的类型往往会降低代码的可重用性，其过于具体的实现类型可能不适合当前的应用。这种现象已经在ML和Haskell的传统Hindley-Milner样式系统中表现出来；在独立输入的环境中，它变得更加普遍。幸运的是，一切都没有失去：依赖类型的表现力足够强，以至于它们可以反思地谈论自己，这使得元编程成为其潜在的杀手应用程序之一，具有结合表达类型和可重用软件组件的潜力。基于并受到诺丁汉最近关于依赖类型编程(EPSRC/C512022/1)和容器类型(EPSRCEP/C511964/2)以及牛津关于数据类型泛型编程(EPSRCGR/S27078/01，EP/E02128X/1)的研究的启发，我们计划探索依赖类型在交付可重用和可靠软件组件方面的潜力。为了实现这一点，我们打算在依赖类型的框架中探索两种替代加载--通过结构实现的可重用性和通过设计实现的可重用性--以及表达。我们的计划是构建扩展Eigram 2框架的新工具，使用容器类型研究底层理论，最重要的是建立新的编程模式和库。我们为诺丁汉的RA(彼得·莫里斯的博士学位为这项提议奠定了大部分基础)和两名博士生(牛津大学和斯特拉斯克莱德大学各一名)寻求资金，并为准备、协调、旅行和分散工作(即一个工作坊和一个暑期学校)提供适当的支持。

Robin Milner coined the slogan well typed programs cannot gowrong , advertising the strength of typed functional languages like MLand Haskell in using types to catch runtime errors. Nowadays, we canand want to go further: dependently typed programming exploits thepower of very expressive type systems to deliver stronger guaranteesbut also additional support for software development, using types toguide the development process. This is witnessed by a recent surge oflanguage proposals with the goal to harness the power of dependenttypes, e.g. Haskell with GADTs, Agda, Coq, Omega, Concoqtion, Guru,Ynot, Epigram and so on.However, expressive type systems have their price: more specific typesfrequently reduce the reusability of code, whose too-specificimplementation type may not fit its current application. Thisphenomenon already shows up in the traditional Hindley-Milner styletype system of ML and Haskell; it becomes even more prevalent in adependently typed setting. Luckily, all is not lost: dependent typesare expressive enough that they can talk about themselvesreflectively, making meta-programming one of its potential killerapplications with the potential of combining expressive types andreusable software components.Based on and inspired by recent research at Nottingham on dependentlytyped programming (EPSRC EP/C512022/1) and container types (EPSRCEP/C511964/2) and at Oxford on datatype-generic programming (EPSRCGR/S27078/01, EP/E02128X/1) we plan to explore the potential ofdependent types to deliver reusable and reliable softwarecomponents. To achieve this, we intend to explore two alternativeroads - reusability by structure and reusability by design - andexpress both within a dependently typed framework. Our programme is tobuild new tools extending the Epigram 2 framework, investigate theunderlying theory using container types, and most importantlyestablish novel programming patterns and libraries. We seek fundingfor an RA at Nottingham (Peter Morris, whose PhD laid much of thegroundwork for this proposal), and two doctoral students (one each atOxford and Strathclyde), together with appropriate support forequipment, coordination, travel, and dissimination (i.e. a workshopand a summer school)