scholarly journals On the adequacy of representing higher order intuitionistic logic as a pure type system

1992 ◽  
Vol 57 (3) ◽  
pp. 251-276 ◽  
Author(s):  
Hans Tonino ◽  
Ken-etsu Fujita
Keyword(s):  
Intuitionistic Logic ◽  
Type System ◽  
Higher Order ◽  
Pure Type

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

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
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.

scholarly journals Pure Type System conversion is always typable

2012 ◽  
Vol 22 (2) ◽  
pp. 153-180 ◽  
Author(s):  
VINCENT SILES ◽  
HUGO HERBELIN
Keyword(s):  
Type System ◽  
Type Systems ◽  
Positive Answer ◽  
General Question ◽  
Pure Type ◽  
Typing System ◽  
Long Time ◽  
Pure Type Systems

AbstractPure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class ofPure Type Systems(PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.

scholarly journals Trust in the λ-calculus

1997 ◽  
Vol 7 (6) ◽  
pp. 557-591 ◽  
Author(s):  
P. ØRBÆK ◽  
J. PALSBERG
Keyword(s):  
Type System ◽  
Higher Order ◽  
Type Inference ◽  
Reduction Property ◽  
The Subject ◽  
Run Time ◽  
Trust Information

This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a confluent λ-calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information is presented as annotations of the underlying Curry types, and type inference is computable in O(n3) time.

scholarly journals 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.

scholarly journals A framework for improving error messages in dependently-typed languages

2019 ◽  
Vol 9 (1) ◽  
pp. 1-32 ◽  
Author(s):  
Joseph Eremondi ◽  
Wouter Swierstra ◽  
Jurriaan Hage
Keyword(s):  
Programming Languages ◽  
Type System ◽  
Higher Order ◽  
Type Checking ◽  
Unification Algorithm ◽  
Implicit Arguments ◽  
Unification Problem ◽  
Heuristic Analysis ◽  
Type Check ◽  
Typed Languages

AbstractDependently-typed programming languages provide a powerful tool for establishing code correctness. However, it can be hard for newcomers to learn how to employ the advanced type system of such languages effectively. For simply-typed languages, several techniques have been devised to generate helpful error messages and suggestions for the programmer. We adapt these techniques to dependently-typed languages, to facilitate their more widespread adoption. In particular, we modify a higher-order unification algorithm that is used to resolve and type-check implicit arguments. We augment this algorithm with replay graphs, allowing for a global heuristic analysis of a unification problem-set, error-tolerant typing, which allows type-checking to continue after errors are found, and counter-factual unification, which makes error messages less affected by the order in which types are checked. A formalization of our algorithm is presented with an outline of its correctness. We implement replay graphs, and compare the generated error messages to those from existing languages, highlighting the improvements we achieved.

scholarly journals Eventually Periodic Solutions of a Max-Type System of Difference Equations of Higher Order

2018 ◽  
Vol 2018 ◽  
pp. 1-6 ◽  
Author(s):  
Guangwang Su ◽  
Taixiang Sun ◽  
Bin Qin
Keyword(s):  
Periodic Solutions ◽  
Difference Equations ◽  
Initial Conditions ◽  
Type System ◽  
Higher Order ◽  
System Of Difference Equations

We study in this paper the following max-type system of difference equations of higher order: xn=max{A,yn-k/xn-1} and yn=max{B,xn-k/yn-1}, n∈{0,1,2,…}, where A≥B>0, k≥1, and the initial conditions x-k,y-k,x-k+1,y-k+1,…,x-1,y-1∈(0,+∞). We show that (1) if AB>1, then every solution of the above system is periodic with period 2 eventually. (2) If AB=1>B, then every solution of the above system is periodic with period 2k or 2 eventually. (3) If A=B=1 or AB<1, then the above system has a solution which is not periodic eventually.

Typing and subtyping for mobile processes

1996 ◽  
Vol 6 (5) ◽  
pp. 409-453 ◽  
Author(s):  
Benjamin Pierce ◽  
Davide Sangiorgi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Type System ◽  
Higher Order ◽  
Order Process ◽  
Process Calculi ◽  
Mobile Processes

The π-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner's presentation of the π-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed λ-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the π-calculus. These can be used, for example, to obtain the validity of β-reduction for the more efficient of Milner's encodings of the call-by-value λ-calculus, which fails in the ordinary π-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner's λ-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.

Sign in / Sign up

Export Citation Format

Share Document