“Gradual typing”的意思、由来-开放百科全书

Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile-time (which is static typing) and some expressions may be left untyped and eventual type errors are reported at run-time (which is dynamic typing). Gradual typing allows software developers to choose either type paradigm as appropriate, from within a single language.^[1] In many cases gradual typing is added to an existing dynamic language, creating a derived language allowing but not requiring static typing to be used. In some cases a language uses gradual typing from the start.

Implementation

In particular, gradual typing uses a special type named dynamic to represent statically-unknown types, and gradual typing replaces the notion of type equality with a new relation called consistency that relates the dynamic type to every other type. The consistency relation is symmetric but not transitive.^[2]

Prior attempts at integrating static and dynamic typing tried to make the dynamic type be both the top and bottom of the subtype hierarchy. However, because subtyping is transitive, that results in every type becoming related to every other type, and so subtyping would no longer rule out any static type errors. The addition of a second phase of plausibility checking to the type system did not completely solve this problem.^[3]^[4]

Gradual typing can easily be integrated into the type system of an object-oriented language that already uses the subsumption rule to allow implicit up-casts with respect to subtyping. The main idea is that consistency and subtyping are orthogonal ideas that compose nicely. To add subtyping to a gradually-typed language, simply add the subsumption rule and add a subtyping rule that makes the dynamic type a subtype of itself, because subtyping is supposed to be reflexive. (But do not make the top of the subtyping order dynamic!)^[5]

Examples

Examples of gradually typed languages derived from existing dynamically typed languages include Closure Compiler, TypeScript (both for JavaScript),^[6] Hack (for PHP), PHP (since 7.0^[7]), Typed Racket (for Racket), Typed Clojure (for Clojure),^[8] Cython (a Python compiler), mypy (a static type checker for Python)^[9], [https://pyre-check.org/ pyre] (alternative static type checker for Python)^[10], or cperl (a typed Perl 5). ActionScript is a gradually typed language^[11] that is now a dialect of JavaScript, though it originally arose separately as a sibling, both influenced by Apple's HyperTalk.

A system for the J programming language has been developed,^[12] adding coercion, error propagation and filtering to the normal validation properties of the type system as well as applying type functions outside of function definitions, thereby the increasing flexibility of type definitions.

Conversely, C# started as a statically typed language, but as of version 4.0 is gradually typed, allowing variables to be explicitly marked as dynamic by using the dynamic type.^[13] Gradually typed languages not derived from a dynamically typed language include Dart, Dylan, and Perl 6 (influenced by Perl 5, but substantially different).

Objective-C has gradual typing for object pointers with respect to method calls. Static typing is used when a variable is typed as pointer to a certain class of object: when a method call is made to the variable, the compiler statically checks that the class is declared to support such a method, or it generates a warning or error. However, if a variable of the type id is used, the compiler will allow any method to be called on it.

Perl 6 has gradual typing implemented from the start. Type checks occur at all locations where values are assigned or bound. An "untyped" variable or parameter is typed as Any, which will match (almost) all values. The compiler flags typechecking conflicts at compile time if it can determine at compile time that they will never succeed.

References

1. ^{{cite web |url=http://homes.soic.indiana.edu/jsiek/what-is-gradual-typing/ |title=What is gradual typing? |author=Siek, Jeremy}}
2. ^{{cite conference|last1 = Siek|first1=Jeremy|last2=Taha|first2=Walid|title = Gradual Typing for Functional Languages|url=http://scheme2006.cs.uchicago.edu/13-siek.pdf|journal = Scheme and Functional Programming 2006|date = September 2006| pages = 81–92|publisher = University of Chicago}}
3. ^{{cite book|last1 = Thatte|first1=Satish|title = Quasi-static typing|journal = POPL 1990: ACM Principles of Programming Languages|date = 1990| pages = 367–381|publisher = ACM|doi=10.1145/96709.96747|isbn=978-0897913430}}
4. ^{{cite techreport|last=Oliart|first=Alberto|title=An Algorithm for Inferring Quasi-Static Types|number=1994-013|url=http://open.bu.edu/xmlui/handle/2144/1483?show=full|institution=Boston University|year=1994|}}
5. ^{{cite book|last1 = Siek|first1=Jeremy|last2=Taha|first2=Walid|title = Gradual Typing for Objects|journal = ECOOP 2007: European Conference on Object-Oriented Programming|volume=4609|date = August 2007| pages = 2–27|publisher = Springer|doi=10.1007/978-3-540-73589-2_2|series=Lecture Notes in Computer Science|isbn=978-3-540-73588-5}}
6. ^{{Cite conference | doi = 10.1145/2535838.2535889| chapter = Gradual typing embedded securely in JavaScript| title = Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '14| url = http://www.cs.umd.edu/~aseem/tsstar.pdf| pages = 425–437| year = 2014| last1 = Swamy | first1 = N. | last2 = Fournet | first2 = C. | last3 = Rastogi | first3 = A. | last4 = Bhargavan | first4 = K. | last5 = Chen | first5 = J. | last6 = Strub | first6 = P. Y. | last7 = Bierman | first7 = G. | isbn = 9781450325448}}
7. ^{{cite web |url=https://secure.php.net/manual/en/functions.arguments.php#functions.arguments.type-declaration.strict |title=PHP: Function arguments - Manual » Strict typing }}
8. ^{{cite web |url=https://github.com/clojure/core.typed/wiki/User-Guide |title=Typed Clojure User Guide |author=Chas Emerick}}
9. ^{{cite web |url=http://mypy-lang.org/ |title=mypy - Optional Static Typing for Python |author=Jukka Lehtosalo}}
10. ^{{Cite web|url=https://pyre-check.org/|title=Pyre - A performant type-checker for Python 3|last=|first=|date=|website=|archive-url=|archive-date=|dead-url=|access-date=}}
11. ^{{cite web | url = https://www.cs.umd.edu/~avik/papers/iogti.pdf | title = The Ins and Outs of Gradual Type Inference | date = January 2012 | accessdate = 2014-09-23 | author1 = Aseem Rastogi | author2 = Avik Chaudhuri | author3 = Basil Hosmer | publisher = Association for Computing Machinery (ACM) }}
12. ^{{cite web |url= https://github.com/Pascal-J/type-system-j |title= type-system-j}}
13. ^{{cite web |url=http://msdn.microsoft.com/en-us/library/dd264741.aspx |title=dynamic (C# Reference) |work=MSDN Library |publisher=Microsoft |accessdate=14 January 2014}}

Implementation

Examples

References

Further reading