Idris(프로그래밍 언어)
Idris (programming language) |
| 패러다임 | 기능하다 |
|---|---|
| 설계자 | 에드윈 브래디 |
| 처음 등장한 | 전([1] |
| 안정된 릴리스 | 1.3.3[2] / 2020년 5월 , 전( |
| 프리뷰 릴리즈 | 0.5.1 (Idris [3]2) / 2021년 9월 20일; 전 ( |
| OS | 크로스 플랫폼 |
| 면허증. | BSD |
| 파일 이름 확장자 | .timeout, .timeoutr |
| 웹 사이트 | idris-lang |
| 영향을 받다 | |
| Agda, Clean,[4] Coq,[5] 에피그램, F#, Haskell,[5] ML,[5] Rust[4] | |
Idris는 종속 유형, 선택적 지연 평가 및 전체성 검사와 같은 기능을 가진 순수 기능 프로그래밍 언어입니다.Idris는 증명 보조로 사용될 수 있지만, Haskell과 유사한 범용 프로그래밍 언어로 설계되어 있습니다.
Idris 유형 시스템은 Agda와 유사하며, 증명은 정교자 [6]반성을 통한 전술(이론 증명 기능/절차)을 포함한 Coq와 유사합니다.Agda 및 Coq와 비교하여 Idris는 부작용 관리와 임베디드 도메인 고유의 언어 지원을 우선시합니다.Idris는 C(Cheney 알고리즘을 사용한 커스텀 복사 가비지 컬렉터에 기반)와 JavaScript(브라우저 기반과 Node.js 기반)로 컴파일됩니다.JVM, CIL, LLVM [7]등 다른 플랫폼용 서드파티 코드 생성기가 있습니다.
이드리스는 1970년대 영국 어린이 텔레비전 프로그램인 아이보르 더 [8]엔진에 나오는 노래하는 용의 이름을 따서 붙여졌다.
특징들
Idris는 비교적 주류 함수 프로그래밍 언어의 많은 특징과 증명 보조자로부터 빌린 특징을 결합합니다.
기능 프로그래밍
Idris의 구문은 Haskell의 구문과 많은 유사점을 보여준다.Idris의 hello world 프로그램은 다음과 같습니다.
모듈 메인 : IO ( ) 메인 = putStrLn "안녕하세요, 월드!"이 프로그램과 Haskell 등가물의 유일한 차이점은 메인 함수의 형식 시그니처에 있는 단일 콜론(이중 대신)과 단어 누락입니다.where모듈 [9]선언에 "가 표시됩니다.
유도 및 파라메트릭 데이터 유형
Idris는 유도적으로 정의된 데이터 유형과 파라메트릭 다형을 지원합니다.이러한 유형은 기존의 "Haskell98"과 같은 구문에서 모두 정의할 수 있습니다.
데이터 트리 a = 노드(트리 a)(트리 a) 리프 a또는 보다 일반적인 GADT와 같은 구문에서 다음과 같이 입력합니다.
데이터 트리 : 입력 -> 노드 : 트리 a -> 트리 a -> 트리 a 리프 : -> 트리 a 에 입력합니다.종속 유형
종속 유형을 사용하면 값이 유형에 표시될 수 있습니다. 실제로 유형 검사 중에 모든 값 수준 계산을 수행할 수 있습니다.다음은 프로그램이 실행되기 전에 길이가 알려진 목록 유형(일반적으로 벡터)을 정의합니다.
data vect : Nat -> Type -> Nil : Vect 0 a ( : : : ) : ( x : a ) -> ( xs : Vect n a ) -> Vect ( n + 1) a 를 입력합니다.이 유형은 다음과 같이 사용할 수 있습니다.
total append : Vect n a -> Vect m a -> Vect (n + m)a append Nil ys = ys = x :: append xs ys함수append벡터를 부가하다m활자 요소a의 벡터까지n활자 요소a입력 벡터의 정확한 유형은 값에 따라 달라지기 때문에 컴파일 시 결과 벡터가 정확히 (를) 가질 수 있습니다.n+m)의 유형 요소a. "라는 단어 "total함수가 가능한 모든 경우를 커버하지 않거나 무한 루프에 들어가지 않는 것을 (자동으로) 증명할 수 없는 경우 오류를 보고하는 토탈리티 체커를 호출합니다.
또 다른 일반적인 예로는 두 벡터의 길이에 걸쳐 매개 변수화된 두 벡터를 쌍으로 추가하는 것입니다.
전체 쌍 추가 : Num a = > Vect n a - > Vect n a - > Vect n 쌍 추가 Nil = Nil 쌍 추가 (x : xs ) = x + y : :: 쌍 추가 xsNuma는 a타입이 type 클래스에 속함을 나타냅니다. Num. 이 함수는 대소문자가 일치하지 않더라도 전체적으로는 정상적으로 타이프 체크됩니다.Nil한 벡터와 다른 벡터에 숫자가 있습니다.타입 시스템은 벡터의 길이가 같다는 것을 증명할 수 있기 때문에 컴파일 시에 그 케이스가 발생하지 않는다는 것을 확신할 수 있으며, 그 케이스를 함수의 정의에 포함할 필요가 없다.
프루프 어시
종속 유형은 프로그램의 대부분의 속성을 인코딩할 수 있을 만큼 강력하며, Idris 프로그램은 컴파일 시 불변성을 증명할 수 있습니다.이것으로 이드리스는 증명 보조원이 된다.
증명 보조원과의 상호작용에는 두 가지 표준 방법이 있습니다. 일련의 전술 호출(Coq 스타일)을 작성하거나 증명 용어를 대화식으로 상세하게 기술하는 방식(Epigram/Agda 스타일)입니다.Idris는 두 가지 상호작용 모드를 모두 지원하지만, 이용 가능한 전술의 [vague]세트는 Coq만큼 유용하지는 않습니다.
코드 생성
Idris는 증명 도우미를 포함하고 있기 때문에, Idris 프로그램은 증명서를 전달하기 위해 작성될 수 있다.순진하게 다루면, 그러한 증거는 런타임에 남는다.Idris는 사용하지 않는 [10][11]용어를 적극적으로 지움으로써 이러한 함정을 피하는 것을 목표로 하고 있다.
기본적으로는 Idris는 C를 통해 네이티브 코드를 생성합니다.공식적으로 지원되는 다른 백엔드는 JavaScript를 생성합니다.
이드리스 2
Idris 2는 양적 유형 이론에 기초한 선형 유형 시스템을 깊이 통합한 새로운 자기 호스트 언어 버전입니다.현재는 Scheme와 [12]C로 컴파일 되어 있습니다.
「 」를 참조해 주세요.
레퍼런스
- ^ Brady, Edwin (12 December 2007). "Index of /~eb/darcs/Idris". University of St Andrews School of Computer Science. Archived from the original on 2008-03-20.
- ^ "Release 1.3.3". Retrieved 2020-05-25.
- ^ "Idris 2 version 0.5.1 Released". www.idris-lang.org. Retrieved 2021-10-16.
- ^ a b "Uniqueness Types". Idris 1.3.1 Documentation. Retrieved 2019-09-26.
- ^ a b c "Idris, a language with dependent types". Retrieved 2014-10-26.
- ^ "Elaborator Reflection — Idris 1.3.2 documentation". Retrieved 27 April 2020.
- ^ "Code Generation Targets — Idris 1.1.1 documentation". docs.idris-lang.org.
- ^ "Frequently Asked Questions". Retrieved 2015-07-19.
- ^ "Syntax Guide — Idris 1.3.2 documentation". Retrieved 27 April 2020.
- ^ "Erasure By Usage Analysis — Idris 1.1.1 documentation". idris.readthedocs.org.
- ^ "Benchmark results". ziman.functor.sk.
- ^ "idris-lang/Idris2". GitHub. Retrieved 2021-04-11.
외부 링크
- Idris 홈페이지(문서 포함)에서는 자주 묻는 질문과 예시를 볼 수 있습니다.
- Hackage 저장소의 Idris
- Idris 언어 문서(튜토리얼, 언어 참조 등)
리스트: 
