scholarly journals On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control

2019 ◽  
Vol 29 ◽  
Author(s):  
YANNICK FORSTER ◽  
OHAD KAMMAR ◽  
SAM LINDLEY ◽  
MATIJA PRETNAR
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Denotational Semantics ◽  
Expressive Power ◽  
Programming Abstractions ◽  
Programming Abstraction ◽  
Natural Type ◽  
Inductive Types

AbstractWe compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.

scholarly journals Annotated Type Systems for Program Analysis

1995 ◽  
Vol 24 (498) ◽  
Author(s):  
Kirsten Lackner Solberg
Keyword(s):  
Program Analysis ◽  
Abstract Interpretation ◽  
Operational Semantics ◽  
Type System ◽  
Denotational Semantics ◽  
Type Systems ◽  
Strictness Analysis ◽  
Binding Time ◽  
The One ◽  
Treat All

<p>In this Ph.D. thesis, we study four program analyses. Three of them are specified by annotated type systems and the last one by abstract interpretation.</p><p>We present a combined strictness and totality analysis. We are specifying the analysis as an annotated type system. The type system allows conjunctions of annotated types, but only at the top-level. The analysis is somewhat more powerful than the strictness analysis by Kuo and Mishra due to the conjunctions and in that we also consider totality. The analysis is shown sound with respect to a natural-style operational semantics. The analysis is not immediately extendable to full conjunction.</p><p>The second analysis is also a combined strictness and totality analysis, however with ``full´´ conjunction. Soundness of the analysis is shown with respect to a denotational semantics. The analysis is more powerful than the strictness analyses by Jensen and Benton in that it in addition to strictness considers totality. So far we have only specified the analyses, however in order for the analyses to be practically useful we need an algorithm for inferring the annotated types. We construct an algorithm for the second analysis using the lazy type approach by Hankin and Le Métayer. The reason for choosing the second analysis from the thesis is that the approach is not applicable to the first analysis.</p><p>The third analysis we study is a binding time analysis. We take the analysis specified by Nielson and Nielson and we construct a more efficient algorithm than the one proposed by Nielson and Nielson. The algorithm collects constraints in a structural manner like the type inference algorithm by Damas. Afterwards the minimal solution to the set of constraints is found.</p><p>The last analysis in the thesis is specified by abstract interpretation. Hunt shows that projection based analyses are subsumed by PER (partial equivalence relation) based analyses using abstract interpretation. The PERs used by Hunt are strict, i.e. bottom is related to bottom. Here we lift this restriction by requiring the PERs to be uniform, in the sense that they treat all the integers equally. By allowing non-strict PERs we get three properties on the integers, corresponding to the three annotations used in the first and second analysis in the thesis.</p>

Pure iso-type systems

2019 ◽  
Vol 29 ◽  
Author(s):  
YANPENG YANG ◽  
BRUNO C. D. S. OLIVEIRA
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Expressive Power ◽  
Functional Languages ◽  
Type Conversion ◽  
Type Checking ◽  
Parallel Reduction ◽  
The Cost ◽  
Typed Languages

Abstract Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax for terms and types. In contrast, many dependently typed languages use a unified syntax that accounts for both terms and types. Unified syntax has some interesting advantages over separate syntax, including less duplication of concepts, and added expressiveness. However, integrating unrestricted general recursion in calculi with unified syntax is challenging when some level of type-level computation is present, since properties such as decidable type-checking are easily lost. This paper presents a family of calculi called pure iso-type systems (PITSs), which employs unified syntax, supports general recursion and preserves decidable type-checking. PITS is comparable in simplicity to pure type systems (PTSs), and is useful to serve as a foundation for functional languages that stand in-between traditional ML-like languages and fully blown dependently typed languages. In PITS, recursion and recursive types are completely unrestricted and type equality is simply based on alpha-equality, just like traditional ML-style languages. However, like most dependently typed languages, PITS uses unified syntax, naturally supporting many advanced type system features. Instead of implicit type conversion, PITS provides a generalization of iso-recursive types called iso-types. Iso-types replace the conversion rule typically used in dependently typed calculus and make every type-level computation explicit via cast operators. Iso-types avoid the complexity of explicit equality proofs employed in other approaches with casts. We study three variants of PITS that differ on the reduction strategy employed by the cast operators: call-by-name, call-by-value and parallel reduction. One key finding is that while using call-by-value or call-by-name reduction in casts loses some expressive power, it allows those variants of PITS to have simple and direct operational semantics and proofs. In contrast, the variant of PITS with parallel reduction retains the expressive power of PTS conversion, at the cost of a more complex metatheory.

scholarly journals A structured alternative to Prolog with simple compositional semantics

