检索结果-内蒙古大学图书馆

Refinement Kinds type-Safe Programming with Practical type-level computation

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2019年第OOPSLA期3卷 1–30页

作者： Caires, Luis Toninho, Bernardo Univ Nova Lisboa NOVA LINCS FCT NOVA Dept Informat Lisbon Portugal

This work introduces the novel concept of kind refinement, which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles expressed by predicates over values in the type domain, kind refinements provide rich kind specifications by means of predicates over types in the kind domain. By leveraging our powerful refinement kind discipline, types in our language are not just used to statically classify program expressions and values, but also conveniently manipulated as tree-like data structures, with their kinds refined by logical constraints on such structures. Remarkably, the resulting typing and kinding disciplines allow for powerful forms of type reflection, ad-hoc polymorphism and type-directed meta-programming, which are often found in modern software development, but not typically expressible in a type-safe manner in general purpose languages. We validate our approach both formally and pragmatically by establishing the standard meta-theoretical results of type safety and via a prototype implementation of a kind checker, type checker and interpreter for our language.

关键词： Refinement Kinds typed Meta-Programming type-level computation type Theory

来源：评论

学校读者我要写书评

暂无评论

Constrained type Families

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2017年第ICFP期1卷 1-28页

作者： Morris, J. Garrett Eisenberg, Richard A. Univ Edinburgh Edinburgh Midlothian Scotland Univ Kansas Lawrence KS 66045 USA Bryn Mawr Coll Bryn Mawr PA 19010 USA

We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.

关键词： type families type-level computation type classes Haskell

来源：评论

学校读者我要写书评

暂无评论

Well-typed Music Does Not Sound Wrong 10

Well-Typed Music Does Not Sound Wrong

引用

10th ACM SIGPLAN Symposium on Haskell (Haskell) co-located with ICFP Conference

作者： Szamozvancev, Dmitrij Gale, Michael B. Univ Cambridge Cambridge England Univ Warwick Coventry W Midlands England

ISBN: (纸本)9781450351829

Music description and generation are popular use cases for Haskell, ranging from live coding libraries to automatic harmonisation systems. Some approaches use probabilistic methods, others build on the theory of Western music composition, but there has been little work done on checking the correctness of musical pieces in terms of voice leading, harmony, and structure. Haskell's recent additions to the type-system now enable us to perform such analysis statically. We present our experience of implementing a type-level model of classical music and an accompanying EDSL which enforce the rules of classical music at compile-time, turning composition mistakes into compiler errors. Along the way, we discuss the strengths and limitations of doing this in Haskell and demonstrate that the type system of the language is fully capable of expressing non-trivial and practical logic specific to a particular domain.

关键词： type-level computation Haskell music theory

来源：评论

学校读者我要写书评

暂无评论

Experience Report: type-checking Polymorphic Units for Astrophysics Research in Haskell

引用

ACM SIGPLAN NOTICES 2014年第12期49卷 31-38页

作者： Muranushi, Takayuki Eiscnberg, Richard A. Kyoto Univ Hakubi Ctr Adv Res Kyoto 6068501 Japan Univ Penn Philadelphia PA 19104 USA

Many of the bugs in scientific programs have their roots in mistreatment of physical dimensions, via erroneous expressions in the quantity calculus. Now that the type system in the Glasgow Haskell Compiler is rich enough to support type-level integers and other promoted datatypes, we can type-check the quantity calculus in Haskell. In addition to basic dimension-aware arithmetic and unit conversions, our units library features an extensible system of dimensions and units, a notion of dimensions apart from that of units, and unit polymorphism designed to describe the laws of physics. We demonstrate the utility of units by writing an astrophysics research paper. This work is free of unit concerns because every quantity expression in the paper is rigorously type-checked.

关键词： type families type-level computation Haskell quantity calculus

来源：评论

学校读者我要写书评

暂无评论

Closed type Families with Overlapping Equations 14

Closed Type Families with Overlapping Equations

引用

41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

作者： Eisenberg, Richard A. Vytiniotis, Dimitrios Jones, Simon Peyton Weirich, Stephanie Univ Penn Philadelphia PA 19104 USA Microsoft Res Cambridge Cambridge England

ISBN: (纸本)9781450325448

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.

关键词： Design Languages Theory type families type-level computation Haskell System FC

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：