首页 分类 维基 链接 关于
SITEMAP订阅

类型理论

Substructural type system

这是维基百科的介绍。但是里面好多专有名词，在网上找到一些定义的介绍，参考

From Wikipedia, the free encyclopedia

Jump to navigationJump to search

Question book-new.svg This article relies largely or entirely on a single source. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources. Find sources: “Substructural type system” – news · newspapers · books · scholar · JSTOR (February 2018)
   
Type systems
General concepts
Type safetyStrong vs. weak typing
Major categories
Static vs. dynamicManifest vs. inferredNominal vs. structuralDuck typing
Minor categories
AbstractDependentFlow-sensitiveGradualIntersectionLatentRefinementSubstructuralUniqueSession

Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems are useful for constraining access to system resources such as files, locks and memory by keeping track of changes of state that occur and preventing invalid states.[1][2]

Contents

Different substructural type systems[edit]

Several type systems have emerged by discarding some of the structural rules of exchange, weakening, and contraction:

  Exchange Weakening Contraction Use
Ordered — — — Exactly once in order
Linear Allowed — — Exactly once
Affine Allowed Allowed — At most once
Relevant Allowed — Allowed At least once
Normal Allowed Allowed Allowed Arbitrarily

The explanation for affine type systems is best understood if rephrased as “every occurrence of a variable is used at most once”.

Ordered type system[edit]

Ordered types correspond to noncommutative logic where exchange, contraction and weakening are discarded. This can be used to model stack-based memory allocation (contrast with linear types which can be used to model heap-based memory allocation).[3] Without the exchange property, an object may only be used when at the top of the modelled stack, after which it is popped off resulting in every variable being used exactly once in the order it was introduced.

Linear type systems[edit]

Linear types corresponds to linear logic and ensures that objects are used exactly once, allowing the system to safely deallocate an object after its use.[4]

线性类型对应于线性逻辑并确保对象只使用一次，从而允许系统在使用后安全地释放对象。[4]

The Clean programming language makes use of uniqueness types (a variant of linear types) to help support concurrency, input/output, and in-place update of arrays.[5]

Linear type systems allow references but not aliases. To enforce this, a reference goes out of scope after appearing on the right-hand side of an assignment, thus ensuring that only one reference to any object exists at once. Note that passing a reference as an argument to a function is a form of assignment, as the function parameter will be assigned the value inside the function, and therefore such use of a reference also causes it to go out of scope.

A linear type system is similar to C++’s unique_ptr class, which behaves like a pointer but can only be moved (i.e. not copied) in an assignment. Although the linearity constraint is checked at compile time, dereferencing an invalidated unique_ptr causes undefined behavior at run-time.[6]

The single-reference property makes linear type systems suitable as programming languages for quantum computation, as it reflects the no-cloning theorem of quantum states. From the category theory point of view, no-cloning is a statement that there is no diagonal functor which could duplicate states; similarly, from the combinator point of view, there is no K-combinator which can destroy states. From the lambda calculus point of view, a variable x can appear exactly once in a term.[7]

Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories.[8]

Affine type systems[edit]

Affine types are a version of linear types allowing to discard (i.e. not use) a resource, corresponding to affine logic. An affine resource can be used at most once, while a linear one must be used exactly once.

仿射类型是线性类型的一个版本，允许丢弃（即不使用）资源，对应于仿射逻辑。仿射资源可以使用最多一次，而线性的，必须使用完全相同一次

Relevant type system[edit]

Relevant types correspond to relevant logic which allows exchange and contraction, but not weakening, which translates to every variable being used at least once.

Programming languages[edit]

The following programming languages support linear or affine types:

See also[edit]

