종속 ML
Dependent ML | 이 글에는 여러 가지 문제가 있다.이 문제를 개선하거나 대화 페이지에서 토의하십시오.(이러한 템플릿 메시지를 제거하는 방법 및 시기 알아보기)
|
종속 ML은 훙웨이자이(2007년 Xi)와 프랭크 페닝이 제안한 실험 기능 프로그래밍 언어다.종속적 ML은 종속적 유형의 제한된 개념에 의해 ML을 확장한다: 유형은 Nat형(자연수)의 정적 지수에 의존할 수 있다.종속적 ML은 제약조건 정리 프로베러를 채택하여 지수 표현에 대한 강력한 동일성 이론을 결정한다.
DML의 유형은 런타임 값에 의존하지 않는다 - 프로그램의 컴파일과 실행 사이에는 여전히 단계적 구분이 존재한다.[1]전체 종속형 확인의 일반성을 제한함으로써, 형식 추론은 결정 불가능한 것으로 유지되지만, 형식 추론은 결정 불가능한 것이 된다.
종속적인 ML은 ATS로 대체되었고 더 이상 활발한 개발이 진행되지 않는다.
참조
- ^ 아스피놀 & 호프만 2005. 페이지 75.
추가 읽기
- Xi, Hongwei (March 2007). "Dependent ML: An Approach to Practical Programming with Dependent Types". Journal of Functional Programming. 17 (2): 215–286. doi:10.1017/S0956796806006216. S2CID 45996427.
- 데이비드 아스피놀과 마틴 호프만(2005년)."종속 유형".Pierce에서 Benjamin C. (ed.) 유형 및 프로그래밍 언어의 고급 주제.MIT 프레스.
외부 링크
