Reachability types: tracking aliasing and separation in higher-order functional programs

Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, λ * , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.

Download Full-text

A system of constructor classes: overloading and implicit higher-order polymorphism

Journal of Functional Programming ◽

10.1017/s0956796800001210 ◽

1995 ◽

Vol 5 (1) ◽

pp. 1-35 ◽

Cited By ~ 32

Author(s):

Mark P. Jones

Keyword(s):

Type System ◽

Type Systems ◽

Natural Generalization ◽

Higher Order ◽

Functional Language ◽

Effective Algorithm ◽

Prototype Implementation ◽

Type Classes

AbstractThis paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

Download Full-text

Functional programming with the FC++ library

Journal of Functional Programming ◽

10.1017/s0956796803004969 ◽

2004 ◽

Vol 14 (4) ◽

pp. 429-472 ◽

Cited By ~ 6

Author(s):

BRIAN MCNAMARA ◽

YANNIS SMARAGDAKIS

Keyword(s):

Data Structures ◽

Functional Programming ◽

Higher Order ◽

Performance Comparison ◽

Type Inference ◽

High Complexity ◽

Time Performance ◽

Order Of Magnitude ◽

Supporting Functional ◽

Higher Order Functions

We describe the FC++ library, a rich library supporting functional programming in C++. Prior approaches to encoding higher order functions in C++ have suffered with respect to polymorphic functions from either lack of expressiveness or high complexity. In contrast, FC++ offers full and concise support for higher-order polymorphic functions through a novel use of C++ type inference. The FC++ library has a number of useful features, including a generalized mechanism to implement currying in C++, a “lazy list” class which enables the creation of “infinite data structures”, a subtype polymorphism facility, and an extensive library of useful functions, including a large part of the Haskell Standard Prelude. The FC++ library has an efficient implementation. We show the results of a number of experiments which demonstrate the value of optimizations we have implemented. These optimizations have improved the run-time performance by about an order of magnitude for some benchmark programs that make heavy use of FC++ lazy lists. We also make an informal performance comparison with similar programs written in Haskell.

Download Full-text

Featherweight generic confinement

Journal of Functional Programming ◽

10.1017/s0956796806006125 ◽

2006 ◽

Vol 16 (6) ◽

pp. 793-811 ◽

Cited By ~ 7

Author(s):

ALEX POTANIN ◽

JAMES NOBLE ◽

DAVE CLARKE ◽

ROBERT BIDDLE

Keyword(s):

Programming Languages ◽

Ad Hoc ◽

Type System ◽

Type Systems ◽

General Purpose ◽

Ownership Type ◽

Essential Change ◽

Polymorphic Type ◽

Syntactic Restrictions

Existing approaches to object encapsulation either rely on ad hoc syntactic restrictions or require the use of specialised type systems. Syntactic restrictions are difficult to scale and to prove correct, while specialised type systems require extensive changes to programming languages. We demonstrate that confinement can be enforced cheaply in Featherweight Generic Java, with no essential change to the underlying language or type system. This result demonstrates that polymorphic type parameters can simultaneously act as ownership parameters and should facilitate the adoption of confinement and ownership type systems in general-purpose programming languages.

Download Full-text

A Complete Calculus of Monotone and Antitone Higher-Order Functions

10.29007/3n54 ◽

2018 ◽

Author(s):

Thomas Icard ◽

Lawrence Moss

Keyword(s):

Type System ◽

Lambda Calculus ◽

Higher Order ◽

Typed Lambda Calculus ◽

Higher Order Functions

This paper adds monotonicity and antitonicity information to the typed lambda calculus, thereby providing a foundation for the Monotonicity Calculus first developed by van Benthem and others. We establish properties of the type system, propose a syntax, semantics, and proof calculus, and prove completeness for the calculus with respect to hierarchies of monotone and antitone functions over base preorders.

Download Full-text

A Unified Type System for Object-Oriented Programming

DAIMI Report Series ◽

10.7146/dpb.v19i341.6571 ◽

1990 ◽

Vol 19 (341) ◽

Author(s):

Jens Palsberg ◽

Michael I. Schwartzbach

Keyword(s):

Type System ◽

Object Oriented ◽

Type Systems ◽

Object Oriented Programming ◽

Type Checking ◽

Separate Compilation ◽

Set Inclusion ◽

New Type ◽

Efficient Type ◽

Object Oriented Languages

We present a new type system for object-oriented languages with assignments. Types are sets of classes, subtyping is set inclusion, and genericity is class substitution. The type system enables separate compilation, and unifies, generalizes, and simplifies the type systems underlying SIMULA/BETA, C++, EIFFEL, and Typed Smalltalk, and the type system with type substitutions proposed by Palsberg and Schwartzbach, Classes and types are both modeled as node-labeled, ordered regular trees; this allows an efficient type-checking algorithm.

Download Full-text

Linearization of the lambda-calculus and its relation with intersection type systems

Journal of Functional Programming ◽

