首页/论文/2011.03076

arXiv 2011.030762020-11cs.PLcs.LO

Towards a more perfect union type

Michał J. Gajda

DOI：: 10.5281/zenodo.3929474

英文摘要：

We present a principled theoretical framework for inferring and checking the union types, and show its work in practice on JSON data structures. The framework poses a union type inference as a learning problem from multiple examples. The categorical framework is generic and easily extensible.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Intersections and Unions of Session Types

Prior work has extended the deep, logical connection between the linear sequent calculus and session-typed message-passing concurrent computation with equi-recursive types and a natural notion of subtyping. In this paper, we extend this further by intersection and union types in order to express multiple behavioral properties of processes in a single type. We prove session fidelity and absence of deadlock and illustrate the expressive power of our system with some simple examples. We observe that we can represent internal and external choice by intersection and union, respectively, which was p…

2017-02-08cs.LOcs.PL

Untangling Typechecking of Intersections and Unions

Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics. Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into…

2011-01-24cs.PL

Session Types = Intersection Types + Union Types

We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories. In particular, intersections and unions provide a native solution to the problem of computing joins and meets of session types. Also, the subtyping relation turns out to be a pre-congruence, while this is not always the case in related behavioral theories.

2011-01-24cs.DCcs.PL

A Type Checker for a Logical Framework with Union and Intersection Types

We present the syntax, semantics, and typing rules of Bull, a prototype theorem prover based on the Delta-Framework, i.e. a fully-typed lambda-calculus decorated with union and intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type Theory Xi of Barbanera-Dezani-de'Liguoro. Bull has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or norm…

2020-02-25cs.LOcs.PL

Improving Precision of Type Analysis Using Non-Discriminative Union

This paper presents a new type analysis for logic programs. The analysis is performed with a priori type definitions; and type expressions are formed from a fixed alphabet of type constructors. Non-discriminative union is used to join type information from different sources without loss of precision. An operation that is performed repeatedly during an analysis is to detect if a fixpoint has been reached. This is reduced to checking the emptiness of types. Due to the use of non-discriminative union, the fundamental problem of checking the emptiness of types is more complex in the proposed type …

2006-12-12cs.PL

Union and intersection contracts are hard, actually

Union and intersection types are a staple of gradually typed language such as TypeScript. While it's long been recognized that union and intersection types are difficult to verify statically, it may appear at first that the dynamic part of gradual typing is actually pretty simple. It turns out however, that in presence of higher-order contracts union and intersection are deceptively difficult. The literature on higher-order contracts with union and intersection, while keenly aware of the fact, doesn't really explain why. We point and illustrate the problems and trade-offs inherent to union and…

2022-03-31cs.PL

更多相关论文收起更多论文

Decidable Tag-Based Semantic Subtyping for Nominal Types, Tuples, and Unions

Semantic subtyping enables simple, set-theoretical reasoning about types by interpreting a type as the set of its values. Previously, semantic subtyping has been studied primarily in the context of statically typed languages with structural typing. In this paper, we explore the applicability of semantic subtyping in the context of a dynamic language with nominal types. Instead of static type checking, dynamic languages rely on run-time checking of type tags associated with values, so we propose using the tags for semantic subtyping. We base our work on a fragment of the Julia language and pres…

2019-12-17cs.PL

Elaborating Intersection and Union Types

Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume many different features. In modern type systems, parametric polymorphism is fundamental, but intersection polymorphism has gained little traction in programming languages. Most practical intersection type systems have supported only refinement intersections, which increase the expressiveness of types (more precise properties can b…

2020-08-15cs.PL

使用联合、交集和否定类型进行编程

Programming with union, intersection, and negation types

本文阐述了集合论类型（联合、交集、否定）在编程中的优势，通过语义子类型理论及其扩展，提出并实现了三种有效的语言系统限制，以精确支持分支、模式匹配和函数重载等语言构造的类型化。

2024-03-27cs.PL

Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics

We propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract the contents of compound variables in a field-sensitive way, whether these fields contain numeric or pointer values, and use stock numerical abstract domains to find an overapproximation of all possible memory states--with the ability to discover relationships between variables. A main novelty of our approach is the dynamic mapping scheme we use t…

2007-03-16cs.PL

动态语言的 polymorphic 类型推断

Polymorphic Type Inference for Dynamic Languages

本文提出一种结合一阶多态性、交集/并集类型及子类型的类型系统，并设计可靠且可终止的类型重构算法，使未标注函数获得多态类型以表达重载行为，适用于动态语言类型化。

2023-11-17cs.PL