Notes[edit]

  1. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-FOOTNOTEWalker2002X_1-0) Walker 2002, p. X.
  2. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-FOOTNOTEWalker20024_2-0) Walker 2002, p. 4.
  3. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-FOOTNOTEWalker200230–31_3-0) Walker 2002, pp. 30–31.
  4. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-FOOTNOTEWalker20026_4-0) Walker 2002, p. 6.
  5. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-FOOTNOTEWalker200243_5-0) Walker 2002, p. 43.
  6. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-6) std::unique_ptr reference
  7. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-7) John c. Baez and Mike Stay, “Physics, Topology, Logic and Computation: A Rosetta Stone”, (2009) ArXiv 0903.0340 in New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174.
  8. [^](https://en.wikipedia.org/wiki/Substructural_type_system#cite_ref-8) S. Ambler, “First order logic in symmetric monoidal closed categories”, Ph.D. thesis, U. of Edinburgh, 1991.

References[edit]

学校的课程

https://groups.seas.harvard.edu/courses/cs152/2021sp/

Course information

This course is an introduction to the theory, design, and implementation of programming languages. Topics covered in this course include: formal semantics of programming languages (operational, axiomatic, denotational, and translational), type systems, higher-order functions and lambda calculus, laziness, continuations, dynamic types, monads, objects, modules, concurrency, and communication.

本课程介绍编程语言的理论、设计和实现。 本课程涵盖的主题包括：编程语言的形式语义（操作、公理、指称和翻译）、类型系统、高阶函数和 lambda 演算、惰性、延续、动态类型、单子、对象、模块、并发性和 沟通。

See the lecture schedule for more detailed information on topics covered.

Resources

Text books

A number of excellent books and on-line resources overlap with the course’s content and can provide alternate explanations despite differences in notation and approach. Let the instructor know if you have trouble finding the intersection between these resources and the course content.

OCaml resources

See also the CS51 Resources web page for OCaml books, references, and tutorials.

Coq resources

Dafny resources

Haskell resources

lectures

NOTE: The current schedule is tentative and subject to change. Nonetheless it gives an idea of the material to be covered in this course. The lecture notes are seeded from previous years, and will be sporadically updated.

Key to readings: P = Pierce; SF = Software Foundations; M = Mitchell; W = Winskel; K = Krishnamurthi 1st ed.; K2nd = Krishnamurthi 2nd ed.; H = Harper. The readings are not required, but may help your understanding of the lecture material.

The lecture notes here contain material from lecture notes by Stephen Chong, Radu Rugina, Andrew Myers, Nate Foster, and Jeff Vaughan.

Videos of the lecture and sections are available on Canvas. The same site also provides a Zoom link for live streaming of and remote participation in lectures.

For background material on sets, relations, functions, and induction, see: W 1, H 2, H Appendix, and/or P 2.

Lec. Date Topic Readings Notes Slides Code Assignments
Semantics              
1 Tue 26-Jan Intro to semantics, Proof tools P 2.4, 3 SF1-Induction,Imp SF2-SmallStep W 2,3,4 H 2   PDF OCaml Coq  
2 Thu 28-Jan Small-step semantics PDF PDF Coq    
3 Tue 2-Feb Induction PDF PDF Coq Assignment 1 released  
4 Thu 4-Feb Large-step semantics PDF PDF Coq    
5 Tue 9-Feb IMP: a simple imperative language PDF PDF Coq    
6 Thu 11-Feb Denotational semantics W 5 M 4.3 PDF PDF    
Lambda calculus              
7 Tue 16-Feb Lambda calculus P 5 M 4.2 K 22 PDF PDF    
8 Thu 18-Feb Lambda calculus encodings and Recursion PDF PDF      
9 Tue 23-Feb Definitional translations   PDF PDF    
10 Thu 25-Feb References and continuations P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 PDF PDF   Assignment 1 due Assignment 2 released
Types              
11 Tue 2-Mar Simply-typed lambda calculus Type soundness P 9 SF2-Stlc SF2-StlcProp M 6.1, 6.2 K 24-26(P 12) (SF2-Norm) PDF PDF    
13 Thu 4-Mar More types P 11, 13 SF2-MoreStlc SF2-References PDF PDF    
12 Tue 9-Mar NO CLASS MIDTERM          
14 Thu 11-Mar Parameteric Polymorphism, Records and Subtyping P 23 M 6.4 P 11.8, 15 PDF PDF   Assignment 3 released
No Class              
15 Thu 18-Mar Curry-Howard isomorphism; Existential types P 9.4 SF1-ProofObjects PDF PDF Haskell Assignment 2 due
16 Tue 23-Mar Type Inference P 22 K30 PDF PDF Prolog  
17 Thu 25-Mar Sub-structural type systems   PDF PDF eg1.rs eg2.rs eg3.rs eg4.rs eg5.rs Assignment 3 due Assignment 4 released
18 Tue 30-Mar Algebraic structures   PDF PDF m.hs agediff.hs io.hs state.hs  
Reasoning About Programs              
19 Thu 1-Apr Axiomatic Semantics and Hoare Logic SF2-Hoare W 6 (W 7) PDF PDF hoare.c hoare.dfy factorial.c factorial.dfy  
20 Tue 6-Apr Dependent types   PDF PDF Twelf  
0 Thu 8-Apr Embedded EthiCS: Specifications of Ethical Concerns         Assignment 4 due Assignment 5 released
Misc. Topics              
21 Tue 13-Apr Logic Programming (Guest appearance: Will Byrd) M 15 K32-34 PDF      
No Class              
22 Tue 20-Apr Probabilistic Programming (Guest lecturer: Yizhou Zhang)     PDF    
25 Thu 22-Apr Semantics for Verified Software-Hardware Stacks (Guest lecturer: Samuel Gruetter)         Assignment 5 due Assignment 6 released
24 Tue 27-Apr Concurrency M 14 PDF PDF ex1.go ex2.go ex3.go  
  Thu 29-Apr           Assignment 6 due
  TBD TBD-May FINAL EXAM: TBD          

Published on Sep 18, 2021 in categories

Powered by Jekyll and Theme by solid

本站总访问量次