2011 ◽  
Vol 11 (4-5) ◽  
pp. 611-627
Author(s):  
ANTÓNIO PORTO
Keyword(s):  
Denotational Semantics ◽  
Expressive Power ◽  
Compositional Semantics ◽  
Variable Binding ◽  
Semantic Framework ◽  
Local Case ◽  
Real World Applications ◽  
Full Power ◽  
Definition Of ◽  
Concrete Language

AbstractProlog's very useful expressive power is not captured by traditional logic programming semantics, due mainly to the cut and goal and clause order. Several alternative semantics have been put forward, exposing operational details of the computation state. We propose instead to redesign Prolog around structured alternatives to the cut and clauses, keeping the expressive power and computation model but with a compositional denotational semantics over much simpler states—just variable bindings. This considerably eases reasoning about programs, by programmers and tools such as a partial evaluator, with safe unfolding of calls through predicate definitions. Anif-then-elseacross clauses replaces most uses of the cut, but the cut's full power is achieved by anuntilconstruct. Disjunction, conjunction anduntil, along with unification, are the primitive goal types with a compositional semantics yielding sequences of variable-binding solutions. This extends to programs via the usual technique of a least fixpoint construction. A simple interpreter for Prolog in the alternative language, and a definition ofuntilin Prolog, establish the identical expressive power of the two languages. Many useful control constructs are derivable from the primitives, and the semantic framework illuminates the discussion of alternative ones. The formalisation rests on a term language with variable abstraction as in the λ-calculus. A clause is an abstraction on the call arguments, a continuation, and the local variables. It can be inclusive or exclusive, expressing a local case bound to a continuation by either a disjunction or anif-then-else. Clauses are open definitions, composed (and closed) with simple functional application β-reduction). This paves the way for a simple account of flexible module composition mechanisms.Cube, a concrete language with the exposed principles, has been implemented on top of a Prolog engine and successfully used to build large real-world applications.

scholarly journals A Presheaf Semantics of Value-Passing Processes

1996 ◽  
Vol 3 (44) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Process Calculi ◽  
Traditional Definition ◽  
Open Maps

This paper investigates presheaf models for process calculi with<br />value passing. Denotational semantics in presheaf models are shown<br />to correspond to operational semantics in that bisimulation obtained<br />from open maps is proved to coincide with bisimulation as defined<br />traditionally from the operational semantics. Both "early" and "late"<br />semantics are considered, though the more interesting "late" semantics<br />is emphasised. A presheaf model and denotational semantics is proposed<br />for a language allowing process passing, though there remains<br />the problem of relating the notion of bisimulation obtained from open<br />maps to a more traditional definition from the operational semantics.<br />A tentative beginning is made of a "domain theory" supporting<br />presheaf models.

FIRST-CLASS CONTEXTS IN ML

2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO
Keyword(s):  
Programming Language ◽  
Operational Semantics ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Hole Filling ◽  
Dynamic Binding ◽  
Polymorphic Type ◽  
Open Program ◽  
Program Modules

This paper develops an ML-style programming language with first-class contexts i.e. expressions with holes. The crucial operation for contexts is hole-filling. Filling a hole with an expression has the effect of dynamic binding or macro expansion which provides the advanced feature of manipulating open program fragments. Such mechanisms are useful in many systems including distributed/mobile programming and program modules. If we can treat a context as a first-class citizen in a programming language, then we can manipulate open program fragments in a flexible and seamless manner. A possibility of such a programming language was shown by the theory of simply typed context calculus developed by Hashimoto and Ohori. This paper extends the simply typed system of the context calculus to an ML-style polymorphic type system, and gives an operational semantics and a sound and complete type inference algorithm.

Semantic Manipulations and Formal Ontology for Machine Learning based on Concept Algebra

2012 ◽  
pp. 194-220
Author(s):  
Yingxu Wang ◽  
Yousheng Tian ◽  
Kendal Hu
Keyword(s):  
Machine Learning ◽  
Operational Semantics ◽  
Mathematical Structure ◽  
Expressive Power ◽  
Formal Ontology ◽  
Cognitive Computing ◽  
Human Beings ◽  
Knowledge Modeling ◽  
Wide Range ◽  
Cognitive Robots

Towards the formalization of ontological methodologies for dynamic machine learning and semantic analyses, a new form of denotational mathematics known as concept algebra is introduced. Concept Algebra (CA) is a denotational mathematical structure for formal knowledge representation and manipulation in machine learning and cognitive computing. CA provides a rigorous knowledge modeling and processing tool, which extends the informal, static, and application-specific ontological technologies to a formal, dynamic, and general mathematical means. An operational semantics for the calculus of CA is formally elaborated using a set of computational processes in real-time process algebra (RTPA). A case study is presented on how machines, cognitive robots, and software agents may mimic the key ability of human beings to autonomously manipulate knowledge in generic learning using CA. This work demonstrates the expressive power and a wide range of applications of CA for both humans and machines in cognitive computing, semantic computing, machine learning, and computational intelligence.

