Scala의 유형 시스템은 Turing이 완료되었습니다. 증명? 예? 혜택?
Scala의 유형 시스템이 Turing 완전하다는 주장이 있습니다. 내 질문은 다음과 같습니다.
이것에 대한 공식적인 증거가 있습니까?
Scala 유형 시스템에서 간단한 계산은 어떻게 보일까요?
이것이 Scala (언어)에 어떤 이점이 있습니까? 이것이 Turing 완전한 유형 시스템이없는 언어에 비해 Scala를 어떤면에서 더 "강력하게"만들까요?
나는 이것이 일반적으로 언어 및 유형 시스템에 적용되는 것 같습니다.
Turing-complete로 알려진 SKI combinator calculus의 유형 수준 구현이 포함 된 블로그 게시물이 어딘가에 있습니다.
Turing-complete 유형 시스템은 기본적으로 Turing-complete 언어와 동일한 장점과 단점을 가지고 있습니다. 무엇이든 할 수 있지만 증명할 수있는 것은 거의 없습니다. 특히, 결국에는 실제로 무언가를 할 것이라는 것을 증명할 수 없습니다.
유형 수준 계산의 한 가지 예는 Scala 2.8의 새로운 유형 보존 컬렉션 변환기입니다. 스칼라 2.8에서, 방법은 좋아한다 map, filter등등 그들이 호출 된 것과 같은 종류의 컬렉션을 반환 보장됩니다. 그래서, 당신이 경우 , 당신은 돌아갈 하고 경우 A는 당신은 다시 얻을 .filterSet[Int]Set[Int]mapList[String]List[Whatever the return type of the anonymous function is]
이제 보시 map다시피 실제로 요소 유형을 변환 할 수 있습니다. 그렇다면 새 요소 유형을 원래 컬렉션 유형으로 표현할 수 없으면 어떻게됩니까? 예 : a BitSet는 고정 너비 정수만 포함 할 수 있습니다. 그렇다면 a가 BitSet[Short]있고 각 숫자를 문자열 표현에 매핑하면 어떻게 될까요?
someBitSet map { _.toString() }
결과는 것 이 될 BitSet[String],하지만 그건 불가능하다. 따라서 Scala는를 BitSet보유 할 수있는 String,이 경우 Set[String].
이 모든 계산은 컴파일 시간 동안 또는 더 정확하게는 유형 수준 함수를 사용하여 유형 검사 시간 동안 진행 됩니다. 따라서 형식이 실제로 계산되어 디자인 타임에 알려지지 않은 경우에도 형식 안전이 정적으로 보장됩니다.
Scala 유형 시스템에서 SKI 미적분을 인코딩하는 것에 대한 내 블로그 게시물 은 Turing 완전성을 보여줍니다.
일부 간단한 유형 수준 계산의 경우 자연수 및 덧셈 / 곱셈 을 인코딩하는 방법에 대한 몇 가지 예도 있습니다.
마지막으로 Apocalisp의 블로그에 유형 수준 프로그래밍에 대한 훌륭한 기사 시리즈가 있습니다.
'programing' 카테고리의 다른 글
| UML 다이어그램을 GitLab 또는 GitHub에 통합하는 방법 (0) | 2021.01.15 |
|---|---|
| Java 9를 32 비트 OS에서 실행할 수 있습니까? (0) | 2021.01.15 |
| JavaScript를 통해 CSS 의사 요소 스타일 변경 (0) | 2021.01.15 |
| Vim에 파일을 저장 한 후 자동으로 쉘 명령을 실행하는 방법은 무엇입니까? (0) | 2021.01.15 |
| 같은 이름의 파일이 많은 프로젝트의 한 파일에 중단 점을 설정하는 방법은 무엇입니까? (0) | 2021.01.15 |