Phase distinction

Last updated

Phase Distinction is a property of programming languages that observe a strict division between types and terms. A concise rule for determining whether phase distinction is preserved in a language or not has been proposed by Luca Cardelli - If A is a compile-time term and B is a subterm of A, then B must also be a compile-time term. [1]

A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered. From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type.

An expression in a programming language is a combination of one or more constants, variables, operators, and functions that the programming language interprets and computes to produce another value. This process, as for mathematical expressions, is called evaluation.

Luca Cardelli Italian computer scientist

Luca Andrea Cardelli FRS is an Italian computer scientist who is an Assistant Director at Microsoft Research in Cambridge, UK. Cardelli is well known for his research in type theory and operational semantics. Among other contributions, he helped design Modula-3, implemented the first compiler for the (non-pure) functional programming language ML, and defined the concept of typeful programming. He helped develop the Polyphonic C# experimental programming language.

Contents

Most statically typed languages conform to the principle of phase distinction. However, some languages with especially flexible and expressive type systems (notably dependently typed programming languages) allow types to be manipulated in the same ways as regular terms. They may be passed to functions or returned as results.

A language with phase distinction may have separate namespaces for types and run-time variables. In an optimizing compiler, phase distinction marks the boundary between expressions which are safe to erase.

In computing, a namespace is a set of symbols that are used to organize objects of various kinds, so that these objects may be referred to by name. In Java, a namespace ensures that all the identifiers within it must have unique names so that they can be easily identified. In order to manage the namespace Java provides the mechanism of creating Java packages. Prominent examples include:

In computing, an optimizing compiler is a compiler that tries to minimize or maximize some attributes of an executable computer program. The most common requirement is to minimize the time taken to execute a program; a less common one is to minimize the amount of memory occupied. The growth of portable computers has created a market for minimizing the power consumed by a program.

In programming languages, type erasure refers to the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. Operational semantics that do not require programs to be accompanied by types are called type-erasure semantics, to be contrasted with type-passing semantics. The possibility of giving type-erasure semantics is a kind of abstraction principle, ensuring that the run-time execution of a program does not depend on type information. In the context of generic programming, the opposite of type erasure is called reification.

Theory

Phase distinction is used in conjunction with static checking. [2] By using a calculus based system, phase distinction removes the need to enforce linear logic between different types and terms of programming. [3]

Introduction

Phase Distinction distinguishes between processing to be done at compile-time versus processing done at runtime.

Consider a simple language, [3] with terms:

   t ::= true | false | x | λx : T . t | t t | if t then t else t

and types:

   T ::= Bool | T -> T

Note how types and terms are distinct. At compile time, types are used to verify the validity of the terms. However, types do not play any role at runtime.

Related Research Articles

A compiler is a computer program that translates computer code written in one programming language into another programming language. The name compiler is primarily used for programs that translate source code from a high-level programming language to a lower level language to create an executable program.

Java (programming language) Object-oriented programming language

Java is a general-purpose programming language that is class-based, object-oriented, and designed to have as few implementation dependencies as possible. It is intended to let application developers "write once, run anywhere" (WORA), meaning that compiled Java code can run on all platforms that support Java without the need for recompilation. Java applications are typically compiled to "bytecode" that can run on any Java virtual machine (JVM) regardless of the underlying computer architecture. The syntax of Java is similar to C and C++, but it has fewer low-level facilities than either of them. As of 2018, Java was one of the most popular programming languages in use according to GitHub, particularly for client-server web applications, with a reported 9 million developers.

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

In computer science, an interpreter is a computer program that directly executes, i.e. performs, instructions written in a programming or scripting language, without requiring them previously to have been compiled into a machine language program. An interpreter generally uses one of the following strategies for program execution:

  1. Parse the source code and perform its behavior directly;
  2. Translate source code into some efficient intermediate representation and immediately execute this;
  3. Explicitly execute stored precompiled code made by a compiler which is part of the interpreter system.

In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.

In computing, code generation is the process by which a compiler's code generator converts some intermediate representation of source code into a form that can be readily executed by a machine.

In computer science, run time, runtime or execution time is the time during which a program is running (executing), in contrast to other program lifecycle phases such as compile time, link time and load time.

