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

Extending the type checker of Standard ML by polymorphic recursion

THEORETICAL COMPUTER SCIENCE 1999年第1-2期212卷 157-181页

作者： Emms, M Leiss, H Univ Munich Ctr Informat & Sprachverarbeitung D-80538 Munich Germany

We describe an extension of the type inference of Standard ML that covers polymorphic recursion. For any term t of SML, a type scheme tau and a system L of inequations between (simple) types is computed, such that the types of t are the instances of tau by substitutions S that satisfy L. Both the inequation constraints L and their principal solutions are computed bottom-up in a modification of Milner's algorithm W. The correctness proof is complicated by the fact that (a) semiunification - unlike unification - generally does not allow one to refine a solution by composition with an arbitrary substitution and (b) a more restrictive criterion for introducing quantifiers in types of let-bound variables is needed. (C) 1999 Published by Elsevier Science B.V. All rights reserved.

关键词： functional programming type inference polymorphic recursion

来源：评论

学校读者我要写书评

暂无评论

TYPE RECONSTRUCTION IN THE PRESENCE OF polymorphic recursion

引用

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 1993年第2期15卷 290-311页

作者： KFOURY, AJ TIURYN, J URZYCZYN, P UNIV WARSAW INST MATHPL-00325 WARSAWPOLAND

We study the problem of type-checking functional programs in three extensions of ML. One distinguishing feature of these extensions is that they allow recursive definitions to be polymorphically typed. Although the motivation for these extensions comes from pragmatic considerations of programming language design, we show that the typability problem for each one of these extensions is polynomial-time equivalent to the Semi-Unification Problem and, therefore, undecidable.

关键词： LANGUAGES THEORY FIXPOINT OPERATOR polymorphic ABSTRACTION polymorphic recursion SEMIUNIFICATION

来源：评论

学校读者我要写书评

暂无评论

Programming Examples Needing polymorphic recursion

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年 136卷 57-102页

作者： Hallett, J. J. Kfoury, A. J. Boston Univ Dept Comp Sci Boston MA 02215 USA

Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic recursion using for all-types has been proved undecidable. This report presents several programming examples involving polymorphic recursion and determines their typability under various type systems, including the Hindley-Milner system, an intersection-type system, and extensions of these two. The goal of this report is to show that many of these examples are typable using a system of intersection types as an alternative form of polymorphism. By accomplishing this, we hope to lay the foundation for future research into a decidable intersection-type inference algorithm. We do not provide a comprehensive survey of type systems appropriate for polymorphic recursion, with or without type annotations inserted in the source language. Rather, we focus on examples for which types may be inferred without type annotations, with an emphasis on systems of intersectiontypes.

关键词： polymorphic recursion intersection types finitary polymorphism examples

来源：评论

学校读者我要写书评

暂无评论

The Simple Essence of Monomorphization

引用

Proceedings of the ACM on Programming Languages 2025年第OOPSLA1期9卷 1015-1041页

作者： Lutze, Matthew Schuster, Philipp Brachthäuser, Jonathan Immanuel Aarhus University Denmark University of Tübingen Germany

Monomorphization is a common implementation technique for parametric type-polymorphism, which avoids the potential runtime overhead of uniform representations at the cost of code duplication. While important as a folklore implementation technique, there is a lack of general formal treatments in the published literature. Moreover, it is commonly believed to be incompatible with higher-rank polymorphism. In this paper, we formally present a simple monomorphization technique based on a type-based flow analysis that generalizes to programs with higher-rank types, existential types, and arbitrary combinations. Inspired by algebraic subtyping, we track the flow of type instantiations through the program. Our approach only supports monomorphization up to polymorphic recursion, which we uniformly detect as cyclic flow. Treating universal and existential quantification uniformly, we identify a novel form of polymorphic recursion in the presence of existential types, which we coin polymorphic packing. We study the meta-theory of our approach, showing that our translation is type-preserving and preserves semantics step-wise. © 2025 Copyright held by the owner/author(s).

关键词： existential types higher-rank types monomorphization polymorphic packing polymorphic recursion

来源：评论

学校读者我要写书评

暂无评论

SEMIUNIFICATION OF 2 TERMS IN ABELIAN-GROUPS

引用

INFORMATION PROCESSING LETTERS 1994年第2期52卷 61-68页

作者： RITTRI, M Department of Computing Science Chalmers University of Technology S-412 96 G&ouml teborg Sweden

A substitution sigma AG-semi-unifies the inequation s less than or equal to(AG)(?) t iff there is another substitution rho such that rho(sigma(s)) =(AG) sigma(t), where =(AG) is equality in Abelian groups. We give an algorithm that decides if an equation has an AG-semi-unifer and, if so, returns a most general one. This is a first step towards type derivation in programming languages with dimension types and polymorphic recursion.

