首页    期刊浏览 2024年12月11日 星期三
登录注册

文章基本信息

  • 标题:Refining Inductive Types
  • 本地全文:下载
  • 作者:Robert Atkey ; Patricia Johann ; Neil Ghani
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2012
  • 卷号:8
  • 期号:2
  • 页码:1
  • DOI:10.2168/LMCS-8(2:9)2012
  • 出版社:Technical University of Braunschweig
  • 摘要:Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists by their lengths. Other data types may be refined in similar ways, but programmers must produce purpose-specific refinements on an ad hoc basis, developers must anticipate which refinements to include in libraries, and implementations must often store redundant information about data and their refinements. In this paper we show how to generically derive inductive characterisations of refinements of inductive types, and argue that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. Our characterisations also ensure that standard techniques for programming with and reasoning about inductive types are applicable to refinements, and that refinements can themselves be further refined.
  • 其他关键词:inductive types, dependent types, category theory, fibrations, refinement types.
国家哲学社会科学文献中心版权所有