scholarly journals Distributing intersection and union types with splits and duality (functional pearl)

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-24
Author(s):  
Xuejing Huang ◽  
Bruno C. d. S. Oliveira
Keyword(s):  
Programming Languages ◽  
Relevant Logic ◽  
Logical Entailment ◽  
Language Constructs ◽  
Functional Code

Subtyping with intersection and union types is nowadays common in many programming languages. From the perspective of logic, the subtyping problem is essentially the problem of determining logical entailment : does a logical statement follow from another one? Unfortunately, algorithms for deciding subtyping and logical entailment with intersections, unions and various distributivity laws can be highly non-trivial. This functional pearl presents a novel algorithmic formulation for subtyping (and logical entailment) in the presence of various distributivity rules between intersections, unions and implications (i.e. function types). Unlike many existing algorithms which first normalize types and then apply a subtyping algorithm on the normalized types, our new subtyping algorithm works directly on source types. Our algorithm is based on two recent ideas: a generalization of subtyping based on the duality of language constructs called duotyping ; and splittable types , which characterize types that decompose into two simpler types. We show that our algorithm is sound, complete and decidable with respect to a declarative formulation of subtyping based on the minimal relevant logic B + . Moreover, it leads to a simple and compact implementation in under 50 lines of functional code.

scholarly journals Constructive Action Semantics for Core ML

2004 ◽  
Vol 11 (37) ◽  
Author(s):  
Jørgen Iversen ◽  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Tool Support ◽  
Semantic Description ◽  
Action Semantics ◽  
Language Constructs ◽  
Description Framework ◽  
The Individual ◽  
Language Construct ◽  
Language Description

Usually, the majority of language constructs found in a programming language can also be found in many other languages, because language design is based on reuse. This should be reflected in the way we give semantics to programming languages. It can be achieved by making a language description consist of a collection of modules, each defining a single language construct. The description of a single language construct should be language independent, so that it can be reused in other descriptions without any changes. We call a language description framework ``constructive'' when it supports independent description of individual constructs.<br /> <br />We present a case study in constructive semantic description. The case study is a description of Core ML, consisting of a mapping from it to BAS (Basic Abstract Syntax) and action semantic descriptions of the individual BAS constructs. The latter are written in ASDF (Action Semantics Definition Formalism), a formalism specially designed for writing action semantic descriptions of single language constructs. Tool support is provided by the ASF+SDF Meta-Environment and by the Action Environment, which is a new extension of the ASF+SDF Meta-Environment.

JOIN POINT DESIGNATION DIAGRAMS: A GRAPHICAL REPRESENTATION OF JOIN POINT SELECTIONS

2006 ◽  
Vol 16 (03) ◽  
pp. 317-346 ◽  
Author(s):  
DOMINIK STEIN ◽  
STEFAN HANENBERG ◽  
RAINER UNLAND
Keyword(s):  
Software Development ◽  
Programming Languages ◽  
Graphical Representation ◽  
Point Selection ◽  
Aspect Oriented Programming ◽  
Specific Language ◽  
Design Issue ◽  
Language Constructs ◽  
Join Point

The specification of join point selections (also known as "pointcuts") is a major design issue in Aspect-Oriented Software Development. Aspect-oriented systems generally provide specific language constructs (subsumed by the term "pointcut language") for specifying such a join point selection. Pointcut languages differ widely with respect to their syntax and semantics. Consequently, developers familiar with one specific language can hardly benefit from this knowledge when designing and implementing pointcuts in another language. This implies that developers working with different aspect-oriented languages can hardly communicate their design to each other, and knowledge about aspect-oriented design can hardly be transferred among developers developing in different languages. In order to overcome this problem, we present novel specification means based on the UML to represent diverse ways of join point selections — without relying on language-specific syntax and semantics. Instead, the proposed language constructs are able to express join point selections in a variety of different aspect-oriented programming languages.

scholarly journals A Taxonomy for Programming Languages wit h Multi-Sequential Processes

1984 ◽  
Vol 13 (175) ◽  
Author(s):  
Kristine Stougård Thomsen ◽  
Jørgen Lindskov Knudsen
Keyword(s):  
Conceptual Framework ◽  
Programming Languages ◽  
Formal Model ◽  
The Other ◽  
Application Area ◽  
Language Constructs ◽  
Concurrent Processes ◽  
Sequential Processes ◽  
High Level

