유형 추론의 한계는 무엇입니까?
https://stackoverflow.com/questions/1251254
-
12-09-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian문제
유형 추론의 한계는 무엇입니까? 일반적인 추론 알고리즘이없는 유형 시스템은 무엇입니까?
해결책
조 웰스 Girard와 Reynolds에 의해 독립적으로 발견 된 가장 기본적인 다형성 람다 미적분학 인 시스템 F에 대해서는 유형 추론이 불안정하다는 것을 보여 주었다. 이것은 유형 추론의 한계를 보여주는 가장 중요한 결과입니다.
여기에 여전히 열려있는 중요한 문제가 있습니다. 일반화 된 대수 데이터 유형을 Hindley-Milner 유형에 통합하는 가장 좋은 방법은 무엇입니까? 매년 사이먼 페이튼 존스 (Simon Peyton Jones)는 새로운 답변을 제시하는데, 이는 전년도의 답변보다 낫습니다. 나는 2009 년 3 월 버전을 읽지 않았으므로 그것이 결정적이라고 믿는다면 말할 수 없습니다.
다른 팁
값 의존성 유형 시스템 (또는 간단히 말하면 종속 유형 시스템)은 다음과 같은 내용을 설명 할 수 있습니다. "평가 시간 (런타임) 에서이 변수의 값은 항상 해당 변수의 값과 동일합니다. 다른 평가 프로세스로 계산됩니다. " 코드 에서이 유형을 자동으로 추론하려면 이론의 자동 증명이 수반됩니다. 표현할 수있는 정리 세트가 자동으로 입증 가능한 것으로 제한되면 문제가되지는 않지만 종속적으로 유형 된 언어의 경우 일반적으로 그렇지 않습니다.
따라서 의존적으로 입력 된 시스템은 일반 (및 완전한) 유형 추론을 가질 수 없습니다.
나는 누군가가 도덕적 형식적이고 완전한 대답을 제공 할 수 있다고 확신합니다 ...