关键词： ALGORITHMS ABELIAN GROUPS EQUATIONAL SEMIUNIFICATION PROGRAMMING LANGUAGES COMPILERS DIMENSION TYPES polymorphic recursion

来源：评论

学校读者我要写书评

暂无评论

Rank 2 intersection for recursive definitions

引用

FUNDAMENTA INFORMATICAE 2007年第4期77卷 451-488页

作者： Damiani, Ferruccio Univ Turin Dipartimento Informat I-10149 Turin Italy

Let proves be an intersection type system. We say that a term is proves-simple (or just simple when the system proves is clear from the context) if system proves can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank 2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (non-simple) recursive definitions have been already proposed in the literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x = e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank 2 intersection, so they can be applied to other type systems.

关键词： type inference principal typings polymorphic recursion

来源：评论

学校读者我要写书评

暂无评论

Rank 2 intersection types for local definitions and conditional expressions

引用

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 2003年第4期25卷 401-451页

作者： Damiani, F Univ Turin Dipartimento Informat I-10149 Turin Italy

We propose a rank 2 intersection type system with new typing rules for local definitions (let-expressions and letrec-expressions) and conditional expressions (if-expressions and match-expressions). This is a further step towards the use of intersection types in "real" programming languages. The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 intersection), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to "limit the use" of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might also be useful for other type systems.

关键词： algorithms theory languages type inference principal typings polymorphic recursion

来源：评论

学校读者我要写书评

暂无评论

Deriving a complete type inference for Hindley-Milner and vector sizes using expansion

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年第Part2期95卷 254-271页

作者： Simon, Axel Tech Univ Munich Garching Germany

Type inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract interpretation. We observe that completeness results in the abstract interpretation literature can be used to derive type inferences that are backward complete, implying that type annotations cannot improve the result of type inference, thus making type annotations optional. The resulting algorithm is similar to that of Milner-Mycroft, that is, it infers Hindley-Milner types while allowing for polymorphic recursion. Although undecidable, we present a practical check that reliably distinguishes typeable from untypeable programs.,Instead of type schemes, we use expansion to instantiate types. Since our expansion operator is agnostic to the abstract domain, we are able to apply it not only to types. We illustrate this by inferring the size of vector types using systems of linear equalities and present practical uses of polymorphic recursion using vector types. (C) 2014 Elsevier B.V. All rights reserved.

关键词： Type inference Completeness Abstract interpretation polymorphic recursion Vector size inference

来源：评论

学校读者我要写书评

暂无评论

Disciplined, efficient, generalised folds for nested datatypes

引用

FORMAL ASPECTS OF COMPUTING 2004年第1期16卷 19-35页

作者： Martin, C Gibbons, J Bayley, I Oxford Brookes Univ Sch Comp & Math Sci Oxford OX33 1HX England Univ Oxford Comp Lab Oxford OX1 3QD England

Nested (or non-uniform, or non-regular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson introduced generalised folds for extra power, but at the cost of a loss of efficiency: folds may take more than linear time to evaluate. Hinze introduced efficient generalised folds to counter this inefficiency, but did so in a pragmatic way: he did not provide categorical or equivalent underpinnings, so did not get the associated universal properties for manipulating folds. We combine the efficiency of Hinze's construction with the powerful reasoning tools of Bird and Paterson's.

关键词： fold functor category nested datatype non-regular datatype non-uniform datatype polymorphic recursion universal property

来源：评论

学校读者我要写书评

暂无评论

Efficient implementation of run-time generic types for Java

引用

IFIP TC2/WG 2 1 Working Conference on Generic Programming

作者： Allen, E Cartwright, R Stoler, B Rice Univ Houston TX 77005 USA

ISBN: (纸本)1402073747

We describe an efficient compiler and run-time system for NEXTGEN, a compatible extension of the Java programming language supporting run-time generic types designed by Cartwright and Steele. The resulting system is comparable in performance with both standard Java and the GJ extension of Java, which does not support run-time generic types. Our implementation of NEXTGEN consists of a compiler extending the GJ compiler and a special class loader that constructs type instantiation classes on demand. The compiler relies on the implementation strategy proposed by Cartwright and Steele with one major exception: to support polymorphic recursion in the definition of generic classes, the compiler generates templates for instantiation classes which are constructed on demand by the class loader. We include an extensive set of benchmarks, specifically developed to stress the use of generic types. The benchmarks a show that the additional code required to support run-time generic types has little overhead compared with ordinary Java and GJ.

关键词： Java GJ NextGen generic types type dependent operation JVM extensions compatibility specification design implementation class loader reflection erasure performance benchmarks run-time object-oriented programming parametric polymorphism polymorphic recursion PolyJ C#

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：