밑단형

Bottom type

유형 이론, 수학 논리 내부의 이론에서, 하단 유형은 값이 없는 유형이다.0형 또는 빈형이라고도 하며, 업태크(업태크) 기호로 표시되기도 한다.

반환 유형이 최하위(확실히)인 함수는 0사이즈 단위 유형도 아니고 값을 반환할 수 없다.따라서 반환 유형이 하단 유형인 함수는 반환할 수 없다.Curry-Howard 통신에서, 하단 유형은 위조에 해당한다.

컴퓨터 과학 응용 프로그램

서브타이핑 시스템에서 하단 유형은 모든 유형의 하위 유형이다.[1](단, 역은 사실이 아니다. 모든 유형의 하위 유형이 반드시 하의 유형은 아니다.)값을 반환하지 않는 함수의 반환 유형을 나타내는 데 사용된다. 예를 들어, 영구적으로 루프하거나 예외를 신호하거나 종료하는 함수의 반환 형식을 나타내기 위해 사용된다.

바닥 타입은 정상적인 수익률이 없음을 나타내는 데 사용되기 때문에, 일반적으로 값이 없다.이것은 시스템에서 가능한 모든 값을 포함하는 상위 유형과 정확히 하나의 값을 갖는 단위 유형과 대조된다.

아래 유형은 다음과 같은 목적으로 자주 사용된다.

  • 함수 또는 계산이 분산된다는 신호, 즉, 호출자에게 결과를 반환하지 않는다. (이는 프로그램이 종료되지 않는다는 것을 반드시 의미하지는 않는다. 서브루틴은 호출자에게 돌아가지 않고 종료되거나 계속과 같은 다른 방법을 통해 종료될 수 있다.)
  • 오류의 표시로서, 이러한 용법은 주로 오류를 구분하는 것이 중요하지 않은 이론적인 언어에서 발생한다.프로덕션 프로그래밍 언어는 일반적으로 옵션 유형(태그된 포인터 포함) 또는 예외 처리와 같은 다른 방법을 사용한다.

Bottom과의 Bounded Quantification에서 [1]Pierce는 "Bot"은 많은 용도를 가지고 있다고 말한다.

  1. 예외를 가진 언어에서 상승구조의 자연형태는 상승 예외 -> Bot이며, 다른 제어구조의 경우도 이와 유사하다.직관적으로, 여기서 Bot은 답을 돌려주지 않는 계산의 유형이다.
  2. Bot는 다형성 데이터 구조의 "leaf node"를 입력하는 데 유용하다.예를 들어, List(Bot)는 nil에 좋은 유형이다.
  3. Bot는 Java와 같은 언어의 "null pointer" 값(아무 개체도 가리키지 않는 포인터)의 자연형이다: 자바에서 null 유형은 참조 유형의 보편적인 하위형이다. nullnull 유형의 유일한 값이며, 모든 참조 유형에 캐스팅할 수 있다.[3]그러나 null 유형은 가능한 값을 가질 수 없고 null 유형은 값을 가지기 때문에 위에서 설명한 바와 같이 bottom type의 모든 속성을 만족시키지 못한다.null.
  4. Top과 Bot을 모두 포함하는 형식 시스템은 생략된 형식 매개 변수에 대한 제약 조건을 한 쌍의 경계로 포착할 수 있도록 하는 형식 추론의 자연스러운 목표인 것 같다. 우리는 S<:X<::::"X의 값은 S와 T 사이에 있어야 한다"는 뜻의 T. 그러한 계획에서 완전히 구속되지 않는 매개변수는 Bot에 의해 아래, 위는 Top에 의해 제한된다.

프로그래밍 언어에서

가장 일반적으로 사용되는 언어는 빈 유형을 명시적으로 나타내는 방법이 없다.몇 가지 주목할 만한 예외가 있다.

