이드리스 (프로그래밍 언어)

이드리스(Idris)는 의존형, 양적 유형 이론(quantitative type theory) 주석, 선택적 느긋한 계산법, 그리고 전역성 검사기(totality checker)와 같은 기능을 갖춘 순수 함수형 프로그래밍 언어다. 이드리스는 하스켈과 유사한 범용 프로그래밍 언어로 설계되었으나, 증명 보조기로도 사용될 수 있다.

이드리스의 자료형 체계는 Agda와 유사하다. Agda와 비교했을 때, 이드리스는 부작용의 관리와 임베디드 도메인 특화 언어(EDSL) 지원을 우선시한다. 이드리스는 코드 생성과 런타임 시스템을 제공하는 모듈식 백엔드에 의해 컴파일된다. 이드리스 컴파일러는 Chez Scheme, 래킷, 자바스크립트(브라우저 및 Node.js 기반 모두), C를 위한 백엔드를 포함한다. 다른 플랫폼을 위한 추가적인 제3자 백엔드들도 사용 가능하다.

이드리스라는 이름은 1970년대 영국의 어린이 텔레비전 프로그램인 아이버 더 엔진에 등장하는 노래하는 용의 이름에서 따왔다.

 특징 
이드리스는 비교적 주류인 함수형 프로그래밍 언어의 여러 특징과 증명 보조기에서 빌려온 특징들을 결합하고 있다.

 함수형 프로그래밍 
이드리스의 구문은 하스켈의 구문과 많은 유사성을 보여준다. 이드리스로 작성한 헬로 월드 프로그램은 다음과 같다.
module Main

main : IO ()
main = putStrLn "Hello, World!"

이 프로그램과 하스켈의 대응하는 프로그램 사이의 유일한 차이점은 메인 함수의 타입 서명에서 콜론이 두 개가 아닌 한 개라는 점과, 모듈 선언에서 "where"라는 단어가 생략되었다는 점이다.

 귀납적 및 매개변수 다형성 데이터 타입 
이드리스는 귀납적으로 정의된 데이터 타입과 매개변수 다형성을 지원한다. 이러한 타입은 전통적인 하스켈 98 스타일의 구문으로 정의할 수 있다:

data Tree a = Node (Tree a) (Tree a) | Leaf a

또는 더 일반적인 일반화된 대수적 데이터 타입(GADT) 스타일의 구문으로도 정의할 수 있다:

data Tree : Type -> Type where
    Node : Tree a -> Tree a -> Tree a
    Leaf : a -> Tree a

 의존형 
의존형을 사용하면 값이 타입에 나타날 수 있다. 사실상 프로그램이 실행되기 전인 컴파일 타임에 모든 값 수준의 계산을 수행할 수 있다. 다음은 프로그램 실행 전에 길이를 알 수 있는 리스트 타입(전통적으로 벡터라고 불림)의 정의다:

data Vect : Nat -> Type -> Type where
  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
append (x :: xs) ys = x :: append xs ys

append 함수는 a 타입의 요소 m개를 가진 벡터를 a 타입의 요소 n개를 가진 벡터 뒤에 붙인다. 입력 벡터의 정확한 타입이 값에 의존하기 때문에, 결과 벡터가 정확히 (n + m)개의 요소를 갖는다는 것을 컴파일 타임에 확신할 수 있다.
"total"이라는 단어는 전역성 검사기(totality checker)를 호출하며, 이 검사기는 함수가 가능한 모든 사례를 다루지 않거나, 무한 루프에 빠지지 않는다는 것을 (자동으로) 증명할 수 없는 경우 오류를 보고한다.

또 다른 일반적인 예는 길이에 대해 매개변수화된 두 벡터의 요소별 덧셈이다:

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

Num a는 타입 a가 타입 클래스 Num에 속함을 의미한다. 한 벡터는 Nil이고 다른 벡터는 숫자인 경우에 대한 매칭 사례가 없음에도 불구하고, 이 함수는 전역적(total)인 것으로 성공적으로 타입 검사를 통과한다. 자료형 체계가 두 벡터의 길이가 같음을 증명할 수 있기 때문에, 해당 사례가 발생하지 않을 것임을 컴파일 타임에 확신할 수 있으며 함수 정의에 그 사례를 포함할 필요가 없다.

 증명 보조기 기능 
의존형은 프로그램의 대부분의 속성을 인코딩할 수 있을 만큼 강력하며, 이드리스 프로그램은 컴파일 타임에 불변량을 증명할 수 있다. 이로 인해 이드리스는 증명 보조기가 된다.

증명 보조기와 상호작용하는 두 가지 표준 방법이 있다. 일련의 전술(tactic) 호출을 작성하거나(Coq 스타일), 증명 항을 대화식으로 정교화하는 것(에피그램–Agda 스타일)이다. 이드리스는 두 가지 상호작용 모드를 모두 지원하지만, 사용 가능한 전술 세트는 아직 Coq만큼 유용하지는 않다.

 코드 생성 
이드리스는 증명 보조기를 포함하고 있기 때문에, 증명을 전달하도록 프로그램을 작성할 수 있다. 이를 단순하게 처리하면 이러한 증명들이 런타임에도 남아있게 된다. 이드리스는 사용되지 않는 항을 공격적으로 삭제함으로써 이러한 함정을 피하는 것을 목표로 한다.

기본적으로 이드리스는 C를 통해 네이티브 코드를 생성한다. 공식적으로 지원되는 다른 백엔드는 자바스크립트를 생성한다.

 이드리스 2 
이드리스 2는 양적 유형 이론에 기반하여 선형 자료형 체계를 깊이 있게 통합한 새로운 자가 호스팅 버전의 언어다. 현재 스킴과 C로 컴파일된다.

 같이 보기 
 증명 보조기 목록
 전체 함수형 프로그래밍

 각주 

 외부 링크 
 , 문서, 자주 묻는 질문, 예제
 Hackage 저장소의 이드리스
 이드리스 언어 문서 (튜토리얼, 언어 레퍼런스 등)

분류:함수형 프로그래밍 언어
분류:하스켈 프로그래밍 언어 계열
분류:2007년 소프트웨어
분류:패턴 매칭 프로그래밍 언어
분류:정적 타입 프로그래밍 언어
분류:고급 프로그래밍 언어
분류:2007년 개발된 프로그래밍 언어
분류:크로스 플랫폼 자유 소프트웨어
분류:BSD 라이선스 소프트웨어