scholarly journals On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces

1998 ◽  
Vol 8 (5) ◽  
pp. 481-540 ◽  
Author(s):  
DANIELE TURI ◽  
JAN RUTTEN
Keyword(s):  
Computer Science ◽  
Mathematical Theory ◽  
Metric Spaces ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Partial Orders ◽  
Present Survey ◽  
Induction Principle ◽  
Structural Operational Semantics ◽  
Modern Mathematics

This paper, a revised version of Rutten and Turi (1993), is part of a programme aiming at formulating a mathematical theory of structural operational semantics to complement the established theory of domains and denotational semantics to form a coherent whole (Turi 1996; Turi and Plotkin 1997). The programme is based on a suitable interplay between the induction principle, which pervades modern mathematics, and a dual, non-standard ‘coinduction principle’, which underlies many of the recursive phenomena occurring in computer science.The aim of the present survey is to show that the elementary categorical notion of a final coalgebra is a suitable foundation for such a coinduction principle. The properties of coalgebraic coinduction are studied both at an abstract categorical level and in some specific categories used in semantics, namely categories of non-well-founded sets, partial orders and metric spaces.

Lightweight family polymorphism

2008 ◽  
Vol 18 (3) ◽  
pp. 285-331 ◽  
Author(s):  
CHIERI SAITO ◽  
ATSUSHI IGARASHI ◽  
MIRKO VIROLI
Keyword(s):  
Type System ◽  
Object Oriented ◽  
Expressive Power ◽  
Type Inference ◽  
Design Decision ◽  
Dependent Types ◽  
Parametric Methods ◽  
Complex Type ◽  
Original Proposal ◽  
Object Oriented Languages

AbstractFamily polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system. In this article, we propose a simpler solution oflightweightfamily polymorphism, based on the idea that families are represented by classes rather than by objects. This change makes the type system significantly simpler without losing much expressive power of the language. Moreover, “family-polymorphic” methods now take a form of parametric methods; thus, it is easy to apply method type argument inference as in Java 5.0. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove that the type system is sound. An algorithm for type inference for family-polymorphic method invocations is also formalized and proved to be correct. Finally, a formal translation by erasure to Featherweight Java is presented; it is proved to preserve typing and execution results, showing that our new language features can be implemented in Java by simply extending the compiler.

scholarly journals Baby Modula-3 and a theory of objects

1994 ◽  
Vol 4 (2) ◽  
pp. 249-283 ◽  
Author(s):  
Martin Abadi
Keyword(s):  
Programming Language ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Object Oriented ◽  
Denotational Semantics ◽  
Object Oriented Programming ◽  
The Core ◽  
Functional Object ◽  
Oriented Programming Language

AbstractBaby Modula-3 is a small, functional, object-oriented programming language. It is intended as a vehicle for explaining the core of Modula-3 from a biased perspective: Baby Modula-3 includes the main features of Modula-3 related to objects, but not much else. To the theoretician, Baby Modula-3 provides a tractable, concrete example of an object-oriented language, and we use it to study the formal semantics of objects. Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition.

scholarly journals A Fully Abstract Presheaf Semantics of SCCS with Finite Delay

1999 ◽  
Vol 6 (28) ◽  
Author(s):  
Thomas Troels Hildebrandt
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Transition Systems ◽  
Finite Delay ◽  
Open Map ◽  
Special Case

We present a presheaf model for the observation of infinite as well<br />as finite computations. We apply it to give a denotational semantics of<br />SCCS with finite delay, in which the meanings of recursion are given by<br />final coalgebras and meanings of finite delay by initial algebras of the<br />process equations for delay. This can be viewed as a first step in representing<br />fairness in presheaf semantics. We give a concrete representation<br />of the presheaf model as a category of generalised synchronisation<br />trees and show that it is coreflective in a category of generalised transition<br />systems, which are a special case of the general transition systems<br />of Hennessy and Stirling. The open map bisimulation is shown to coincide<br />with the extended bisimulation of Hennessy and Stirling. Finally<br />we formulate Milners operational semantics of SCCS with finite delay<br />in terms of generalised transition systems and prove that the presheaf<br />semantics is fully abstract with respect to extended bisimulation.

Sign in / Sign up

Export Citation Format

Share Document