Haskell2010년부터 Haskell은 빈 데이터 유형을 지원한다.따라서, 그것은 그 정의를 허용한다.data Empty(시공자 없음).유형Empty비응시 프로그램, 비응시 프로그램 등을 포함하고 있어, 그다지 비어 있지 않다.undefined상수의그undefined상수는 종종 어떤 것이 빈 타입을 갖기를 원할 때 사용된다. 왜냐하면undefined모든 유형과 일치하고(모든 유형의 "하위 유형"의 일종임) 평가 시도undefined프로그램을 중단하게 할 것이고, 따라서 그것은 결코 답을 돌려주지 않을 것이다.

Common Lisp에서 기호NIL그것의 다른 용도들 중에서, 또한 값이 없는 유형의 이름이다.의 보완책이다.T어떤 타입이 제일 좋은지.명명된 유형NIL때때로 이름이 붙은 유형과 혼동되기도 한다.NULL, 하나의 값, 즉 기호를 가지고 있다.NIL그 자체로

스칼라에서 아래쪽 유형은 다음과 같이 표시된다.Nothing . 예외를 발생시키거나 그렇지 않으면 정상적으로 복귀하지 않는 기능에 사용되는 것 외에도 공변량 매개변수 유형에도 사용된다.예를 들어 스칼라의 목록은 공변량 유형 생성자이므로List[Nothing]의 하위 유형이다.List[A]모든 타입 A에 대하여그래서 스칼라의Nil, 모든 유형의 목록 끝을 표시하는 개체는 유형에 속함List[Nothing].

러스트에서는 밑의 타입을 never type이라고 하며, 에 의해 표시된다.!. 예를 들어, 전화를 걸어 다시는 돌아오지 않을 것을 보증하는 기능의 유형 서명에 존재한다.panic!()영원히 루핑을 할 수도 있어또한 다음과 같은 특정 제어 흐름 키워드의 유형이기도 하다.break그리고return값을 생성하지는 않지만 표현으로 사용할 수 있는 값.[4]

실론에서는 밑단 타입이Nothing에 [5]필적할 만하다Nothing스칼라에서 빈 집합뿐만 아니라 다른 모든 유형의 교차점을 나타낸다.

줄리아에서는 밑의 타입은Union{}.[6]

TypeScript에서 아래쪽 유형은never.[7][8]

Closure Compiler 주석이 있는 JavaScript에서 아래쪽 유형은!Null(iii, non-temperative ember of the)Null 단위 유형).

PHP에서 아래쪽 유형은never.

Python에서 아래 타입은typing.NoReturn.[9]

코틀린에서는 밑단 타입이Nothing.[10]

Elm에서 아래쪽 유형은Never.[11]

참고 항목

참조

  1. ^ a b Pierce, Benjamin C. (1997). "Bounded Quantification with Bottom". CiteSeerX 10.1.1.17.9230. {{cite journal}}:Cite 저널은 필요로 한다. journal=(도움말)
  2. ^ Griffin, Timothy G. (1990). "The Formulae-as-Types Notion of Control". Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17-19 Jan 1990. pp. 47–57.
  3. ^ "Section 4.1: The Kinds of Types and Values". Java Language Specification (3rd ed.).
  4. ^ "Primitive Type never". The Rust Standard Library Documentation. Retrieved 2020-09-24.
  5. ^ "Chapter 3. Type system — 3.2.5. The bottom type". The Ceylon Language. Red Hat, Inc. Retrieved 2017-02-19.
  6. ^ "Essentials - The Julia Language", The Julia Programming Language Documentation, retrieved 2021-08-13
  7. ^ The never type, TypeScript 2.0 release notes, Microsoft, 2016-10-06, retrieved 2019-11-01
  8. ^ The never type, TypeScript 2.0 release notes, source code, Microsoft, 2016-10-06, retrieved 2019-11-01
  9. ^ typing.NoReturn, typing — Support for type hints, Python documentation, Python Software Foundation, retrieved 2020-02-25
  10. ^ Nothing, retrieved 2020-05-15
  11. ^ Never, retrieved 2021-03-25

추가 읽기