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

A constraint-based approach to guarded algebraic data types

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 2007年第1期29卷 A1-A56页

作者： Simonet, Vincent Pottier, Francois INRIA F-78153 Le Chesnay France

We study HMG(X), an extension of the constraint-based type system HM(X) with deep pattern matching, polymorphic recursion, and guarded algebraic data types. Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, (first-class) phantom types, and equality qualified types, and are closely related to inductive types. Their characteristic property is to allow every branch of a case construct to be typechecked under different assumptions about the type variables in scope. We prove that HMG( X) is sound and that, provided recursive definitions carry a type annotation, type inference can be reduced to constraint solving. constraint solving is decidable, at least for some instances of X, but prohibitively expensive. Effective type inference for guarded algebraic data types is left as an issue for future research.

关键词： languages theory generalized algebraic data types GADTs constraint-based type inference

来源：评论

学校读者我要写书评

暂无评论

Skalpel: A constraint-based type error slicer for Standard ML

引用

JOURNAL OF SYMBOLIC COMPUTATION 2017年第Part1期80卷 164-208页

作者： Rahli, Vincent Wells, Joe Pirie, John Kamareddine, Fairouz Univ Luxembourg SnT Luxembourg Luxembourg Heriot Watt Univ Edinburgh Midlothian Scotland

Compilers for languages with type inference algorithms often produce confusing type error messages and give a single error location which is sometimes far away from the real location of the error. Attempts at solving this problem often (1) fail to include the multiple program points which make up the type error;(2) report tree fragments which do not correspond to any place in the user program;and (3) give incorrect type information/diagnosis which can be highly confusing. We present Skalpel, a type error slicing tool which solves these problems by giving the programmer all and only the information involved with a type error to significantly aid in diagnosis and repair of type errors. Skalpel relies on a simple and general constraint system, a sophisticated constraint generator which is linear in program size, and a constraint solver which is terminating. Skalpel's constraint system can elegantly and efficiently handle intricate features such as SML's open. We also show that the Skalpel tool is general enough to deal not only with one source code file and one single error, but highlights all and only the possible locations of the error(s) in all affected files and produces all the culprit multiple program slices. (C) 2016 Elsevier Ltd. All rights reserved.

关键词： constraint-based type inference Automated type inference Automated error diagnosis type error slicing Improved error reports

来源：评论

学校读者我要写书评

暂无评论

A compiler architecture for domain-specific type error diagnosis

引用

OPEN COMPUTER SCIENCE 2019年第1期9卷 33-51页

作者： Serrano, Alejandro Hage, Jurriaan Univ Utrecht Utrecht Netherlands

Domain-specific languages (DSLs) permeate current programming practices. An important kind of DSLs includes those developed and integrated within a host language, which we call embedded or internal DSLs. Unfortunately, embedded DSLs usually fall short on domain-specific error diagnosis, that is, they do not give control to DSL authors over how errors are reported to the programmer. As a consequence, implementation details of the DSL leak through in error messages, and programmers need to understand the internals of the DSL implementation to fix their code in a productive way. This paper addresses the challenge of building a compiler with integrated support for domain-specific error diagnosis. We assume that the type system is described using a constraint-based approach, and constraint solving is specified using rewrite rules. Domain information can then be injected at constraint gathering time via type rules, during constraint solving via specialized rules and axioms, and finally at blaming and reparation time via transformations. Furthermore, we define error contexts as a way to control the order in which solving and blaming proceeds. We engineer domain-specific error diagnosis in such a way that the compiler can also reuse the techniques for improving general error diagnosis.

关键词： domain-specific languages type error diagnosis constraint-based type inference

来源：评论

学校读者我要写书评

暂无评论

type inference for first-class messages with feature constraints 4th

Type inference for first-class messages with feature constra...

引用

4th Asian Computing Science Conference (ASIAN 98)

作者： Müller, M Nishimura, S Univ Saarland D-66041 Saarbrucken Germany Kyoto Univ Rims Sakyo Ku Kyoto 6068502 Japan

ISBN: (纸本)3540653880

We present a constraint system OF of feature trees that is appropriate to specify and implement type inference for first-class messages. OF extends traditional systems of feature constraints by a selection constraint x(y)z "by first-class feature tree" y, in contrast to the standard selection constraint x[f]y "by fixed feature" f. We investigate the satisfiability problem of OF and show that it can be solved in polynomial time, and even in quadratic time in an important special case. We compare OF with Treinen's constraint system EF of feature constraints with first-class features, which has an NP-complete satisfiability problem. This comparison yields that the satisfiability problem for OF with negation is NP-hard. based on OF we give a simple account of type inference for first-class messages in the spirit of Nishimura's recent proposal, and we show that it has polynomial time complexity: We also highlight an immediate extension,that is desirable but makes type inference NP-hard.

关键词： object-oriented programming first-class messages constraint-based type inference complexity feature constraints

来源：评论

学校读者我要写书评

暂无评论

An extension of HM(X) with bounded existential and universal data-types 03

An extension of HM(X) with bounded existential and universal...

引用

8th International Conference on Functional Programming (ICFP 03)

作者： Simonet, V INRIA Rocquencourt Rocquencourt France

ISBN: (纸本)9781581137569

We propose a conservative extension of HM(X), a generic constraint-based type inference framework, with bounded existential (a.k.a. abstract) and universal (a.k.a. polymorphic) data-types. In the first part of the article, which remains abstract of the type and constraint language (i.e. the logic X), we introduce the type system, prove its safety and define a type inference algorithm which computes principal typing judgments. In the second part, we propose a realistic constraint solving algorithm for the case of structural subtyping, which handles the non-standard construct of the constraint language generated by type inference: a form of bounded universal quantification.

关键词： constraint-based type inference existential and universal data-types structural subtyping

来源：评论

学校读者我要写书评

暂无评论

type inference FOR FIRST-CLASS MESSAGES WITH FEATURE constraintS

引用

International Journal of Foundations of Computer Science 2000年第1期11卷 29-63页

作者： MARTIN MÜLLER SUSUMU NISHIMURA Universität des Saarlandes Programming Systems Lab 66041 Saarbrücken Germany Partly supported by the Deutsche Forschungsgemeinschaft (DFG) through Sonderforschungsbereich 378 at the Universität des Saarlandes Saarbrücken 1996-98. RIMS Kyoto University Sakyo-ku Kyoto 606-8502 Japan Partly supported by the Japanese Ministry of Education Science Sports and Culture Grant-in-Aid for Encouragement of Young Scientists 10780187 1998.

We present a constraint system, OF, of feature trees that is appropriate to specify and implement type inference for first-class messages. OF extends traditional systems of feature constraints by a selection constraint x z, "by first-class feature tree" y, which is in contrast to the standard selection constraint x[f]y, "by fixed feature" f. We investigate the satisfiability problem of OF and show that it can be solved in polynomial time, and even in quadratic time if the number of features is bounded. We compare OF with Treinen's system EF of feature constraints with first-class features, which has an NP-complete satisfiability problem. This comparison yields that the satisfiability problem for OF with negation is NP-hard. Further we obtain NP-completeness, for a specific subclass of OF with negation that is useful for a related type inference problem. based on OF we give a simple account of type inference for first-class messages in the spirit of Nishimura's recent proposal, and we show that it has polynomial time complexity: We also highlight an immediate extension of this type system that appears to be desirable but makes type inference NP-complete.

关键词： object-oriented programming first-class messages constraint-based type inference complexity feature constraints

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：