scholarly journals Polymorphic Subtyping for Side Effects

1997 ◽  
Vol 26 (529) ◽  
Author(s):  
Torben Amtoft ◽  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Side Effects ◽  
Type System ◽  
Common Type ◽  
Prototype System ◽  
Inference Algorithm ◽  
Post Processing ◽  
Core Subset ◽  
Causality Information

<p>The integration of polymorphism (in the style of the ML let-construct), subtyping, and effects (modelling assignment or communication) into one common type system has proved remarkably difficult. This paper presents a type system for (a core subset of) Concurrent~ML that extends the ML type system in a conservative way and that employs all these features; and in addition causality information has been incorporated into the effects (which may therefore be termed "behaviours").</p><p>The semantic soundness of the system is established via a subject reduction result. An inference algorithm is presented; it is proved sound and (in a certain sense) also complete. A prototype system based on this algorithm has been implemented and can be experienced on the <a href="http://www.daimi.aau.dk/~bra8130/TBAcml/TBA_CML.html">WWW</a>; thanks to a special post-processing phase it produces quite readable and informative output.</p>

scholarly journals Polymorphic Subtyping for Effect Analysis: The Integration

1996 ◽  
Vol 25 (501) ◽  
Author(s):  
Hanne Riis Nielson ◽  
Flemming Nielson ◽  
Torben Amtoft
Keyword(s):  
Type System ◽  
Common Type ◽  
Inference Algorithm ◽  
Conservative Extension ◽  
Effect Analysis

The integration of polymorphism (in style of the ML <kbd>let</kbd>-construct), subtyping, and effects (modelling assignment or communication) into one common type system has proved remarkably difficult. One line of research has succeeded in integrating polymorphism and subtyping; adding effects in a straightforward way results in a semantically unsound system. Another line of research has succeeded in integrating polymorphism, effects, and subeffecting; adding sybtyping in a straightforward way invalidaters the construction of the inference algorithm. This paper integrates all op polymorphism, effects, and sybtyping into an annotated type and effect system for Concurrent ML and shows that the resulting system is a conservative extension of the ML type system.

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.

Weak polymorphism can be sound

1996 ◽  
Vol 6 (1) ◽  
pp. 111-141 ◽  
Author(s):  
John Greiner
Keyword(s):  
New Jersey ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Inference Algorithm ◽  
Standard Ml ◽  
Polymorphic Type

AbstractThe weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.

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 Association of lamotrigine and valproate in refractory epilepsies of children and adolescents

2008 ◽  
Vol 66 (3a) ◽  
pp. 477-481 ◽  
Author(s):  
Karen P. Grisotto ◽  
Isac Bruck ◽  
Sérgio A. Antoniuk ◽  
Lúcia H.C. Santos
Keyword(s):  
Side Effects ◽  
Children And Adolescents ◽  
Retrospective Analysis ◽  
Sodium Valproate ◽  
Seizure Control ◽  
Common Type ◽  
Response To Treatment ◽  
Seizure Type ◽  
Treatment Side Effects ◽  
Clonic Seizures

OBJECTIVE: To evaluate the efficacy or eventual side-effects of the association of lamotrigine and sodium valproate in the control of refractory epilepsies. METHOD: A retrospective analysis of 37 children with a mean age of 12 years taking exclusivelly lamotrigine and sodium valproate. Efficacy of seizure control was considered satisfactory if there was a reduction in seizures >50% or total control. RESULTS: The association of lamotrigine and sodium valproate was considered satisfactory in 65% of the studied children, independent of seizure type. Total seizure control was obtained in 33% and 35% had an unsatisfactory response or remained unchanged. Primary generalized tonic clonic seizures were the most common type with 84% of day-time seizures having a good response to treatment. Side-effects were seen in 11% of patients and the most common was tremor. CONCLUSION: Total or satisfactory control of seizures was seen in the majority of patients and side-effects were uncommon.

Integrating region memory management and tag-free generational garbage collection

2021 ◽  
Vol 31 ◽  
Author(s):  
MARTIN ELSMAN ◽  
NIELS HALLENBERG
Keyword(s):  
Memory Management ◽  
Garbage Collection ◽  
State Of The Art ◽  
Type System ◽  
Inference Algorithm ◽  
Machine Code ◽  
Standard Ml ◽  
Management Scheme ◽  
Time Region ◽  
Formal Properties

Abstract We present a region-based memory management scheme with support for generational garbage collection. The scheme features a compile-time region inference algorithm, which associates values with logical regions, and builds on a region type system that deploys region types at runtime to avoid the overhead of write barriers and to support partly tag-free garbage collection. The scheme is implemented in the MLKit Standard ML compiler, which generates native x64 machine code. Besides demonstrating a number of important formal properties of the scheme, we measure the scheme’s characteristics, for a number of benchmarks, and compare the performance of the generated executables with the performance of executables generated with the MLton state-of-the-art Standard ML compiler and configurations of the MLKit with and without region inference and generational garbage collection enabled. Although region inference often serves the purpose of generations, combining region inference with generational garbage collection is shown often to be superior to combining region inference with non-generational collection despite the overhead introduced by a larger amount of memory waste, due to region fragmentation.

scholarly journals On-Site BIM-Enabled Augmented Reality for Construction

2021 ◽  
pp. 46-56
Author(s):  
Adam Chernick ◽  
Christopher Morse ◽  
Steve London ◽  
Tim Li ◽  
David Ménard ◽  
...  
Keyword(s):  
Augmented Reality ◽  
Prototype System ◽  
Post Processing ◽  
Building Element ◽  
Combining Data ◽  
Data Flows ◽  
Building Information ◽  
General Contractors ◽  
Processing Information ◽  
Intuitive User Interface

AbstractWe describe a prototype system for communicating building information and models directly to on-site general contractors and subcontractors. The system, developed by SHoP Architects, consists of a workflow of pre-processing information within Revit, post-processing information outside of Revit, combining data flows inside of a custom application built on top of Unity Reflect, and delivering the information through a mobile application on site with an intuitive user interface. This system incorporates augmented reality in combination with a dashboard of documentation views categorized by building element.

Common Type System

2004 ◽  
pp. 3-27
Author(s):  
Gregory S. MacBeth
Keyword(s):  
Type System ◽  
Common Type

scholarly journals Coercions in a polymorphic type system

2008 ◽  
Vol 18 (4) ◽  
pp. 729-751 ◽  
Author(s):  
ZHAOHUI LUO
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Functional Programming Languages ◽  
Polymorphic Type ◽  
And Function ◽  
Dependent Type

We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete.

Sign in / Sign up

Export Citation Format

Share Document