소개
소개 (Introduction)
전통적인 프로그래밍 언어에서는 타입(type)과 값(value) 사이에 뚜렷한 구분이 있어요. 예를 들어 Haskell에서 다음은 각각 정수, 문자, 문자 리스트, 임의의 값 리스트를 나타내는 타입이에요:
Int,Char,[Char],[a]
그에 대응해서, 다음 값들은 그 타입들의 원소(inhabitant)의 예시예요:
42,'a',"Hello world!",[2,3,4,5,6]
하지만 의존 타입(dependent types)을 가진 언어에서는 그 구분이 덜 명확해요. 의존 타입은 타입이 값에 "의존"할 수 있게 해줘요 — 다시 말해, 타입은 일급(first class) 언어 구성물이며 다른 값처럼 조작될 수 있어요. 표준 예는 주어진 길이의 리스트 [1] 타입인 Vect n a인데, 여기서 a는 원소 타입이고 n은 리스트의 길이이며 임의의 용어(term)가 될 수 있어요.
타입이 값을 포함할 수 있고, 그 값들이 예를 들어 리스트의 길이 같은 속성을 기술할 때, 함수의 타입은 자신의 속성을 기술하기 시작할 수 있어요. 두 리스트의 연결(concatenation)을 예로 들어볼게요. 이 연산은 결과 리스트의 길이가 두 입력 리스트 길이의 합이라는 속성을 가져요. 따라서 벡터를 연결하는 app 함수에 다음 타입을 줄 수 있어요:
app : Vect n a -> Vect m a -> Vect (n + m) a
이 튜토리얼은 의존 타입을 가진 범용 함수형 프로그래밍 언어인 Idris를 소개해요. Idris 프로젝트의 목표는 검증 가능한(verifiable) 범용 프로그래밍에 적합한 의존 타입 언어를 구축하는 것이에요. 이를 위해 Idris는 효율적인 실행 코드 생성을 목표로 하는 컴파일 언어이며, 외부 C 라이브러리와 쉽게 상호작용할 수 있는 가벼운 외부 함수 인터페이스(foreign function interface)도 갖추고 있어요.
대상 독자 (Intended Audience)
이 튜토리얼은 언어에 대한 간략한 소개를 목적으로 하며, Haskell이나 OCaml 같은 함수형 언어에 이미 익숙한 독자를 대상으로 해요.
특히 Haskell 문법에 대한 어느 정도의 친숙함을 가정하지만, 대부분의 개념은 최소한 간단히라도 설명될 거예요. 독자는 또한 의존 타입을 시스템 소프트웨어 작성·검증에 사용하는 데 어느 정도 관심이 있다고 가정해요.
더 천천한 속도로 진행되며 대화형 프로그램 개발을 다루고 예제가 훨씬 많은 심화 소개는 Edwin Brady의 Type-Driven Development with Idris를 참고하면 돼요. Manning에서 구할 수 있어요.
예제 코드 (Example Code)
이 튜토리얼은 Idris에 대해 테스트된 예제 코드를 일부 포함해요. 이 파일들은 Idris 배포판과 함께 제공되어 쉽게 시도해볼 수 있어요. samples 아래에서 찾을 수 있어요. 다만 단순히 불러와 읽기만 하기보다 직접 타이핑해보는 것을 강력히 권장해요.
[1]
일반적으로, 그리고 어쩌면 혼란스럽게도, 의존 타입 프로그래밍 문헌에서는 "벡터(vectors)"라고 부르기도 해요.
출처: 문서