<p>The purpose of this paper is to describe a high level conceptual framework -- a taxonomy -- for programming languages with language constructs for specification of co-sequential and concurrent/interleaved processes.</p><p>Using a semi-formal model for processes we identify the major differences and similarities between co-sequential, interleaved and concurrent processes. We discuss the essential aspects of co-sequential processes, concerning different patterns in which control can be transferred between the processes. Moreover, we discuss the important common properties of co-sequential and concurrent/interleaved processes: Synchronization and communication. The form of this taxonomy is a tree of orthogonal aspects where each aspect may be further subdivided into orthogonal aspects. Each aspect is precisely defined and can be discussed without reference to the other aspects. This makes it easy to use the taxonomy when analyzing and comparing language constructs.</p><p>We find that the taxonomy is useful in at least three areas: When choosing a language for a specific application, when designing a language for a specific application area, and when teaching high level languages with multi-sequential processes.</p>

scholarly journals Type Checking Semantic Functions in ASDF

2004 ◽  
Vol 11 (35) ◽  
Author(s):  
Jørgen Iversen
Keyword(s):  
Side Effects ◽  
Programming Languages ◽  
Type System ◽  
Type Checking ◽  
Semantic Function ◽  
Semantic Framework ◽  
Language Constructs ◽  
Type Check

When writing semantic descriptions of programming languages, it is convenient to have tools for checking the descriptions. With frameworks that use inductively defined semantic functions to map programs to their denotations, we would like to check that the semantic functions result in denotations with certain properties. In this paper we present a type system for a modular style of the action semantic framework that, given signatures of all the semantic functions used in a semantic equation defining a semantic function, performs a soft type check on the action in the semantic equation.<br /> <br />We introduce types for actions that describe different properties of the actions, like the type of data they expect and produce, whether they can fail or have side effects, etc. A type system for actions which uses these new action types is presented. Using the new action types in the signatures of semantic functions, the language describer can assert properties of semantic functions and have the assertions checked by an implementation of the type system.<br /> <br />The type system has been implemented for use in connection with the recently developed formalism ASDF. The formalism supports writing language definitions by combining modules that describe single language constructs. This is possible due to the inherent modularity in ASDF. We show how we manage to preserve the modularity and still perform specialised type checks for each module.

scholarly journals Parsing multi-ordered grammars with the Gray algorithm

2019 ◽  
Author(s):  
Nick Papoulias
Keyword(s):  
Programming Languages ◽  
Language Processing ◽  
Language Design ◽  
Formal Specifications ◽  
Problem Statement ◽  
Language Constructs ◽  
Chart Parsing ◽  
Parsing Algorithm ◽  
Definition Of ◽  
Context Free

Background. Context-free grammars (CFGs) and Parsing-expression Grammars (PEGs) are the two main formalisms used by formal specifications and parsing frameworks to describe programming languages. They mainly differ in the definition of the choice operator, describing language alternatives. CFGs support the use of non-deterministic choice (i.e., unordered choice), where all alternatives are equally explored. PEGs support a deterministic choice (i.e., ordered choice), where alternatives are explored in strict succession. In practice the two formalisms, are used through concrete classes of parsing algorithms (such as Left-to-right, rightmost derivation (LR) for CFGs and Packrat parsing for PEGs), that follow the semantics of the formal operators. Problem Statement. Neither the two formalisms, nor the accompanying algorithms are sufficient for a complete description of common cases arising in language design. In order to properly handle ambiguity, recursion, precedence or associativity, parsing frameworks either introduce implementation specific directives or ask users to refactor their grammars to fit the needs of the framework/algorithm/formalism combo. This introduces significant complexity even in simple cases and results in incompatible grammar specifications. Our Proposal. We introduce Multi-Ordered Grammars (MOGs) as an alternative to the CFG and PEG formalisms. MOGs aim for a better exploration of ambiguity, ordering, recursion and associativity during language design. This is achieved by (a) allowing both deterministic and non-deterministic choices to co-exist, and (b) introducing a form of recursive and scoped ordering. The formalism is accompanied by a new parsing algorithm (Gray) that extends chart parsing (normally used for Natural Language Processing) with the proposed MOG operators. Results. We conduct two case-studies to assess the expressiveness of MOGs, compared to CFGs and PEGs. The first consists of two idealized examples from literature (an expression grammar and a simple procedural language). The second examines a real-world case (the entire Smalltalk grammar and eleven new Smalltalk extensions) probing the complexities of practical needs. We show that in comparison, MOGs are able to reduce complexity and naturally express language constructs, without resorting to implementation specific directives. Conclusion. We conclude that combining deterministic and non-deterministic choices in a single grammar specification is indeed not only possible but also beneficial. Moreover, augmented by operators for recursive and scoped ordering the resulting multi-ordered formalism presents a viable alternative to both CFGs and PEGs. Concrete implementations of MOGs can be constructed by extending chart parsing with MOG operators for recursive and scoped ordering.

scholarly journals Parsing multi-ordered grammars with the Gray algorithm

2019 ◽  
Author(s):  
Nick Papoulias
Keyword(s):  
Programming Languages ◽  
Language Processing ◽  
Language Design ◽  
Formal Specifications ◽  
Problem Statement ◽  
Language Constructs ◽  
Chart Parsing ◽  
Parsing Algorithm ◽  
Definition Of ◽  
Context Free

