shopkeeper/korean_wiki_content_only_120125 huggingface dataset:
1세대 TIROS 우주선의 위성 버스는 직경 약 및 높이 의 18면체 각기둥 모양이었다. 알루미늄 합금과 스테인리스강으로 제작된 각 우주선은 약 의 무게였다. 위성은 니켈-카드뮴 전지로 구동되었으며, 이는 우주선 측면에 장착된 9,200개의 태양 전지에 의해 충전되었다. TIROS 우주선은 스핀 안정화를 유지하기 위해 8-12 rpm으로 회전하도록 설계되었다. 장비 하우징의 바닥판에 장착된 한 쌍의 고체 로켓은 한 번에 한 쌍씩 발사되어 회전 속도 저하를 상쇄하기 위해 회전율을 3 rpm 증가시킬 수 있었다. 첫 8개의 TIROS 위성에 장착된 카메라는 또한 바닥판에 위치하며 우주선의 회전축과 평행하게 정렬되었다. 1세대 TIROS에는 자세 제어 기능이 없었기 때문에 지구는 위성 궤도의 일부 동안에만 카메라의 시야에 들어왔으며, 위성은 설계상 전체 서비스 수명 동안 우주에 대해 고정된 방향을 유지했다. 지자기와의 상호 작용으로 인해 TIROS-1의 회전축이 진동했다. TIROS-2에 도입되어 TIROS-8까지 유지된 자력 토커는 우주선 자체의 자기장을 점진적으로 변화시켜 궤도당 1.5°의 우주선 자세 변경을 가능하게 했다. Quarter Orbit Magnetic Attitude Control System이라는 더 강력한 자기 시스템이 TIROS-9에 도입되어 더 빠르고 정밀한 자세 제어를 가능하게 하고 우주선 스핀 축을 최대 10°까지 변경할 수 있도록 했다. TIROS-9의 카메라는 바닥판 대신 우주선 측면에 방사형으로 부착되었다. 이전 TIROS 우주선의 "축" 구성과 대조적으로 이 "바퀴" 구성은 지구의 더 빈번한 이미지를 가능하게 했다.
1세대 TIROS 위성은 두 대의 직경 비디콘 라인 스캔 카메라를 탑재했으며, 일반적으로 다른 분해능을 지원하는 다른 시야를 가졌다. 초기 TIROS 반복에 사용된 자기 테이프 레코더는 고정된 30초 간격으로 촬영된 총 64장의 사진을 저장할 수 있었으며, 이는 최대 2궤도 데이터에 해당한다. TIROS-9부터는 이미지 저장 용량이 96장으로 증가했으며, 시계 시스템 구현으로 이미지 간의 가변 간격이 가능해졌다. 카메라 셔터는 위성이 지상 명령 지점에 접근할 때 2와트 FM 송신기를 통해 지구로 저장 및 전송되는 일련의 정지 사진을 가능하게 했다. 전송 후 테이프는 지워지거나 청소되어 추가 기록을 위해 준비되었다. TIROS-8은 새로운 APT 시스템의 시험 운행 역할을 했으며, 온보드 저장 장치에 의존하지 않고 이미지를 쉽게 방송하고 수신할 수 있게 했다. 후속 TIROS 우주선은 APT 시스템을 유지했으며, 온보드 시스템 및 지상국 네트워크 확장 모두에서 개선이 이루어졌다. 일부 초기 TIROS 우주선에는 5채널 중해상도 적외선 스캔 복사계와 저해상도 복사계도 포함되었다. 5채널 복사계는 주야간 운량 관측을 가능하게 했다. 데이터는 우주선 바닥판에서 튀어나온 4개의 무선 안테나를 통해 전송되었으며, 상단판 중앙에 단일 수신 안테나가 장착되었다.
첫 열 번의 TIROS 임무는 고도 약 의 원형 태양 동기 궤도를 취하도록 계획되었다. TIROS-9 발사 시스템의 2단계 과성능으로 인해 해당 우주선이 타원 궤도에 잘못 배치되었다. 첫 네 개의 TIROS 위성은 적도에 대해 48°의 궤도 경사를 가진 원형 궤도에 발사되어 55°N에서 55°S 사이의 지구를 커버했다. TIROS 프로그램에 선택된 Thor-Delta 발사체의 동시 개선으로 후기 페이로드의 궤도 경사를 증가시킬 수 있었다. TIROS-5부터 TIROS-8까지의 다음 네 개의 위성은 58°의 더 높은 경사를 가졌으며, 위성 커버리지를 65°N–65°S로 확장했다. TIROS-9와 TIROS-10은 적도에 대해 98°의 거의 극궤도 경사를 가진 지구의 주간 면을 완전히 커버했다. 첫 8개의 TIROS 위성과 그 궤도의 방향은 지구의 햇빛 비추는 부분의 관측 가능한 부분을 제한했으며, 수개월 동안 궤도 세차에 의존하여 북반구와 남반구 모두의 영역을 커버했다.
2009년 6월 기준으로 1960년부터 1965년 사이에 발사된 모든 TIROS 위성(TIROS-7 제외)은 여전히 궤도에 있었다.
고급 TIROS-N.
고급 TIROS-N(ATN) 우주선은 추가 페이로드 통합을 위해 확장된 장비 지원 모듈을 제외하고 NOAA-A부터 -D 위성과 유사했다. TIROS-N부터 NOAA-D 우주선과의 변경 사항은 저속 데이터 시스템 TIROS 정보 프로세서(TIP)의 예비 단어 위치가 지구 복사 에너지 위성(ERBE) 및 SBUV/2와 같은 특수 장비에 사용되었다는 점이다. 수색 및 구조(SAR) 시스템은 지상으로 데이터를 전송하기 위한 특수 주파수를 사용하여 독립적으로 작동하게 되었다.
컴퓨터 과학에서 자료형 안전 또는 타입 안정성(type safety)은 프로그래밍 언어가 타입 오류를 방지하거나 막는 정도를 말한다. 타입 안전 언어는 때때로 강력하게 또는 엄격하게 타입이 지정된 언어라고도 불린다. 주어진 프로그래밍 언어에서 타입 오류로 분류되는 동작은 일반적으로 적절한 자료형이 아닌 값에 대해 연산을 수행하려는 시도로 인해 발생하는 것이다. 예를 들어, 문자열을 정수형에 더하려고 하는 경우 등이 있다.
타입 강제는 정적(잠재적 오류를 컴파일 타임에 잡아냄), 동적(런타임에 값과 타입 정보를 연결하고 필요에 따라 임박한 오류를 감지하기 위해 이를 참조함), 또는 둘의 조합일 수 있다. 동적 타입 강제는 정적 강제 하에서는 유효하지 않을 프로그램을 실행할 수 있지만, 런타임에 오류를 발생시킬 수 있다는 단점이 있다.
정적(컴파일 타임) 타입 시스템의 맥락에서 타입 안전성은 일반적으로 (다른 것들과 함께) 어떤 식의 최종 값이 그 식의 정적 타입의 합법적인 멤버가 될 것이라는 보장을 포함한다. 정확한 요구사항은 이보다 더 미묘한데, 예를 들어 서브타이핑과 다형성과 같은 복잡성을 참조하라.
직관적으로 타입 건전성은 로빈 밀너의 간결한 진술에 포착되어 있다.
다시 말해, 타입 시스템이 건전하다면, 그 타입 시스템에 의해 허용된 식은 적절한 타입의 값으로 평가되어야 한다(다른 무관한 타입의 값을 생성하거나 타입 오류로 인해 충돌하는 대신). 비자이 사라사와트는 다음과 같은 관련 정의를 제공한다.
그러나 프로그램이 "타입이 잘 지정되었다"거나 "잘못된다"는 것이 정확히 무엇을 의미하는지는 해당 프로그래밍 언어에 특정한 정적 및 동적 의미론의 속성이다. 따라서 타입 건전성에 대한 정확하고 형식적인 정의는 언어를 지정하는 데 사용되는 형식 의미론의 스타일에 따라 달라진다. 1994년에 앤드류 라이트와 마티아스 펠라이젠은 동작적 의미론에 의해 정의된 언어에서 타입 안전성에 대한 표준 정의 및 증명 기법을 공식화했다. 이는 대부분의 프로그래머가 이해하는 타입 안전성 개념에 가장 가깝다. 이 접근 방식에 따라 언어의 의미론은 타입 건전하다고 간주되기 위해 다음 두 가지 속성을 가져야 한다.
타입 건전성에 대한 여러 다른 형식적 처리 방법도 표시적 의미론 및 구조적 동작 의미론의 관점에서 발표되었다.
다른 형태의 안전성과의 관계.
고립된 상태에서 타입 건전성은 비교적 약한 속성이다. 본질적으로 타입 시스템의 규칙이 내부적으로 일관되며 전복될 수 없음을 나타낼 뿐이기 때문이다. 그러나 실제로는 프로그래밍 언어가 잘 타입화되면 다른 더 강력한 속성도 수반하도록 설계되며, 그 중 일부는 다음과 같다.
타입 안전 언어와 타입 불안전 언어.
타입 안전성은 일반적으로 학술 프로그래밍 언어 연구에서 제안되는 모든 장난감 언어(즉, 난해한 프로그래밍 언어)의 요구 사항이다. 반면에 많은 언어는 인간이 생성하는 타입 안전성 증명에는 너무 커서 수천 가지 경우를 확인해야 하는 경우가 많다. 그럼에도 불구하고, 엄격하게 정의된 의미론을 가진 표준 ML과 같은 일부 언어는 타입 안전성의 한 가지 정의를 충족하는 것으로 입증되었다. 하스켈과 같은 일부 다른 언어는 특정 "탈출" 기능이 사용되지 않는 한 타입 안전성의 어떤 정의를 충족한다고 여겨진다(예를 들어, I/O가 가능한 일반적인 제한된 환경에서 "탈출"하는 데 사용되는 하스켈의 는 타입 시스템을 우회하여 타입 안전성을 깨뜨릴 수 있다.) 타입 펀닝은 이러한 "탈출" 기능의 또 다른 예이다. 언어 정의의 속성과 관계없이 구현의 버그나 다른 언어로 작성된 연결된 라이브러리로 인해 런타임에 특정 오류가 발생할 수 있다. 이러한 오류는 특정 상황에서 주어진 구현을 타입 불안전하게 만들 수 있다. 초기 버전의 선 마이크로시스템즈 자바 가상 머신은 이러한 종류의 문제에 취약했다.
프로그래밍 언어는 종종 타입 안전성의 특정 측면을 지칭하기 위해 강력하게 타입이 지정되었거나 약하게 타입이 지정되었다(느슨하게 타입이 지정되었다고도 함)고 통속적으로 분류된다. 1974년에 리스코프와 질레스는 강력하게 타입이 지정된 언어를 "객체가 호출 함수에서 호출된 함수로 전달될 때마다 그 타입이 호출된 함수에 선언된 타입과 호환되어야 하는" 언어라고 정의했다.
1977년에 잭슨은 "강력하게 타입이 지정된 언어에서는 각 데이터 영역이 고유한 타입을 가지며 각 프로세스는 이러한 타입의 관점에서 통신 요구 사항을 명시할 것이다"라고 썼다.
대조적으로, 약하게 타입이 지정된 언어는 예측할 수 없는 결과를 생성하거나 암시적 타입 변환을 수행할 수 있다.
메모리 관리 및 자료형 안전.
자료형 안전은 메모리 보안과 밀접하게 연관되어 있다. 예를 들어, 특정 비트 패턴은 허용하지만 다른 비트 패턴은 허용하지 않는 타입 formula_1를 가진 언어의 구현에서, 허상 포인터 메모리 오류는 formula_1 타입의 죽은 변수에 formula_1의 유효한 멤버를 나타내지 않는 비트 패턴을 쓰는 것을 허용하여, 변수를 읽을 때 타입 오류를 유발한다. 반대로, 언어가 메모리 안전하다면, 임의의 정수를 포인터로 사용하는 것을 허용할 수 없으므로, 별도의 포인터 또는 참조 타입이 있어야 한다.
최소한의 조건으로, 타입 안전 언어는 다른 타입의 할당에 걸쳐 허상 포인터를 허용해서는 안 된다. 그러나 대부분의 언어는 메모리 안전성이나 어떤 종류의 치명적인 오류 방지를 위해 엄격하게 필요하지 않더라도 프로그래머가 정의한 추상 자료형의 적절한 사용을 강제한다. 할당은 그 내용물을 설명하는 타입을 부여받으며, 이 타입은 할당 기간 동안 고정된다. 이를 통해 타입 기반의 별칭 분석이 다른 타입의 할당이 구별된다고 추론할 수 있다.
대부분의 타입 안전 언어는 쓰레기 수집을 사용한다. 피어스(Pierce)는 허상 포인터 문제 때문에 "명시적인 할당 해제 연산이 있는 상황에서 타입 안전성을 달성하는 것은 극히 어렵다"고 말한다. 그러나 러스트는 일반적으로 타입 안전하다고 여겨지며, 쓰레기 수집 대신 빌림 검사기(borrow checker)를 사용하여 메모리 안전성을 달성한다.
객체 지향 언어의 타입 안전성.
객체 지향 언어에서 타입 안전성은 일반적으로 자료형 체계가 존재한다는 사실에 내재되어 있다. 이는 클래스 정의 측면에서 표현된다.
클래스는 본질적으로 그로부터 파생된 객체들의 구조와 이 객체들을 처리하기 위한 계약으로서의 API를 정의한다. 새로운 객체가 생성될 때마다 그 계약을 준수하게 된다.
특정 클래스에서 파생되거나 특정 인터페이스를 구현하는 객체를 교환하는 각 함수는 해당 계약을 준수할 것이다. 따라서 해당 함수에서 해당 객체에 허용되는 연산은 객체가 구현하는 클래스의 메서드에 의해 정의된 것들뿐이다.
이는 객체의 무결성이 보존되도록 보장할 것이다.
이것에 대한 예외는 객체 구조의 동적 수정을 허용하는 객체 지향 언어나, 클래스 메서드 정의에 의해 부과된 제약을 극복하기 위해 리플렉션을 사용하여 객체의 내용을 수정하는 경우이다.
특정 언어의 타입 안전성 문제.
에이다는 임베디드 시스템, 장치 드라이버 및 기타 형태의 시스템 프로그래밍에 적합하도록 설계되었지만, 타입 안전 프로그래밍을 장려하도록 설계되기도 했다. 이러한 상충되는 목표를 해결하기 위해 에이다는 타입 불안전성을 보통 문자열로 시작하는 이름의 특정 특수 구성 집합으로 제한한다. Unchecked_Deallocation은 이 유닛에 를 적용함으로써 에이다 텍스트 유닛에서 효과적으로 금지될 수 있다. 프로그래머는 구성을 매우 신중하게, 그리고 필요한 경우에만 사용할 것으로 예상된다. 이를 사용하지 않는 프로그램은 타입 안전하다.
SPARK 프로그래밍 언어는 에이다의 모든 잠재적 모호성과 불안정성을 제거하면서 동시에 언어 기능에 정적으로 검사되는 계약을 추가한 에이다의 부분 집합이다. SPARK는 런타임에 할당을 완전히 허용하지 않음으로써 허상 포인터 문제를 피한다.
에이다 2012는 언어 자체에 정적으로 검사되는 계약을 추가한다 (사전 및 사후 조건, 그리고 타입 불변식의 형태로).
C 프로그래밍 언어는 제한된 맥락에서 타입 안전하다. 예를 들어, 명시적 캐스트가 사용되지 않는 한 한 타입의 구조체에 대한 포인터를 다른 타입의 구조체에 대한 포인터로 변환하려는 시도는 컴파일 타임 오류를 발생시킨다. 그러나 많은 일반적인 연산은 타입 안전하지 않다. 예를 들어, 정수를 출력하는 일반적인 방법은 codice_2와 같은데, 여기서 codice_3는 codice_4에게 런타임에 정수 인수를 예상하도록 지시한다. (codice_5와 같은, 함수에게 문자열에 대한 포인터를 예상하도록 지시하면서 정수 인수를 제공하는 것은 컴파일러에 의해 허용될 수 있지만, 정의되지 않은 결과를 생성할 것이다.) 이는 일부 컴파일러(예: gcc)가 printf 인수와 형식 문자열 간의 타입 일치 여부를 확인함으로써 부분적으로 완화된다.
또한, C는 에이다와 마찬가지로 명시적이고 불분명하거나 정의되지 않은 변환을 제공한다. 그리고 에이다와는 달리, 이러한 변환을 사용하는 관용구는 매우 흔하며, C에 타입 불안전하다는 평판을 안겨주는 데 일조했다. 예를 들어, 힙에 메모리를 할당하는 표준적인 방법은 필요한 바이트 수를 나타내는 인자와 함께 codice_6과 같은 메모리 할당 함수를 호출하는 것이다. 이 함수는 void 포인터 (codice_7)를 반환하며, 호출 코드는 이를 명시적으로 또는 암시적으로 적절한 포인터 타입으로 캐스트해야 한다. C의 표준화 이전 구현에서는 이를 위해 명시적 캐스트가 필요했으므로, codice_8의 할당을 위해 codice_9 코드가 일반적인 관행이 되었다. codice_10은 codice_7를 반환하며 C에서는 명시적으로 캐스트할 필요가 없지만, C++에서는 타입 안전성을 위해 이 캐스팅이 의무화된다.
보다 타입 안전한 코드를 촉진하는 C++의 일부 기능:
C 샤프는 타입 안전하다. 타입이 지정되지 않은 포인터를 지원하지만, 이는 컴파일러 수준에서 금지될 수 있는 "unsafe" 키워드를 사용하여 접근해야 한다. 런타임 캐스트 유효성 검사를 위한 내재적 지원을 제공한다. 캐스트는 유효하지 않은 경우 null 참조를 반환하는 "as" 키워드를 사용하거나, 유효하지 않은 경우 예외를 발생시키는 C 스타일 캐스트를 사용하여 유효성을 검사할 수 있다. C 샤프 변환 연산자를 참조하라.
모든 다른 타입이 파생되는 객체 타입에 과도하게 의존하는 것은 C# 타입 시스템의 목적을 무력화시킬 위험이 있다. 일반적으로 .NET의 제네릭 프로그래밍|제네릭을 선호하여 객체 참조를 포기하는 것이 더 나은 관행이다.
자바 언어는 타입 안전성을 강제하도록 설계되었다.
자바의 모든 것은 객체 내에서 발생하며
각 객체는 클래스의 인스턴스이다.
타입 안전성 강제를 구현하기 위해 각 객체는 사용 전에 할당되어야 한다.
자바는 원시 자료형의 사용을 허용하지만, 이는 적절하게 할당된 객체 내에서만 가능하다.
때때로 타입 안전성의 일부는 간접적으로 구현된다. 예를 들어, `BigDecimal` 클래스는 임의 정밀도의 부동 소수점 숫자를 나타내지만, 유한한 표현으로 나타낼 수 있는 숫자만 처리한다.
`BigDecimal.divide()` 연산은 `BigDecimal`로 표현된 두 숫자의 나눗셈으로 새 객체를 계산한다.
이 경우 나눗셈에 유한한 표현이 없는 경우 (예: 1/3=0.33333... 계산 시), 연산에 대해 반올림 모드가 정의되지 않으면 `divide()` 메서드가 예외를 발생시킬 수 있다.
따라서 언어보다는 라이브러리가 클래스 정의에 내재된 계약을 객체가 준수하도록 보장한다.
표준 ML은 엄격하게 정의된 의미론을 가지며 타입 안전하다는 것이 알려져 있다. 그러나 Standard ML of New Jersey (SML/NJ), 그 구문 변형인 Mythryl, 그리고 MLton을 포함한 일부 구현은 안전하지 않은 연산을 제공하는 라이브러리를 제공한다. 이러한 기능은 종종 특정 방식으로 데이터가 배치되어야 할 수 있는 비-ML 코드(예: C 라이브러리)와 상호 작용하기 위해 해당 구현의 외부 함수 인터페이스와 함께 사용된다. 또 다른 예는 SML/NJ 대화형 최상위 수준 자체로, 사용자가 입력한 ML 코드를 실행하기 위해 안전하지 않은 연산을 사용해야 한다.
모듈라-2.
모듈라-2는 강력하게 타입이 지정된 언어로, 안전하지 않은 기능을 명시적으로 안전하지 않은 것으로 표시하도록 요구하는 설계 철학을 가지고 있다. 이는 그러한 기능을 SYSTEM이라는 내장된 유사 라이브러리로 "이동"시켜 사용하기 전에 가져와야 함으로써 달성된다. 따라서 가져오기는 그러한 기능이 사용될 때 가시적으로 만든다. 불행히도, 이는 원래 언어 보고서와 그 구현에서 일관되게 구현되지 않았다. 타입 캐스트 구문과 (파스칼에서 상속된) 변형 레코드와 같이 사전 가져오기 없이 사용할 수 있는 안전하지 않은 기능이 여전히 남아 있었다. 이러한 기능을 SYSTEM 유사 모듈로 이동하는 어려움은 가져올 수 있는 식별자가 없다는 것이었다. 식별자만 가져올 수 있고 구문은 가져올 수 없었기 때문이다.
IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *)
VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS;
addr := SYSTEM.ADR(word);
VAR i : INTEGER; n : CARDINAL;
n := CARDINAL(i); (* or *) i := INTEGER(n);
ISO 모듈라-2 표준은 타입 캐스트 구문을 유사 모듈 SYSTEM에서 가져와야 하는 CAST라는 함수로 변경하여 타입 캐스트 기능을 수정했다. 그러나 변형 레코드와 같은 다른 안전하지 않은 기능은 유사 모듈 SYSTEM에서 가져오지 않아도 계속 사용할 수 있었다.
IMPORT SYSTEM;
i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)
언어의 최근 개정판은 원래의 설계 철학을 엄격하게 적용했다. 먼저, 유사 모듈 SYSTEM은 UNSAFE로 이름이 변경되어 그곳에서 가져온 기능의 안전하지 않은 특성을 더욱 명확하게 했다. 그런 다음 나머지 안전하지 않은 기능은 완전히 제거되거나(예: 변형 레코드) UNSAFE 유사 모듈로 이동되었다. 가져올 수 있는 식별자가 없는 기능의 경우, 활성화 식별자가 도입되었다. 그러한 기능을 활성화하려면 해당 활성화 식별자를 UNSAFE 유사 모듈에서 가져와야 한다. UNSAFE에서 가져오기를 요구하지 않는 안전하지 않은 기능은 언어에 남아있지 않다.
IMPORT UNSAFE;
i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)
FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *)
&lt;*FFI="C"*&gt; (* pragma for foreign function interface to C *)
파스칼은 여러 가지 타입 안전성 요구 사항을 가지고 있었으며, 그중 일부는 일부 컴파일러에서 유지되고 있다. 파스칼 컴파일러가 "엄격한 타이핑"을 지시하는 경우, 두 변수는 호환되는 경우(예: 정수에서 실수로의 변환) 또는 동일한 서브타입에 할당된 경우가 아니면 서로 할당될 수 없다. 예를 들어, 다음과 같은 코드 조각이 있다고 가정해 보자.
TwoTypes = record
I: Integer;
Q: Real;
DualTypes = record
T1, T2: TwoTypes;
D1, D2: DualTypes;
엄격한 타이핑 하에서는 로 정의된 변수는 와 호환되지 않는다(동일하지 않기 때문에, 비록 사용자 정의 타입의 구성 요소가 동일하더라도). 따라서 codice_12 할당은 불법이다. codice_13 할당은 정의된 서브타입이 동일하므로 합법적이다. 그러나 codice_14와 같은 할당은 합법적이다.
일반적으로 커먼 리스프는 타입 안전 언어이다. 커먼 리스프 컴파일러는 타입 안전성을 정적으로 증명할 수 없는 연산에 대해 동적 검사를 삽입할 책임이 있다. 그러나 프로그래머는 프로그램이 더 낮은 수준의 동적 타입 검사로 컴파일되어야 함을 나타낼 수 있다. 이러한 모드로 컴파일된 프로그램은 타입 안전하다고 간주할 수 없다.
다음 예제는 C++ 캐스트 연산자가 잘못 사용될 때 어떻게 타입 안전성을 깨뜨릴 수 있는지 보여준다. 첫 번째 예제는 기본 자료형이 어떻게 잘못 캐스팅될 수 있는지 보여준다.
int ival = 5; // integer value
float fval = reinterpret_cast&lt;float&amp;&gt;(ival); // reinterpret bit pattern
cout « fval « endl; // output integer as float
이 예제에서 codice_15는 컴파일러가 정수에서 부동 소수점 값으로 안전한 변환을 수행하는 것을 명시적으로 방지한다. 프로그램이 실행될 때 쓰레기 부동 소수점 값이 출력될 것이다. codice_16이라고 대신 작성했다면 이 문제는 피할 수 있었을 것이다.
다음 예제는 객체 참조가 어떻게 잘못 다운캐스트될 수 있는지 보여준다.
class Parent {
virtual ~Parent() {} // virtual destructor for RTTI
class Child1 : public Parent {
class Child2 : public Parent {
float b;
Child1 c1;
c1.a = 5;
Parent &amp; p = c1; // upcast always safe
Child2 &amp; c2 = static_cast&lt;Child2&amp;&gt;(p); // invalid downcast
cout « c2.b « endl; // will output garbage data
두 자식 클래스는 서로 다른 타입의 멤버를 가지고 있다. 부모 클래스 포인터를 자식 클래스 포인터로 다운캐스트할 때, 결과 포인터가 올바른 타입의 유효한 객체를 가리키지 않을 수 있다. 이 예제에서는 쓰레기 값이 출력되는 결과를 초래한다. codice_17를 유효하지 않은 캐스트에 예외를 던지는 codice_18로 대체했다면 이 문제를 피할 수 있었을 것이다.
로렌츠 다양체 이론에서 구형 대칭 시공간은 일련의 내포된 둥근 구들을 허용한다. 이러한 시공간에서 특히 중요한 종류의 좌표 도표는 슈바르츠실트 도표()이며, 이는 이러한 내포된 둥근 구에 맞춰진 정적 및 구형 대칭 시공간 상의 일종의 극 구면좌표계 도표이다. 슈바르츠실트 도표의 결정적인 특징은 반경 좌표가 각 구의 겉넓이 및 가우스 곡률 측면에서 자연스러운 기하학적 해석을 갖는다는 것이다. 그러나 반경 거리와 각도는 정확하게 표현되지 않는다.
이러한 도표는 일반 상대성이론과 같은 계량 중력 이론에서 많은 응용 분야를 갖는다. 그것들은 대부분 정적 구형 대칭 시공간에서 사용된다. 일반 상대성이론의 경우, 버코프의 정리에 따르면 아인슈타인 방정식의 모든 고립된 구형 대칭 진공 또는 전기진공 해는 정적이지만, 이는 이상 유체의 경우에는 확실히 사실이 아니다. 슈바르츠실트 진공 해의 외부 영역이 구형 대칭 블랙홀의 사건의 지평선 안쪽으로 확장될 때, 지평선 안쪽은 정적이지 않고 (공간꼴) 내포된 구들의 집합은 지평선 안쪽으로 확장될 수 없으므로, 이 해에 대한 슈바르츠실트 도표는 지평선에서 필연적으로 무너진다.
계량 텐서 formula_1를 지정하는 것은 모든 로렌츠 다양체 정의의 일부이다. 이 텐서를 정의하는 가장 간단한 방법은 호환되는 국소 좌표 도표에서 정의하고 도표 영역의 겹침에서 동일한 텐서가 정의되는지 확인하는 것이다. 이 글에서는 단일 도표 영역에서 계량 텐서만 정의하려고 한다.
슈바르츠실트 도표(정적 구형 대칭 시공간에서)에서 선 요소는 다음과 같은 형태를 취한다.
여기서 formula_4는 표준 구면좌표이고 formula_5는 단위 2-구의 표준 계량이다. 이 표현에 대한 자세한 유도는 슈바르츠실트 해 유도를 참조하라.
문맥에 따라, a와 b를 반경 좌표의 미정 함수로 간주하는 것이 적절할 수 있다 (예를 들어, 아인슈타인 방정식의 정확한 정적 구형 대칭 해를 유도할 때). 또는 특정 함수 (일부 매개변수에 따라 달라질 수 있음)를 대입하여 특정 로렌츠 시공간에 대한 슈바르츠실트 좌표 도표를 얻을 수 있다.
만약 이것이 에너지-운동량 텐서를 허용하여 결과 모델이 아인슈타인 방정식을 만족한다면 (예를 들어, 적절한 에너지 조건과 합리적인 이상 유체에서 예상되는 다른 속성을 따르는 정적 구형 대칭 이상 유체에 대해), 물질 및 운동량 밀도와 같은 물리량을 나타내는 적절한 텐서 필드를 사용하여 우리는 더 큰 시공간의 일부를 갖게 된다. 이 부분은 아인슈타인 방정식의 국소 해로 간주될 수 있다.
슈바르츠실트 도표에 대해 킬링 벡터장의 리 대수는 시간꼴 비회전 킬링 벡터장에 의해 생성된다.
그리고 세 개의 공간꼴 킬링 벡터장
여기서 formula_10가 비회전적이라는 것은 해당 시간꼴 합류의 회전도 텐서가 사라진다는 것을 의미한다. 따라서 이 킬링 벡터장은 초곡면 직교이다. 우리 시공간이 비회전 시간꼴 킬링 벡터장을 허용한다는 사실은 사실 정적 시공간의 정의적 특징이다. 한 가지 직접적인 결과는 일정한 시간 좌표 표면 formula_11이 (등거리) 공간 초단면족을 형성한다는 것이다. (예를 들어 커 진공의 외부 영역에 대한 보이어–린드퀴스트 도표에서는 시간꼴 좌표 벡터가 초곡면 직교가 아니므로 이것은 사실이 아니다.)
마지막 두 필드는 formula_12 좌표 변환 하에서 서로 회전임을 주목하라. 킬링 벡터장에 대한 글은 세 개의 공간꼴 필드에 대한 자세한 유도 및 논의를 제공한다.
정적 내포 구족.
슈바르츠실트 도표에서 표면 formula_13은 둥근 구로 나타나며(극 구형 방식으로 자취를 그릴 때), 그 형태에서 우리는 이러한 표면 중 어느 하나로 제한된 슈바르츠실트 계량이 양의 정부호이며 다음과 같이 주어짐을 알 수 있다.
여기서 formula_5는 단위 반지름 2-구의 표준 리만 계량이다. 즉, 이 내포된 좌표 구들은 실제로 다음과 같은 기하학적 구들을 나타낸다.
특히, 이들은 기하학적 둥근 구이다. 더욱이, 각 좌표 formula_18는 정확히 일반적인 극 구형 각 좌표이다. formula_19는 때때로 여위도로 불리고 formula_20는 보통 경도로 불린다. 이것이 본질적으로 슈바르츠실트 도표의 결정적인 기하학적 특징이다.
위에서 주어진 네 개의 킬링 장들은 우리 로렌츠 다양체의 추상적인 벡터장으로 간주될 때, 정적 구형 대칭 시공간의 대칭성을 가장 잘 표현하며, 우리 도표에서 취하는 특정 삼각 함수 형태는 슈바르츠실트 도표라는 용어의 의미를 가장 잘 표현한다는 것을 덧붙이는 것이 도움이 될 것이다. 특히, 세 개의 공간 킬링 벡터장은 E3 상의 구형 대칭 도표에서 세 개의 비병진 킬링 벡터장과 정확히 같은 형태를 가지며, 즉 원점 또는 구형 대칭에 대한 임의의 유클리드 회전 개념을 보여준다.
그러나 다음을 잘 주목하라: 일반적으로, 슈바르츠실트 반경 좌표는 반경 거리를 정확하게 나타내지 않는다. 즉, formula_21의 적분 곡선으로 발생하는 공간꼴 측지선 합류를 따라 취한 거리를 정확하게 나타내지 않는다. 오히려, 우리 내포 구들 사이의 적절한 '공간 거리' 개념을 찾기 위해, 우리는 원점으로부터의 일부 좌표선을 따라 formula_22을 적분해야 한다.
마찬가지로, 우리는 각 구를 이상화된 관찰자들의 구형 구름의 자취로 간주할 수 있는데, 이들은 (일반적으로) 그들의 위치를 유지하기 위해 로켓 엔진을 사용하여 바깥쪽으로 반경 방향으로 가속해야 한다. 이들은 정적 관찰자이며, formula_24 형태의 세계선을 가지며, 이는 물론 슈바르츠실트 도표에서 수직 좌표선의 형태를 갖는다.
이러한 관찰자 중 한 명의 세계선에서 두 사건 사이의 고유 시간 간격을 계산하기 위해, 우리는 해당 좌표선을 따라 formula_25를 적분해야 한다.
좌표 특이점.
위의 좌표 범위를 다시 살펴보면, formula_27에서의 좌표 특이점은 우리 정적 내포 구들 중 하나의 북극 위치를 나타내는 반면, formula_28는 남극 위치를 나타낸다. E3의 일반적인 극 구형 도표와 마찬가지로, 위상학적 이유로 전체 구에서 연속적인 좌표를 얻을 수 없다. 우리는 자오선 formula_29으로 작용할 일부 경선(대원)을 선택하고 이를 도표에서 잘라내야 한다. 결과적으로 우리는 축 formula_30과 그 축에서 확장되는 반평면을 포함하여 각 공간 초단면 formula_11에서 닫힌 반평면을 잘라낸다.
위에서 formula_32가 킬링 벡터장이라고 말했을 때 우리는 formula_20를 주기적 좌표로 생각하고, 실제로 세 공간꼴 킬링 벡터를 둥근 구에 작용하는 것으로 생각한다는, 따분하지만 중요한 수식어를 생략했다.
물론 formula_34 또는 formula_35일 수 있으며, 이 경우 우리는 도표의 영역에서 어떤 공 바깥 영역 또는 어떤 공 안쪽 영역을 제외해야 한다. 이것은 f 또는 g가 슈바르츠실트 반경 좌표 r의 어떤 값에서 폭발할 때 발생한다.
정적 초단면 시각화.
슈바르츠실트 반경 좌표의 중요성을 더 잘 이해하려면 공간 초단면 중 하나인 formula_11(물론 모두 서로 등거리이다)를 평평한 유클리드 공간에 삽입하는 것이 도움이 될 수 있다. 4차원 유클리드 공간을 시각화하기 어렵다고 생각하는 사람들은 구형 대칭을 이용하여 하나의 좌표를 억제할 수 있다는 점을 반길 것이다. 이는 formula_37로 설정함으로써 편리하게 달성할 수 있다. 이제 우리는 국소 반경 좌표 도표를 가진 2차원 리만 다양체를 갖게 된다.
이 표면(또는 환형 고리)을 E3에 삽입하기 위해, E3에서 다음과 같은 틀 필드를 채택한다.
즉, 매개변수화된 표면을 고려한다.
이 표면의 좌표 벡터 필드는 다음과 같다.
E3의 유클리드 계량을 우리 매개변수화된 표면에 제한할 때 상속되는 유도 계량은 다음과 같다.
이것을 우리 초단면의 계량과 동일시하려면, 우리는 분명히 다음과 같이 formula_39을 선택해야 한다.
다소 우스꽝스러운 예를 들자면, formula_45일 수 있다.
이는 두 개의 반경 방향으로 분리된 점 사이의 실제 거리가 그들의 반경 좌표 차이보다 큰 표면에 대해 유효하다. 만약 실제 거리가 더 작다면, 우리 리만 다양체를 대신 E1,2의 공간꼴 표면으로 삽입해야 한다. 예를 들어, formula_46일 수 있다. 때때로 양의 가우스 곡률 또는 음의 가우스 곡률 영역에 대해 두 개 이상의 국소 환형 고리 삽입이 필요할 수 있다. 일반적으로, 우리는 어떤 평면 공간(리만 텐서가 사라지는)에서도 전역적인 삽입을 얻을 것으로 기대해서는 안 된다.
요점은 슈바르츠실트 도표의 결정적인 특징인 반경 좌표의 기하학적 해석이 이러한 종류의 공간 초단면의 구형 대칭 삽입을 (원칙적으로) 수행하는 데 필요한 것과 정확히 일치한다는 것이다.
계량 가설 풀이.
위에 주어진 선 요소는 f, g를 슈바르츠실트 반경 좌표 r의 미정 함수로 간주하여 일반 상대성이론(또는 기타 계량 중력 이론)에서 정적 구형 대칭 해를 유도하는 데 가설 풀이로 자주 사용된다.
예시로, 카르탕의 외 미적분 방법을 사용하여 접속 및 곡률을 계산하는 방법을 보여준다. 먼저 선 요소에서 코프레임 필드를 읽는다.
여기서 formula_51는 아직 미정인 formula_52의 매끄러운 함수로 간주한다. (우리 시공간이 이러한 특정 삼각 함수 형태를 갖는 프레임을 허용한다는 사실은 정적, 구형 대칭 로렌츠 다양체에서 슈바르츠실트 도표 개념의 또 다른 등가 표현이다.)
둘째, 이 코기저 1형식의 외미분을 계산한다.
카르탕의 첫 번째 구조 방정식(또는 그 완전성 조건)과 비교하여,
접속 1형식에 대한 표현을 추측한다. (모자는 지표가 좌표 1형식 formula_58가 아니라 우리 코기저 1형식을 참조한다는 것을 상기시키는 표기 장치이다.)
formula_59에서 어떤 지표 쌍이 대칭(시공간)이고 어떤 쌍이 반대칭(공간-공간)인지 기억한다면, 6개의 접속 1형식이 다음과 같음을 확인할 수 있다.
이 1형식들을 1형식의 행렬로 묶거나, 더 좋게는 SO(1,3)-값 1형식으로 묶을 수 있다.
결과 1형식 행렬이 SO(4)-값 1형식처럼 완전히 반대칭이 아닐 것임에 유의하라. 대신 로렌츠 수반에서 발생하는 전치 개념을 사용해야 한다.
셋째, 접속 1형식의 외미분을 계산하고 카르탕의 두 번째 구조 방정식
을 사용하여 곡률 2형식을 계산한다. 넷째, 다음 공식을 사용하여
여기서 바흐 막대는 (i,j)의 증가하는 6개 쌍에 대해서만 합해야 함을 나타내며, 우리 코프레임과 그 쌍대 프레임 필드에 대한 리만 텐서의 선형 독립 성분을 읽을 수 있다. 우리는 다음을 얻는다.
다섯째, 지수를 내리고 성분 formula_72를 행렬로 정리할 수 있다.
여기서 E, L은 대칭이고 (일반적으로 6개의 선형 독립 성분), B는 무적이다 (일반적으로 8개의 선형 독립 성분). 이는 (각 사건에서) 6차원 2형식 벡터 공간에 대한 선형 연산자를 나타내는 것으로 생각된다. 이로부터 시간꼴 단위 벡터장 formula_74에 대한 벨 분해를 읽을 수 있다. 전자기중력 텐서는 다음과 같다.
자기중력 텐서는 항등적으로 사라지며, 지형중력 텐서는 ( formula_76가 비회전이라는 사실을 사용하여) 공간 초단면의 3차원 리만 텐서를 결정할 수 있는데, 이는 다음과 같다.
이것은 모든 로렌츠 다양체에 대해 유효하지만, 일반 상대성이론에서 전자기중력 텐서는 우리 프레임에 해당하는 관찰자들이 측정한 작은 물체에 대한 조석 응력을 제어하고, 자기중력 텐서는 우리 프레임에 해당하는 관찰자들이 측정한 회전하는 물체에 대한 스핀-스핀 힘을 제어한다.
우리 코프레임 필드의 쌍대 프레임 필드는 다음과 같다.
여기서 formula_82 인수가 세 개의 정규 직교 공간꼴 벡터 필드 중 첫 번째에만 곱해진다는 사실은 슈바르츠실트 도표가 공간적으로 등방성이지 않다는 것을 의미한다 (국소적으로 평탄한 시공간의 자명한 경우는 제외). 오히려, 빛 원뿔은 (반경 방향으로 납작해지거나) (반경 방향으로 길어진) 형태로 나타난다. 이것은 물론 슈바르츠실트 도표가 각 내포된 둥근 구 내의 거리를 올바르게 나타내지만, 반경 좌표는 반경 고유 거리를 충실하게 나타내지 않는다는 것을 말하는 또 다른 방법이다.
슈바르츠실트 도표를 허용하는 몇 가지 정확한 해.
이러한 방식으로 얻을 수 있는 정확한 해의 몇 가지 예는 다음과 같다.
비정적이지만 구형 대칭인 시공간을 고려하는 것은 자연스러운 일이며, 시공간 계량이 다음 형태를 취하는 일반화된 슈바르츠실트 도표를 사용한다.
다른 방향으로 일반화하여, 둥근 2-구에 다른 좌표계를 사용하여 예를 들어 때때로 유용한 스테레오그래픽 슈바르츠실트 도표를 얻을 수 있다.
자료형 추론(資料型推論, Type inference) 또는 자료형 재구성(type reconstruction)은 형식 언어에서 식의 자료형을 자동으로 감지하는 것을 의미한다. 여기에는 프로그래밍 언어와 수학적 자료형 체계뿐만 아니라 컴퓨터 과학 및 언어학의 일부 분야에서 자연어도 포함된다.
자료형 가능성(Typeability)은 때때로 자료형 추론과 거의 동의어로 사용되지만, 일부 저자는 예/아니오 답변을 가지는 결정 문제로서의 자료형 가능성과 항에 대한 실제 자료형을 계산하는 자료형 추론을 구별한다.
비기술적 설명.
유형화된 언어에서 용어의 자료형은 해당 언어에서 용어가 사용될 수 있는 방식과 사용될 수 없는 방식을 결정한다. 예를 들어, 영어와 "노래하다 _"라는 구문에서 빈칸을 채울 수 있는 용어를 생각해 보자. "노래"라는 용어는 노래할 수 있는 자료형이므로 빈칸에 넣어 의미 있는 구문인 "노래를 부르다"를 형성할 수 있다. 반면에 "친구"라는 용어는 노래할 수 있는 자료형이 아니므로 "친구를 노래하다"는 무의미하다. 기껏해야 은유일 수 있으며, 자료형 규칙을 구부리는 것은 시적 언어의 특징이다.
용어의 자료형은 해당 용어가 포함된 연산의 해석에도 영향을 미칠 수 있다. 예를 들어, "노래"는 구성 가능한 자료형이므로 "노래를 쓰다"라는 구문에서 생성되는 것으로 해석한다. 반면에 "친구"는 수령자 자료형이므로 "친구에게 쓰다"라는 구문에서 받는 사람으로 해석한다. 일반적인 언어에서 "노래를 쓰다"가 노래에 편지를 보내는 것을 의미하거나 "친구에게 쓰다"가 종이에 친구를 스케치하는 것을 의미한다면 우리는 놀랄 것이다.
서로 다른 자료형을 가진 용어라도 실질적으로 동일한 것을 지칭할 수 있다. 예를 들어, "빨랫줄을 걸다"는 그것을 사용하는 것으로 해석하지만, "목줄을 걸다"는 그것을 치우는 것으로 해석할 수 있다. 비록 문맥상 "빨랫줄"과 "목줄"이 다른 시점에 같은 밧줄을 지칭할 수 있더라도 말이다.
자료형은 종종 개체가 너무 일반적으로 고려되는 것을 방지하기 위해 사용된다. 예를 들어, 자료형 시스템이 모든 숫자를 동일하게 취급한다면, 프로그래머가 실수로 `4`가 "4초"를 의미해야 하지만 "4미터"로 해석되는 코드를 작성하면 런타임에 문제가 발생할 때까지 실수에 대한 경고를 받지 못할 것이다. 측정 단위를 자료형 시스템에 통합함으로써 이러한 실수를 훨씬 일찍 감지할 수 있다. 다른 예로, 러셀의 역설은 모든 것이 집합의 원소가 될 수 있고 모든 술어가 집합을 정의할 수 있을 때 발생하지만, 더 신중한 자료형 지정은 역설을 해결하는 여러 가지 방법을 제공한다. 사실 러셀의 역설은 자료형 이론의 초기 버전을 촉발시켰다.
용어가 자료형을 얻는 몇 가지 방법이 있다:
특히 프로그래밍 언어에서는 컴퓨터에 사용할 수 있는 공유된 배경 지식이 많지 않을 수 있다. 명시적으로 자료형이 지정된 언어에서는 대부분의 자료형을 명시적으로 선언해야 한다는 것을 의미한다. 자료형 추론은 이러한 부담을 덜어주어, 컴퓨터가 문맥에서 추론할 수 있어야 하는 자료형을 저자가 선언하지 않아도 되게 한다.
자료형 검사 대 자료형 추론.
자료형 지정에서 표현식 E는 자료형 T와 대립되며, 형식적으로 E : T로 작성된다. 일반적으로 자료형 지정은 어떤 맥락 내에서만 의미가 있으며, 여기서는 생략한다.
이러한 설정에서 다음 질문들이 특히 중요하다:
단순형 람다 대수의 경우, 세 가지 질문 모두 결정가능하다. 그러나 더 표현력이 뛰어난 자료형이 허용될 때는 상황이 그리 편안하지 않다.
프로그래밍 언어의 자료형.
자료형은 일부 강력한 정적 자료형 지정 언어에 존재하는 기능이다. 일반적으로 함수형 프로그래밍 언어의 특징인 경우가 많다. 자료형 추론을 포함하는 언어로는 C (C23부터), C++ (C++11부터), C# (버전 3.0부터), 채플, 클린, 크리스탈, D, 다트, F#, 프리베이직, Go, 하스켈, 자바 (버전 10부터), 줄리아, 코틀린, ML, 님, OCaml, 오파, Q#, RPython, 러스트, 스칼라, 스위프트, 타입스크립트, 발라, Zig, 그리고 비주얼 베이직 (버전 9.0부터) 등이 있다.
대부분의 언어는 단순한 형태의 자료형 추론을 사용한다. 힌들리-밀너 자료형 체계는 더 완전한 자료형 추론을 제공할 수 있다. 자료형을 자동으로 추론하는 기능은 많은 프로그래밍 작업을 더 쉽게 만들며, 프로그래머가 자료형 주석을 생략하면서도 자료형 검사를 허용한다.
일부 프로그래밍 언어에서는 모든 값이 컴파일 타임에 명시적으로 선언된 자료형을 가지며, 특정 표현식이 런타임에 취할 수 있는 값을 제한한다. 점점 더 JIT 컴파일은 런타임과 컴파일 타임의 구분을 모호하게 만든다. 그러나 역사적으로 값의 자료형이 런타임에만 알려져 있다면 이러한 언어는 동적 자료형이다. 다른 언어에서는 표현식의 자료형이 컴파일 타임에만 알려져 있다. 이러한 언어는 정적 자료형이다. 대부분의 정적 자료형 언어에서는 함수의 입력 및 출력 자료형과 지역 변수의 자료형을 일반적으로 자료형 주석으로 명시적으로 제공해야 한다. 예를 들어, ANSI C에서는 다음과 같다:
int add_one(int x) {
int result; /* 정수형 결과 선언 */
result = x + 1;
이 함수 정의의 시그니처인 `int add_one(int x)`는 `add_one`이 하나의 인수인 정수형을 취하고 정수를 반환하는 함수임을 선언한다. `int result;`는 지역 변수 `result`가 정수임을 선언한다. 자료형 추론을 지원하는 가상의 언어에서는 코드가 대신 다음과 같이 작성될 수 있다:
add_one(x) {
var result; /* 추론된 자료형 변수 result */
var result2; /* 추론된 자료형 변수 result #2 */
result2 = x + 1.0; /* 이 줄은 (제안된 언어에서) 작동하지 않는다 */
이것은 언어 다트에서 코드가 작성되는 방식과 동일하지만, 아래에 설명된 몇 가지 추가 제약이 적용된다. 컴파일 타임에 모든 변수의 자료형을 추론하는 것이 가능하다. 위 예제에서 컴파일러는 상수 `1`이 정수 자료형이므로 `result`와 `x`가 정수 자료형임을 추론할 것이며, 따라서 `add_one`은 `int -&gt; int` 함수가 된다. 변수 `result2`는 유효한 방식으로 사용되지 않으므로 자료형이 없을 것이다.
마지막 예제가 작성된 가상의 언어에서 컴파일러는 반대되는 정보가 없는 한 `+`가 두 개의 정수를 받아 하나의 정수를 반환한다고 가정할 것이다. (이것은 예를 들어 OCaml에서 작동하는 방식이다.) 여기에서 자료형 추론기는 `x + 1`의 자료형이 정수임을 추론할 수 있으며, 이는 `result`가 정수이고 따라서 `add_one`의 반환 값이 정수임을 의미한다. 마찬가지로 `+`는 두 인수가 동일한 자료형이어야 하므로 `x`는 정수여야 하며, 따라서 `add_one`은 하나의 정수를 인수로 받는다.
그러나 다음 줄에서 result2는 십진수 `1.0`을 부동소수점 연산으로 더하여 계산되는데, 이는 정수 및 부동소수점 표현식 모두에 `x`를 사용하는 데 충돌을 일으킨다. 이러한 상황에 대한 올바른 자료형 추론 알고리즘은 1958년부터 알려져 있었고, 1982년부터 정확하다는 것이 알려져 있었다. 이 알고리즘은 이전 추론을 재검토하고 처음부터 가장 일반적인 자료형을 사용한다. 이 경우 부동소수점 자료형이다. 그러나 이는 처음부터 부동소수점을 사용하면 정수 자료형에서는 존재하지 않았을 정밀도 문제를 야기할 수 있다는 등 해로운 영향을 미칠 수 있다.
그러나 종종 이러한 상황에서 역추적할 수 없고 대신 오류 메시지를 생성하는 퇴행적 자료형 추론 알고리즘이 사용된다. 자료형 추론이 항상 알고리즘적으로 중립적이지 않을 수 있기 때문에 이 동작이 더 바람직할 수 있다. 이는 이전의 부동소수점 정밀도 문제에서 알 수 있다.
중간 정도의 일반성을 가진 알고리즘은 result2를 부동소수점 변수로 암시적으로 선언하고, 덧셈은 `x`를 부동소수점으로 암시적으로 변환한다. 이는 호출 컨텍스트에서 부동소수점 인수를 제공하지 않는 경우 올바를 수 있다. 이러한 상황은 형 변환을 포함하지 않는 자료형 추론과, 종종 제한 없이 데이터를 다른 자료형으로 강제 변환하는 암시적 형 변환 간의 차이를 보여준다.
마지막으로, 복잡한 자료형 추론 알고리즘의 중요한 단점은 결과적인 자료형 추론 해결책이 사람에게 명확하지 않을 수 있다는 점이다(특히 역추적 때문에). 이는 코드가 주로 사람이 이해할 수 있도록 의도되었기 때문에 해로울 수 있다.
최근 JIT 컴파일의 등장으로 다양한 호출 컨텍스트에서 제공되는 인수의 자료형이 컴파일 타임에 알려져 동일한 함수의 많은 컴파일된 버전을 생성할 수 있는 하이브리드 접근 방식이 가능해졌다. 각 컴파일된 버전은 서로 다른 자료형 세트에 최적화될 수 있다. 예를 들어, JIT 컴파일은 add_one의 컴파일된 버전을 최소 두 개 이상 가질 수 있도록 한다:
자료형 추론은 컴파일 시점에 표현식의 자료형을 부분적으로 또는 완전히 자동으로 추론하는 기능이다. 컴파일러는 명시적인 자료형 주석이 주어지지 않아도 변수의 자료형이나 함수의 자료형 시그니처를 종종 추론할 수 있다. 자료형 추론 시스템이 충분히 강력하거나 프로그램이나 언어가 충분히 단순하다면 많은 경우 프로그램에서 자료형 주석을 완전히 생략하는 것이 가능하다.
표현식의 자료형을 추론하는 데 필요한 정보를 얻기 위해 컴파일러는 하위 표현식에 주어진 자료형 주석을 집계하고 후속적으로 축소하거나, 다양한 원자 값의 자료형(예: true : Bool; 42 : Integer; 3.14159 : Real; 등)을 암시적으로 이해함으로써 이 정보를 수집한다. 컴파일러는 표현식이 암시적으로 자료형이 지정된 원자 값으로 최종적으로 축소되는 것을 인식함으로써 자료형 추론 언어용 컴파일러가 자료형 주석 없이 프로그램을 완전히 컴파일할 수 있다.
고차 프로그래밍 및 다형성의 복잡한 형태에서는 컴파일러가 그만큼 많이 추론하는 것이 항상 가능하지 않으며, 모호성을 해소하기 위해 때때로 자료형 주석이 필요하다. 예를 들어, 다형적 재귀를 사용한 자료형 추론은 결정 불가능한 것으로 알려져 있다. 또한 명시적인 자료형 주석은 컴파일러가 추론했던 것보다 더 구체적인(더 빠르거나 더 작은) 자료형을 사용하도록 강제함으로써 코드를 최적화하는 데 사용될 수 있다.
일부 자료형 추론 방법은 제약 충족 또는 이론 모듈로 만족 가능성을 기반으로 한다.
고수준 예제.
예를 들어, 하스켈 함수 map은 리스트의 각 요소에 함수를 적용하며 다음과 같이 정의될 수 있다.
map f [] = []
map 함수에 대한 자료형 추론은 다음과 같이 진행된다. map은 두 개의 인수를 받는 함수이므로 자료형은 a -&gt; b -&gt; c 형태여야 한다. 하스켈에서 []와 (first:rest) 패턴은 항상 리스트와 일치하므로 두 번째 인수는 리스트 자료형이어야 한다: 일부 자료형 d에 대해 b = [d]. 첫 번째 인수 f는 first 인수에 적용되며, 이 인수는 리스트 인수의 자료형에 해당하는 자료형 d를 가져야 하므로 일부 자료형 e에 대해 f :: d -&gt; e (::는 "자료형이 ~이다"를 의미한다). 마지막으로 map f의 반환 값은 f가 생성하는 것의 리스트이므로 [e]이다.
이러한 부분을 조합하면 map :: (d -&gt; e) -&gt; [d] -&gt; [e]가 된다. 자료형 변수에 특별한 것은 없으므로 다음과 같이 재지정할 수 있다.
map :: (a -&gt; b) -&gt; [a] -&gt; [b]
추가 제약이 적용되지 않으므로 이것이 가장 일반적인 자료형임이 밝혀졌다. map의 추론된 자료형은 매개변수적으로 다형성이므로, f의 인수 및 결과의 자료형은 추론되지 않고 자료형 변수로 남는다. 따라서 map은 호출할 때마다 실제 자료형이 일치하는 한 다양한 자료형의 함수와 리스트에 적용될 수 있다.
상세 예제.
컴파일러와 같은 프로그램이 사용하는 알고리즘은 위에 비공식적으로 구조화된 추론과 동등하지만, 약간 더 장황하고 체계적이다. 정확한 세부 사항은 선택된 추론 알고리즘에 따라 다르지만(가장 잘 알려진 알고리즘은 다음 섹션 참조), 아래 예제는 일반적인 아이디어를 제공한다. 다시 map의 정의로 시작한다.
먼저, 각 개별 항에 대해 새로운 자료형 변수를 만든다:
그런 다음 이러한 항으로 구성된 하위 표현식에 대해 새로운 자료형 변수를 만들고, 호출되는 함수의 자료형을 그에 따라 제한한다:
또한 각 방정식의 왼쪽과 오른쪽이 서로 통합되도록 제한한다: `κ ~ [δ]` 및 `μ ~ ο`. 통합 시스템을 모두 풀면 다음과 같다:
그런 다음 더 이상 변수를 제거할 수 없을 때까지 대입한다. 정확한 순서는 중요하지 않다. 코드가 자료형 검사를 통과하면 어떤 순서든 동일한 최종 형식으로 이어진다. `ο`를 `μ`로, `[δ]`를 `κ`로 대입하는 것부터 시작해 보자:
`ζ`를 `η`로, `[ζ]`를 `θ`와 `λ`로, `ι`를 `ν`로, `[ι]`를 `ξ`와 `ο`로 대입한다. · -&gt; ·와 같은 자료형 생성자는 인수에 대해 역변환 가능하므로 이 모든 대입이 가능하다:
`ε`에 `ζ -&gt; ι`를, `α`에 `β -&gt; [γ] -&gt; [δ]`를 대입하고, 마지막에 `α`를 복구할 수 있도록 두 번째 제약을 유지한다.
그리고 마침내 [·]와 같은 자료형 생성자는 역변환 가능하므로 `β`에 `(ζ -&gt; ι)`를, `γ`에 `ζ`를, `δ`에 `ι`를 대입하면 두 번째 제약에 특정한 모든 변수가 제거된다.
더 이상 대입할 수 없으며, 자료형을 재지정하면 map :: (a -&gt; b) -&gt; [a] -&gt; [b]가 된다. 이는 이 세부 사항에 들어가지 않고 찾았던 것과 동일하다.
힌들리-밀너 자료형 추론 알고리즘.
자료형 추론을 수행하는 데 처음 사용된 알고리즘은 현재 비공식적으로 힌들리-밀너 알고리즘이라고 불리지만, 이 알고리즘은 다마스와 밀너에게 제대로 귀속되어야 한다.