10.1017/s0956796803004970 ◽

2004 ◽

Vol 14 (5) ◽

pp. 519-546 ◽

Cited By ~ 5

Author(s):

MÁRIO FLORIDO ◽

LUÍS DAMAS

Keyword(s):

Programming Languages ◽

Functional Programming ◽

Type System ◽

Lambda Calculus ◽

Type Systems ◽

Functional Programming Languages

In this paper we present a notion of expansion of a term in the lambda-calculus which transforms terms into linear terms. This transformation replaces each occurrence of a variable in the original term by a fresh variable taking into account non-trivial implications in the structure of the term caused by these simple replacements. We prove that the class of terms which can be expanded is the same of terms typable in an Intersection Type System, i.e. the strongly normalizable terms. We then show that expansion is preserved by weak-head reduction, the reduction considered by functional programming languages.

Download Full-text

Elaborating intersection and union types

Journal of Functional Programming ◽

10.1017/s0956796813000270 ◽

2014 ◽

Vol 24 (2-3) ◽

pp. 133-165 ◽

Cited By ~ 11

Author(s):

JOSHUA DUNFIELD

Keyword(s):

Programming Languages ◽

Type System ◽

Type Systems ◽

Prototype Implementation ◽

Value Evaluation ◽

Source Program ◽

Parametric Polymorphism ◽

New Type ◽

Dynamic Typing ◽

System Feature

AbstractDesigning 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 onlyrefinement intersections, which increase the expressiveness of types (more precise properties can be checked) without altering the expressiveness of terms; refinement intersections can simply be erased during compilation. In contrast,unrestrictedintersections increase the expressiveness of terms, and can be used to encode diverse language features, promising an economy of both theory and implementation. We describe a foundation for compiling unrestricted intersection and union types: an elaboration type system that generates ordinary λ-calculus terms. The key feature is a Forsythe-like merge construct. With this construct, not all reductions of the source program preserve types; however, we prove that ordinary call-by-value evaluation of the elaborated program corresponds to a type-preserving evaluation of the source program. We also describe a prototype implementation and applications of unrestricted intersections and unions: records, operator overloading, and simulating dynamic typing.

Download Full-text

Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-72013-1_14 ◽

2021 ◽

pp. 262-280

Author(s):

Yuki Nishida ◽

Hiromasa Saito ◽

Ran Chen ◽

Akira Kawata ◽

Jun Furuse ◽

...

Keyword(s):

Type System ◽

Higher Order ◽

Smart Contracts ◽

Static Verification ◽

Smt Solver ◽

The Core ◽

Verification Conditions ◽

Refinement Types ◽

Characteristic Features ◽

Higher Order Functions

AbstractA smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them.This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

Download Full-text

Estimate the Memory Bounds Required by Shared Variables in Software Transactional Memory Programs

VNU Journal of Science Computer Science and Communication Engineering ◽

10.25073/2588-1086/vnucsce.280 ◽

2021 ◽

Vol 37 (2) ◽

Author(s):

Nguyen Ngoc Khai ◽

Truong Anh Hoang ◽

Dang Duc Hanh

Keyword(s):

Transactional Memory ◽

Type System ◽

Type Systems ◽

Research Topic ◽

Software Transactional Memory ◽

Loop Body ◽

Shared Variables ◽

New Type

Estimating memory required by complex programs is a well-known research topic. In this work, we build a type system to statically estimate the memory bounds required by shared variables in software transactional memory (STM) programs. This work extends our previous works with additional language features such as explicitly declared shared variables, introduction of primitive types, and allowing loop body to contain any statement, not required to be well-typed as in our previous works. Also, the new type system has better compositionality compared to available type systems.

Download Full-text

Relational nullable types with Boolean unification

Proceedings of the ACM on Programming Languages ◽

10.1145/3485487 ◽

2021 ◽

Vol 5 (OOPSLA) ◽

pp. 1-28

Author(s):

Magnus Madsen ◽

Jaco van de Pol

Keyword(s):

Open Source ◽

Programming Languages ◽

Type System ◽

Type Systems ◽

Type Inference ◽

System A ◽

Wide Range ◽

Programming Patterns ◽

Null Value ◽

Preliminary Study

We present a simple, practical, and expressive relational nullable type system. A relational nullable type system captures whether an expression may evaluate to null based on its type, but also based on the type of other related expressions. The type system extends the Hindley-Milner type system with Boolean constraints, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support full Hindley-Milner style type inference with an extension of Algorithm W. We conduct a preliminary study of open source projects showing that there is a need for relational nullable type systems across a wide range of programming languages. The most important findings from the study are: (i) programmers use programming patterns where the nullability of one expression depends on the nullability of other related expressions, (ii) such invariants are commonly enforced with run-time exceptions, and (iii) reasoning about these programming patterns requires not only knowledge of when an expression may evaluate to null, but also when it may evaluate to a non-null value. We incorporate these observations in the design of the proposed relational nullable type system.

Download Full-text