Background. Context-free grammars (CFGs) and Parsing-expression Grammars (PEGs) are the two main formalisms used by formal specifications and parsing frameworks to describe programming languages. They mainly differ in the definition of the choice operator, describing language alternatives. CFGs support the use of non-deterministic choice (i.e., unordered choice), where all alternatives are equally explored. PEGs support a deterministic choice (i.e., ordered choice), where alternatives are explored in strict succession. In practice the two formalisms, are used through concrete classes of parsing algorithms (such as Left-to-right, rightmost derivation (LR) for CFGs and Packrat parsing for PEGs), that follow the semantics of the formal operators. Problem Statement. Neither the two formalisms, nor the accompanying algorithms are sufficient for a complete description of common cases arising in language design. In order to properly handle ambiguity, recursion, precedence or associativity, parsing frameworks either introduce implementation specific directives or ask users to refactor their grammars to fit the needs of the framework/algorithm/formalism combo. This introduces significant complexity even in simple cases and results in incompatible grammar specifications. Our Proposal. We introduce Multi-Ordered Grammars (MOGs) as an alternative to the CFG and PEG formalisms. MOGs aim for a better exploration of ambiguity, ordering, recursion and associativity during language design. This is achieved by (a) allowing both deterministic and non-deterministic choices to co-exist, and (b) introducing a form of recursive and scoped ordering. The formalism is accompanied by a new parsing algorithm (Gray) that extends chart parsing (normally used for Natural Language Processing) with the proposed MOG operators. Results. We conduct two case-studies to assess the expressiveness of MOGs, compared to CFGs and PEGs. The first consists of two idealized examples from literature (an expression grammar and a simple procedural language). The second examines a real-world case (the entire Smalltalk grammar and eleven new Smalltalk extensions) probing the complexities of practical needs. We show that in comparison, MOGs are able to reduce complexity and naturally express language constructs, without resorting to implementation specific directives. Conclusion. We conclude that combining deterministic and non-deterministic choices in a single gram- mar specification is indeed not only possible but also beneficial. Moreover, augmented by operators for recursive and scoped ordering the resulting multi-ordered formalism presents a viable alternative to both CFGs and PEGs. Concrete implementations of MOGs can be constructed by extending chart parsing with MOG operators for recursive and scoped ordering.

scholarly journals Un protocole de fertilisation croisée d’un langage fonctionnel et d’un langage objet: application à la mise en oeuvre d’un prototype d’éditeur coopératif asynchrone

2011 ◽  
Vol Volume 14 - 2011 - Special... ◽  
Author(s):  
Maurice Tchoupé Tchendji
Keyword(s):  
Programming Languages ◽  
Mise En Œuvre ◽  
International Audience ◽  
The Cross ◽  
Programming Paradigms ◽  
Two Sectors ◽  
Cross Fertilization ◽  
Functional Code

International audience The cross-fertilization is a technique to pool expertise and resources of at least two sectors in order to make the best of each. In this paper, we present a protocol of programming based on cross-fertilization of two programming languages (Haskell and Java) under two different programming paradigms: the functional paradigm and the object paradigm. This pooling of the strengths of each type of language permit to develop more secure applications in a shorter time, with functional code concise, easily understandable and thus, easily maintainable by one third. We present the meta-architecture of applications developed following this approach and an instantiation of it for the implementation of a prototype of an asynchronous collaborative editor. La fertilisation croisée est une technique permettant de mettre en commun des compétences et des ressources d’au moins deux secteurs d’activité afin d’en tirer le meilleur de chaque. Dans ce papier, nous présentons un protocole de programmation basé sur la fertilisation croisée de deux langages de programmation (Haskell et Java) relevant de deux paradigmes de programmation différents: le paradigme fonctionnel et le paradigme objet. Cette mutualisation des points forts de chaque type de langage permet de développer des applications plus sûres, en un temps moindre, ayant un code fonctionnel concis, facilement compréhensible et donc, facilement maintenable par un tiers. Nous présentons la méta-architecture des applications développées suivant cette approche ainsi qu’une instanciation de celle-ci pour la mise en oeuvre d’un prototype d’éditeur coopératifasynchrone.

scholarly journals An Action Environment

2004 ◽  
Vol 11 (36) ◽  
Author(s):  
Mark Van den Brand ◽  
Jørgen Iversen ◽  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Semantic Description ◽  
New Formalism ◽  
Recent Advances ◽  
Language Constructs ◽  
Conditional Statements

