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

When Subtyping Constraints Liberate A Novel Type Inference Approach for first-class polymorphism

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2024年第POPL期8卷 1418-1450页

作者： Parreaux, Lionel Boruch-Gruszecki, Aleksander Fan, Andong Chau, Chun Yin HKUST Hong Kong Peoples R China Ecole Polytech Fed Lausanne Lausanne Switzerland

Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain open, such as how to type check expressions like (lambda x. (x 123, x True)) id reliably. We show that a type inference approach based on multi-bounded polymorphism, a form of implicit polymorphic subtyping with multiple lower and upper bounds, can help us resolve most of these problems in a uniquely simple and regular way. We define F-{<=}, a declarative type system derived from the existing theory of implicit coercions by Cretin and Remy (LICS 2014), and we introduce SuperF, a novel algorithm to infer polymorphic multi-bounded F-{<=} types while checking user type annotations written in the syntax of System F. We use a recursion-avoiding heuristic to guarantee termination of type inference at the cost of rejecting some valid programs, which thankfully rarely triggers in practice. We show that SuperF is vastly more powerful than all first-class-polymorphic type inference systems proposed so far, significantly advancing the state of the art in type inference for general-purpose programming languages.

关键词： type inference first-class polymorphism subtyping constraint solving

来源：评论

学校读者我要写书评

暂无评论

FreezeML Complete and Easy Type Inference for first-class polymorphism 2020

FreezeML Complete and Easy Type Inference for First-Class Po...

引用

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

作者： Emrich, Frank Lindley, Sam Stolarek, Jan Cheney, James Coates, Jonathan Univ Edinburgh Edinburgh Midlothian Scotland Imperial Coll London London England Lodz Univ Technol Lodz Poland Alan Turing Inst London England

ISBN: (纸本)9781450376136

ML is remarkable in providing statically typed polymorphism without the programmer ever having to write any type annotations. The cost of this parsimony is that the programmer is limited to a form of polymorphism in which quantifiers can occur only at the outermost level of a type and type variables can be instantiated only with monomorphic types. Type inference for unrestricted System F-style polymorphism is undecidable in general. Nevertheless, the literature abounds with a range of proposals to bridge the gap between ML and System F. We put forth a new proposal, FreezeML, a conservative extension of ML with two newfeatures. first, let- and lambda-binders may be annotated with arbitrary System F types. Second, variable occurrences may be frozen, explicitly disabling instantiation. FreezeML is equipped with type-preserving translations back and forth between System F and admits a type inference algorithm, an extension of algorithm W, that is sound and complete and which yields principal types.

关键词： first-class polymorphism type inference impredicative types

来源：评论

学校读者我要写书评

暂无评论

Constraint-Based Type Inference for FreezeML

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2022年第ICFP期6卷 570–595页

作者： Emrich, Frank Stolarek, Jan Cheney, James Lindley, Sam Lodz Univ Technol Lodz Poland Alan Turing Inst London England Univ Edinburgh Edinburgh Midlothian Scotland

FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to AlgorithmW. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/Remy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.

关键词： first-class polymorphism type inference impredicative types constraints

来源：评论

学校读者我要写书评

暂无评论

Seamless Scope-Safe Metaprogramming through Polymorphic Subtype Inference (Short Paper) 2024

Seamless Scope-Safe Metaprogramming through Polymorphic Subt...

引用

Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences

作者： Cunyuan Gao Lionel Parreaux Hong Kong University of Science and Technology Hong Kong China

ISBN: (纸本)9798400712111

Practical metaprogramming applications often involve manipulating open code fragments, which is easy to get wrong in the absence of static verification that all variable occurrences remain correctly bound. Many approaches have been proposed to verify the type- and scope-safety of metaprograms, but these approaches are either incomplete or cumbersome, imposing heavy type annotation or proof obligation burdens on metaprogrammers. In this short paper, we propose a new type system to statically keep track of the context requirements of code fragments. Our system uses a novel combination of Boolean-algebraic subtyping and first-class polymorphic type inference techniques to alleviate the annotation burden. The former provides the ability to encode scope requirements as unions of types and the latter allows these types to be locally quantified through a flexible form of polymorphic subtyping. We formalize this type system and demonstrate its implementation in the nascent MLscript functional and object-oriented programming language.

关键词： first-class polymorphism

来源：评论

学校读者我要写书评

暂无评论

ML^F Raising ML to the Power of System F

引用

ACM SIGPLAN NOTICES 2014年第4期49卷 52-63页