In programming languages, a type system is a set of rules that assigns a property called type to the various constructs of a computer program, such as variables, expressions, functions or modules. These types formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components. The main purpose of a type system is to reduce possibilities for bugs in computer programs by defining interfaces between different parts of a computer program, and then checking that the parts have been connected in a consistent way. This checking can happen statically, dynamically, or as a combination of static and dynamic checking. Type systems have other purposes as well, such as expressing business rules, enabling certain compiler optimizations, allowing for multiple dispatch, providing a form of documentation, etc.

In computing, just-in-time (JIT) compilation is a way of executing computer code that involves compilation during execution of a program – at run time – rather than prior to execution. Most often, this consists of source code or more commonly bytecode translation to machine code, which is then executed directly. A system implementing a JIT compiler typically continuously analyses the code being executed and identifies parts of the code where the speedup gained from compilation or recompilation would outweigh the overhead of compiling that code.

Dynamic programming language, in computer science, is a class of high-level programming languages which, at runtime, execute many common programming behaviors that static programming languages perform during compilation. These behaviors could include extension of the program, by adding new code, by extending objects and definitions, or by modifying the type system. Although similar behaviours can be emulated in nearly any language, with varying degrees of difficulty, complexity and performance costs, dynamic languages provide direct tools to make use of them. Many of these features were first implemented as native features in the Lisp programming language.

In programming languages and type theory, polymorphism is the provision of a single interface to entities of different types or the use of a single symbol to represent multiple different types.

Execution in computer and software engineering is the process by which a computer or virtual machine executes the instructions of a computer program. Each instruction of a program is a description of a specific action to be carried out in order for a specific problem to be solved; as instructions of a program and therefore the actions they describe are being carried out by an executing machine, specific effects are produced in accordance to the semantics of the instructions being executed.

TOPS-10 System is a discontinued operating system from Digital Equipment Corporation (DEC) for the PDP-10 mainframe computer family. Launched in 1967, TOPS-10 evolved from the earlier "Monitor" software for the PDP-6 and PDP-10 computers; this was renamed to TOPS-10 in 1970.

Late binding, dynamic binding, or dynamic linkage is a computer programming mechanism in which the method being called upon an object or the function being called with arguments is looked up by name at runtime.

A runtime system, also called run-time system, runtime environment or run-time environment, primarily implements portions of an execution model. This is not to be confused with the runtime lifecycle phase of a program, during which the runtime system is in operation. Most languages have some form of runtime system that provides an environment in which programs run. This environment may address a number of issues including the layout of application memory, how the program accesses variables, mechanisms for passing parameters between procedures, interfacing with the operating system, and otherwise. The compiler makes assumptions depending on the specific runtime system to generate correct code. Typically the runtime system will have some responsibility for setting up and managing the stack and heap, and may include features such as garbage collection, threads or other dynamic features built into the language.

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without depending on their type. Such functions and data types are called generic functions and generic datatypes respectively and form the basis of generic programming.

In computer science, ahead-of-time compilation is the act of compiling a higher-level programming language such as C or C++, or an intermediate representation such as Java bytecode or .NET Framework Common Intermediate Language (CIL) code, into a native (system-dependent) machine code so that the resulting binary file can execute natively.

Baby Modula-3 is a functional programming sublanguage of Modula-3 programming language based on ideals invented by Martín Abadi. It is an object oriented language for studying programming language design; one part of it is implicitly prototype-oriented programming language, and the other is explicitly statically typed designed for studying computer science type theories. It has been checked as a formal language of metaprogramming systems. It comes from the "Scandinavian School" of object-oriented programming languages.

In computer programming, programming languages are often colloquially classified as to whether the language's type system makes it strongly typed or weakly typed. Generally, a strongly typed language has stricter typing rules at compile time, which implies that errors and exceptions are more likely to happen during compilation. Most of these rules affect variable assignment, return values and function calling. On the other hand, a weakly typed language has looser typing rules and may produce unpredictable results or may perform implicit type conversion at runtime. A different but related concept is latent typing.

References

  1. ↑ Cardelli, Luca (3 January 1988). "Phase Distinctions in Type Theory" (PDF). Digital Equipment Corporation.
  2. ↑ Cardelli, Luca (3 January 1988). "Phase Distinctions in Type Theory" (PDF). Digital Equipment Corporation.
  3. 1 2 "CMSC 336: Type Systems for Programming Languages; Lecture 7: Curry-Howard Isomorphism & Derived Forms" (PDF). 31 January 2008.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.