Some basic programming constructs (e.g., conditional statements) are found in many different programming languages, and can often be included without change when a new language is designed. When writing a semantic description of a language, however, it is usually not possible to reuse parts of previous descriptions without change.<br /> <br />This paper introduces a new formalism, ASDF, which has been designed specifically for giving reusable action semantic descriptions of individual language constructs. An initial case study in the use of ASDF has already provided reusable descriptions of all the basic constructs underlying Core ML.<br /> <br /> The paper also describes the Action Environment, a new environment supporting use and validation of ASDF descriptions. The Action Environment has been implemented on top of the ASF+SDF Meta-Environment, exploiting recent advances in techniques for integration of different formalisms, and inheriting all the main features of the Meta-Environment.

scholarly journals Two N-of-1 self-trials on readability differences between anonymous inner classes (AICs) and lambda expressions (LEs) on Java code snippets

2021 ◽  
Vol 27 (2) ◽  
Author(s):  
Stefan Hanenberg ◽  
Nils Mehlhorn
Keyword(s):  
Reaction Time ◽  
Programming Languages ◽  
Single Subject ◽  
Scientific Methods ◽  
Language Constructs ◽  
Data Points ◽  
Independent Variable ◽  
The Relationship ◽  
Language Construct ◽  
Java Code

AbstractIn Java, lambda expressions (LEs) were introduced at a time where the similar language construct anonymous inner class (AIC) already existed for years. But while LEs became quite popular in mainstream programming languages in general, their usability is hardly studied. From the Java perspective the need to study the relationship between LEs and AICs was and is quite obvious, because both language constructs co-exist. However, it is quite usual that new language constructs are introduced although they are not or hardly studied using scientific methods – and an often heard argument from programming language designers is that the effort or the costs for the application of the scientific method on language constructs is too high. The present paper contributes in two different ways. First, with respect to LEs in comparison to AICs, this paper presents two N-of-1 studies (i.e. randomized control trials executed on a single subject) where LEs and AICs are used as listeners in Java code. Both experiments had two similar and rather simple tasks (“count the number of parameters”, respectively “count the number of used parameters”) with the dependent variable being reaction time. The first experiment used the number of parameters, the second the number of used parameters as the controlled, independent variable (in addition to the technique LE and AIC). Other variables (LOC, etc.) were randomly generated within given boundaries. The main result of both experiments is that LEs without type annotations require less reading time (p hs .2, reduction of reaction time of at most 35%). The results are based on 9,600 observations (one N-of-1 trial with eight replications). This gives evidence that the readability of LEs without type annotations improves the readability of code. However, the effect seems to be so small, that we do not expect this to have a larger impact on daily programming. Second, we see the contribution of this paper in the application of N-of-1 trials. Such experiments require relatively low effort in the data selection but still permit to analyze results in a non-subjective way using commonly accepted analysis techniques. Additionally, they permit to increase the number of selected data points in comparison to traditional multi–subject experiments. We think that researchers should take such experiments into account before planning and executing larger experiments.

The lazy logic of partial terms

2002 ◽  
Vol 67 (3) ◽  
pp. 1065-1077
Author(s):  
Raymond D. Gumb
Keyword(s):  
Computer Science ◽  
Programming Languages ◽  
Programming Language ◽  
Specific Area ◽  
The Other ◽  
Science Program ◽  
Free Logic ◽  
Partial Functions ◽  
Unary Function ◽  
Language Constructs

AbstractThe Logic of Partial TermsLPTis a strict negative free logic that provides an economical framework for developing many traditional mathematical theories having partial functions. In these traditional theories, all functions and predicates are strict. For example, if a unary function (predicate) is applied to an undefined argument, the result is undefined (respectively, false). On the other hand, every practical programming language incorporates at least one nonstrict or lazy construct, such as the if-then-else, but nonstrict functions cannot be either primitive or introduced in definitional extensions inLPT. Consequently, lazy programming language constructs do not fit the traditional mathematical mold inherent inLPT. A nonstrict (positive free) logic is required to handle nonstrict functions and predicates.Previously developed nonstrict logics are not fully satisfactory because they are verbose in describing strict functions (which predominate in many programming languages), and some logicians find their semantics philosophically unpalatable. The newly developed Lazy Logic of Partial TermsLLis as concise asLPTin describing strict functions and predicates, and strict and nonstrict functions and predicates can be introduced in definitional extensions of traditional mathematical theories.LLis “built on top of”LPT. and, likeLPT, admits only one domain in the semantics. In the semantics, for the case of a nonstrict unary functionhin an LL theoryT, we have ⊨Th(⊥) =y↔ ∀x(h(x) = y), where ⊥ is a canonical undefined term. Correspondingly, in the axiomatization, the “indifference” (to the value of the argument) axiomh(⊥) =y↔ ∀x(h(x) = y)guarantees a proper fit with the semantics. The price paid forLL's naturalness is that it is tailored for describing a specific area of computer science, program specification and verification, possibly limiting its role in explicating classical mathematical and philosophical subjects.

Sign in / Sign up

Export Citation Format

Share Document