作者： Le Botlan, Didier Remy, Didier INRIA Rocquencourt F-78153 Le Chesnay France

We propose a type system MLF that generalizes ML with first-class polymorphism as in System F. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred. All expressions of ML are well-typed without any annotations. All expressions of System F can be mechanically encoded into MLF by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into MLF types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.

关键词： Type Inference first-class polymorphism Second-Order polymorphism System F ML Type Annotations

来源：评论

学校读者我要写书评

暂无评论

Flexible Types Robust type inference for first-class polymorphism 09

Flexible Types Robust type inference for first-class polymor...

引用

36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

作者： Leijen, Daan Microsoft Research Redmond WA USA

ISBN: (纸本)9781605583792

We present HML, a type inference system that supports full first-class polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be annotated. HML is a simplification of MLF where only flexibly quantified types are used. This makes the types easier to work with from a programmers perspective, and simplifies the implementation of the type inference algorithm. Still, HML retains much of the expressiveness of MLF, it is robust with respect to small program transformations, and has a simple specification of the type rules with an effective type inference algorithm that infers principal types. A small reference implementation with many examples is available at: http://***/users/daan/***.

关键词： Languages Design Theory first-class polymorphism System F MLF

来源：评论

学校读者我要写书评

暂无评论

HMF: Simple type inference for first-class polymorphism

引用

ACM SIGPLAN NOTICES 2008年第9期43卷 283-293页

作者： Leijen, Daan Microsoft Res Cambridge England

HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism. In contrast to other proposals, HML uses regular System F types and has a simple type inference algorithm that is just a small extension of the usual Damas-Milner algorithm W. Given the relative simplicity and expressive power, we feel that HMF can be an attractive type system in practice. There is a reference implementation of the type system available online together with a technical report containing proofs (Leijen 2007a,b).

关键词： languages design theory type inference first-class polymorphism

来源：评论

学校读者我要写书评

暂无评论

HMF: Simple Type Inference for first-class polymorphism

HMF: Simple Type Inference for First-Class Polymorphism

引用

13th ACM SIGPLAN International Conference on Functional Programming

作者： Leijen, Daan Microsoft Research

ISBN: (纸本)9781595939197

关键词： Type Inference first-class polymorphism

来源：评论

学校读者我要写书评

暂无评论

Recasting ML^F

引用

INFORMATION AND COMPUTATION 2009年第6期207卷 726-785页

作者： Le Botlan, Didier Remy, Didier INRIA Paris Rocquencourt F-78153 Le Chesnay France CNRS LAAS F-31077 Toulouse France Univ Toulouse UPS INSA INPISAELAAS F-31077 Toulouse France

The language MLF is a proposal for a new type system that supersedes both ML and System F, allows for efficient, predictable, and complete type inference for partially annotated terms. In this work, we revisit the definition of ML following a more progressive approach and focusing on the design-space and expressiveness. We introduce a Curry-style version iML(F) of MLF and provide an interpretation of iML(F) types as instantiation-closed sets of System-F types, from which we derive the definition of type-instance in iML(F) We give equivalent syntactic definition of the type-instance, presented as a set of inference rules. We also show an encoding of iML(F) into the closure of Curry-style System F by let-expansion. We derive the Church-style version eML(F) by refining types of iML(F) so as to distinguish between given and inferred polymorphism. We show an embedding of ML in eML(F) and a straightforward encoding of System F into eML(F). (C) 2009 Elsevier Inc. All rights reserved.

关键词： ML System F Type inference Type checking polymorphism first-class polymorphism

来源：评论

学校读者我要写书评

暂无评论

A type directed translation of MLF to system F

引用

ACM SIGPLAN NOTICES 2007年第9期42卷 111-122页

作者： Leijen, Daan Microsoft Research

The MLF type system by Le Botlan and Remy (2003) is a natural extension of Hindley-Milner type inference that supports full first-class polymorphism, where types can be of higher-rank and impredicatively instantiated. Even though MLF is theoretically very attractive, it has not seen widespread adoption. We believe that this partly because it is unclear how the rich language of MLF types relate to standard System F types. In this article we give the first type directed translation of MLF terms to System F terms. Based on insight gained from this translation, we also define "Rigid MLF" (MLF=), a restriction of MLF where all bound values have a System F type. The expressiveness of MLF= is the same as that of boxy types, but MLF= needs fewer annotations and we give a detailed comparison between them.

关键词： languages design theory first-class polymorphism system F MLF

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：