"실제"프로그래밍에 가장 적합한 종속 형식 언어?

Question

은 실제로 프로그래밍 언어를 실제 응용 프로그램 개발에 사용할 수 있습니까?

이

내 생각은 중요하다는 것을, 몇 가지 사항은 다음과 같습니다

• 문서
• 예제 프로그램
• 표준 라이브러리
• 또는 사용 적어도 쉽게 외국 기능 인터페이스
• 실제 작업을 위해 언어를 사용하는 사람들의 커뮤니티
• 도구 지원

Answer 1

하스켈과의 호환성이 있으므로 Agda을 제안합니다. 따라서 아마도 최상의 라이브러리를 사용하는 종속 형 언어 일 것입니다. 문서 및 튜토리얼은 약간 모자라지만 도구 지원도 그다지 좋지 않습니다. 솔직히 말하면, 대부분의 종속 형 언어는 현재 완전히 개발되지 않았습니다.

언어가 GADT's 인 약간 약한 요구에 대신 대처하면 매우 잘 유지되는 두 가지 옵션 인 스칼라와 하스켈이 있습니다. IMHO GADT를 사용하여 종속 유형의 이점 대부분을 얻습니다. 그리고 당신은 타이핑 검사를 결정할 수 있습니다.

스칼라와 하스켈 모두 크고 잘 문서화 된 라이브러리, 작업 도구 체인 및 FFI (Java 및 C 각각)가 있습니다. 둘 다 실제 세계 문제를 해결하기 위해 커뮤니티를 사용합니다. parsing 및 webdevelopment.

Answer 2

Agda는 범용 프로그래밍 언어로 설계되지 않았습니다. ATS는 하위 레벨 프로그래밍을 위해 설계된 종속 형식 언어이지만 Agda보다 다소 덜 우아합니다. Idris는 성능이 우수한 응용 프로그램 수준의 프로그램을 위해 고안된 상용 언어 형식의 언어입니다.

Answer 3

허용되는 대답에는 잘못된 정보가 들어 있습니다. 긍정/종료/유니버스 검사를 해제하지 않는 한 Agda의 Typechecking은 결정할 수 없습니다. 더욱이 무한한 프로세스는 Agda에서 프로그래밍 할 수 있습니다. 하스켈에서는 입출력 프로세스가 프로그래밍 할 수있는 것과 같습니다 : 유일한 제한은 실행될 때 무한한 프로세스가 무한대로 전개 될 수 없다는 것입니다.의 형식 검사 중 . Agda에서 Turing Machine 시뮬레이터를 구현할 수 있습니다. 거짓말을 말하면 타이프 검사기를 끝내거나 설득하여 무제한 방식으로 실행하도록 보장 할 수 없습니다.

그러나 "실제"프로그래밍과 관련하여 의존적으로 입력 된 언어가 아직 실험 단계에 있다는 것에 동의합니다. 우리는 아직 무거운 임무 개발을 지원할 수는 없지만, 예전에는 기능 언어와 같이 미래를 염두에 둔 사람들 사이에서 중요한 취미를 견뎌 낼 수 있습니다.

트위터 (Twey)가 제안한 이드리스는 "실제 세계"의존형 언어에 가장 가까운 후보입니다. Agda보다 물건을 완성하는 데 훨씬 더 집중했습니다. 나는 Agda를 종속 형식의 프로그래밍 뒤에있는 아이디어와 잘 어울리는 도구로 추천하지만, Idris가 더 실용적인 옵션입니다.

이 토론에서 하스켈의 최신 버전을 고려해 볼 가치가 있다고 생각합니다. GHC 이후 7.4에서, Haskell은 타입 레벨 데이터의 유용한 개념을 지원하기 시작했으며 적어도 싱글 톤 기법 (실제로는 kludge)을 사용하여 런타임 값에 따라 유형을 가질 수 있습니다 (정적 변수 동등한 런타임 값에 제약됨). 하스켈은 종속 유형을 실험하는 초기 단계에서 실제 "실제"언어입니다.