하부구조형 시스템

Substructural type system
유형 시스템
일반적인 개념
주요 카테고리
마이너 카테고리

서브구조형 시스템은 하나 이상의 구조 규칙이 없거나 통제된 상황에서만 허용되는 서브구조 로직스와 유사한 유형 시스템 패밀리입니다.이러한 시스템은 발생하는 상태 변화를 추적하고 비활성 상태를 [1]방지함으로써 파일, 잠금 및 메모리 등의 시스템 리소스에 대한 액세스를 제한할 때 유용합니다.

다른 하부구조형 시스템

교환, 약화 및 수축의 구조적 규칙 중 일부를 폐기함으로써 다음과 같은 여러 유형의 시스템이 등장했습니다.

교환하다 약해지다 수축 사용하다
주문된 — — — 딱 한 번만
선형 허용된 — — 딱 한 번
아핀 허용된 허용된 — 한 번에
관련된 허용된 — 허용된 한 번쯤은
보통의 허용된 허용된 허용된 임의로
  • 주문형 시스템(폐기 교환, 약화 및 수축):모든 변수는 처음 도입된 순서대로 정확히 한 번 사용됩니다.
  • 선형 시스템(교환은 가능하지만 약해지거나 수축하지는 않음):모든 변수는 정확히 한 번 사용됩니다.
  • 아핀형 시스템(교환 및 약화를 허용하지만 수축은 허용하지 않음):모든 변수는 최대 한 번에 사용됩니다.
  • 관련 유형 시스템(교환 및 수축이 가능하지만 약해지지는 않음):모든 변수는 적어도 한 번 사용됩니다.
  • 일반형 시스템(교환, 약화 및 수축 가능):모든 변수는 임의로 사용할 수 있습니다.

아핀 유형 시스템에 대한 설명은 "변수의 모든 발생이 최대 한 번에 사용된다"로 바꿔 말하면 가장 잘 이해할 수 있습니다.

주문형 시스템

순서형은 교환, 수축 및 약화가 폐기되는 비가환 논리에 대응합니다.이는 스택 기반 메모리 할당 모델링에 사용할 수 있습니다(히프 기반 메모리 [2]할당 모델링에 사용할 수 있는 선형 유형과의 대비).교환 속성이 없으면 오브젝트는 모델링된 스택의 맨 위에 있을 때만 사용할 수 있습니다.이 후 오브젝트가 팝업되고 모든 변수가 추가된 순서대로 정확히 한 번 사용됩니다.

선형 시스템

선형 유형은 선형 논리에 해당하며 개체가 정확히 한 번만 사용됩니다.이를 통해 객체 사용 [3]후 안전하게 할당 해제하거나 리소스가 닫히거나 다른 [4]상태로 전환되면 사용할 수 없도록 보장하는 소프트웨어 인터페이스를 설계할 수 있습니다.

Clean Programming Language에서는 고유 유형(선형 유형의 배리언트)을 사용하여 [5]어레이의 동시성, 입출력 및 인플레이스 업데이트를 지원합니다.

선형 유형 시스템에서는 참조를 허용하지만 별칭은 허용하지 않습니다.이를 적용하기 위해 참조는 할당 오른쪽에 표시된 후 범위를 벗어나므로 한 번에 하나의 개체에 대한 참조만 존재합니다.참조를 인수로 함수에 전달하는 것은 할당의 한 형태입니다.이는 함수 파라미터에 함수 내부의 값이 할당되기 때문입니다.따라서 참조를 사용하면 해당 파라미터도 범위를 벗어납니다.

선형 유형 시스템은 포인터처럼 동작하지만 할당 내에서 이동(복사되지 않음)만 가능한 C++의 unique_ptr 클래스와 유사합니다.선형성 제약조건은 컴파일 시에 체크되지만 무효화된 unique_ptr을 참조하면 [6]런타임에 정의되지 않은 동작이 발생합니다.마찬가지로 Rust 프로그래밍 언어에서는 보풀 주석을[7] 사용하여 선형 유형을 부분적으로 지원하지만 C++와 달리 변수에서 이동된 변수를 [8]다시 사용할 수 없습니다.

단일 참조 특성은 양자 상태의 무복제 정리를 반영하기 때문에 선형형 시스템을 양자 계산을 위한 프로그래밍 언어로 적합하게 만든다.범주 이론의 관점에서, 무복제는 상태를 복제할 수 있는 대각 함수가 없다는 진술이다. 마찬가지로, 조합 논리의 관점에서, 상태를 파괴할 수 있는 K-콤비네이터는 없다.람다 미적분의 관점에서 변수 x는 한 [9]항에 정확히 한 번 나타날 수 있습니다.

선형 유형 시스템은 닫힌 대칭 모노이드 범주의 내부 언어이며, 단순하게 유형화된 람다 미적분이 데카르트 닫힌 범주의 언어인 것과 거의 같은 방식이다.보다 정확하게는 선형 유형 시스템의 범주와 닫힌 대칭 모노이드 [10]범주 사이에 함수를 구성할 수 있다.

아핀형 시스템

아핀 타입은 아핀 로직에 대응하는 자원을 폐기(사용하지 않음)할 수 있는 선형 타입의 버전입니다.아핀 리소스는 한 번만 사용할 수 있지만 선형 리소스는 한 번만 사용해야 합니다.

관련 유형 시스템

관련 유형은 교환과 수축을 허용하지만 약해지지는 않는 관련 논리에 해당하며, 이는 모든 변수가 적어도 한 번 사용되는 것으로 해석됩니다.

프로그래밍 언어

다음 프로그래밍 언어는 선형 또는 아핀 유형을 지원합니다.

「 」를 참조해 주세요.

메모들

  1. ^ 워커 2002, 페이지 4
  2. ^ 워커 2002, 페이지 30-31.
  3. ^ 워커 2002, 6페이지
  4. ^ Bernardy et al. 2017.
  5. ^ 워커 2002, 페이지 43
  6. ^ std::syslog_ptr 참조
  7. ^ 필수_사용
  8. ^ Rust 및 C++에서 의미론 이동
  9. ^ Baez & Stay 2010.
  10. ^ 앰블러 1991년
  11. ^ Haskell 9.0.1 릴리즈 노트

레퍼런스

  • Walker, David (2002). "Substructural Type Systems". In Pierce, Benjamin C. (ed.). Advanced Topics in Types and Programming Languages (PDF). MIT Press. pp. 3–43. ISBN 0-262-16228-8.
  • Bernardy, Jean-Philippe; Boespflug, Mathieu; Newton, Ryan R; Peyton Jones, Simon; Spiwack, Arnaud (2017). "Linear Haskell: practical linearity in a higher-order polymorphic language". Proceedings of the ACM on Programming Languages. 2: 1–29. arXiv:1710.09756. doi:10.1145/3158093. S2CID 9019395.
  • Ambler, S. (1991). First order logic in symmetric monoidal closed categories (PhD). U. of Edinburgh.
  • Baez, John C.; Stay, Mike (2010). "Physics, Topology, Logic and Computation: A Rosetta Stone". In Springer (ed.). New Structures for Physics (PDF). pp. 95–174.