자주 묻는 질문

자주 묻는 질문 (Frequently Asked Questions)

출처: 문서

본문

Agda와 Idris의 차이는 무엇인가요? (What are the differences between Agda and Idris?)

Agda도 Idris처럼 의존 타입을 가진 함수형 언어이며, 의존 패턴 매칭을 지원해요. 둘 다 프로그램과 증명을 작성하는 데 사용될 수 있어요.

하지만 Idris는 처음부터 정리 증명(testing theorems)보다는 범용 프로그래밍을 강조하도록 설계됐어요. 따라서 시스템 라이브러리 및 C 프로그램과의 상호운용성과, 도메인 특화 언어 구현을 위한 언어 구성물을 지원해요. 또한 인터페이스(타입 클래스와 유사)와 do 표기법 같은 더 고수준의 프로그래밍 구성물도 포함해요.

Idris는 여러 백엔드(기본적으로 C와 JavaScript, 플러그인으로 더 추가 가능)를 지원하며, C로 작성된 참조 런타임 시스템에 가비지 컬렉터와 내장 메시지 전달 동시성을 갖추고 있어요.

Idris는 프로덕션에 사용할 준비가 되었나요? (Is Idris production ready?)

Idris는 주로 의존 타입을 사용한 소프트웨어 개발의 가능성을 탐구하기 위한 연구 도구이며, 즉 주요 목표는 (아직) 프로덕션에서 사용할 수 있는 시스템을 만드는 것이 아니에요. 따라서 거친 부분이 몇 가지 있고, 빠진 라이브러리도 많아요. 아무도 Idris에 풀타임으로 일하지 않고 있으며, 우리는 지금 이 시스템을 스스로 다듬을 자원이 없어요. 그러므로 비즈니스를 그 위에 세우는 것은 권장하지 않아요!

그렇지만 Idris를 프로덕션에 적합하게 만드는 데 기여하는 것들은 매우 환영해요 — 여기에는 (다음에 국한되지 않음) 추가 라이브러리 지원, 런타임 시스템 다듬기(그리고 그것이 견고함을 보장하기), JVM 백엔드 제공·유지 등이 포함돼요.

표준 라이브러리에 대한 문서? 함수 목록은? (Is there some documentation for the standard lib? List of functions?)

배포된 패키지에 대한 API 문서는 documentation 페이지에 나열되어 있어요.

안타깝게도 Idris의 기본 프렐류드와 배포된 패키지는 문서와 관련해 반드시 완전하지는 않아요. 함수를 찾는 다른 방법은 다음과 같아요:

  • REPL 명령: :apropos를 사용해 문서와 함수 이름에서 텍스트를 검색.

  • :search를 사용해 주어진 타입의 함수를 검색.

  • :browse를 사용해 주어진 네임스페이스의 내용을 나열.

  • REPL의 자동 완성 기능 사용.

  • libs/ 소스 코드를 grep.

배포된 패키지에 문서가 부족하다고 생각되면 마음껏 문서를 작성해주세요. 아니면 누군가에게 부탁하세요. Idris에는 풍부한 문서를 제공하는 문법이 있으며, :doc 명령으로 볼 수 있고 생성된 HTML API 문서에 나열돼요.

왜 Idris는 지연 평가(lazy)가 아니라 조급 평가(eager)를 사용하나요? (Why does Idris use eager evaluation rather than lazy?)

Idris는 더 예측 가능한 성능을 위해 조급 평가를 사용해요. 특히 장기 목표 중 하나가 디바이스 드라이버나 네트워크 인프라 같은 효율적이고 검증된 저수준 코드를 작성하는 것이기 때문이에요.

게다가 Idris 타입 시스템은 각 값의 타입, 따라서 각 값의 런타임 형태를 정밀하게 진술할 수 있게 해줘요. 지연 언어에서 타입 Int의 값을 생각해보세요:

thing : Int

런타임에서 thing의 표현은 무엇일까요? 정수를 나타내는 비트 패턴일까요, 아니면 정수를 계산할 어떤 코드를 가리키는 포인터일까요? Idris에서는 이 구분을 타입에서 정밀하게 만들기로 결정했어요:

thing_val : Int
thing_comp : Lazy Int

여기서 thing_val이 구체적인 Int임이 보장된다는 것이 타입에서 분명한 반면, thing_comp는 Int를 만들어낼 계산이에요.

어떻게 느슨한 제어 구조를 만들 수 있나요? (How can I make lazy control structures?)

특수 Lazy 타입을 사용해 제어 구조를 만들 수 있어요. 예를 들어 Idris의 if...then...else...는 ifThenElse라는 함수의 적용으로 펼쳐져요. 불리언에 대한 기본 구현은 라이브러리에서 다음과 같이 정의돼요:

ifThenElse : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
ifThenElse True  t e = t
ifThenElse False t e = e

t와 e에 대한 타입 Lazy a는 그 인자들이 사용될 때만 평가된다는 것, 즉 느슨하게(lazily) 평가된다는 것을 나타내요.

REPL에서의 평가가 기대한 대로 작동하지 않아요. 무슨 일인가요? (Evaluation at the REPL doesn't behave as I expect. What's going on?)

완전히 의존 타입된 언어인 Idris에는 무언가를 평가하는 두 단계, 즉 컴파일 타임과 런타임이 있어요. 컴파일 타임에는 타입 검사를 결정 가능하게 유지하기 위해 전체적(total, 즉 종료하고 모든 가능한 입력을 덮는)으로 알려진 것만 평가해요. 컴파일 타임 평가기는 Idris 커널의 일부이며, Haskell에서 값의 HOAS(고차 추상 구문, higher order abstract syntax) 스타일 표현을 사용해 구현돼요. 여기서 모든 것이 정규 형식을 가진다고 알려져 있으므로, 어느 쪽이든 같은 답을 얻기 때문에 평가 전략은 실제로 중요하지 않아요. 그리고 실제로는 Haskell 런타임 시스템이 선택하는 대로 동작해요.

편의를 위해 REPL은 컴파일 타임의 평가 개념을 사용해요. (평가기가 있기 때문에) 구현하기 더 쉬울 뿐 아니라, 용어가 타입 검사기에서 어떻게 평가되는지 보여주는 데 매우 유용할 수 있어요. 따라서 다음 사이의 차이를 볼 수 있어요:

Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat

Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat

왜 타입에서 인자가 없는 함수를 사용할 수 없나요? (Why can't I use a function with no arguments in a type?)

소문자로 시작하고 어떤 인자에도 적용되지 않는 이름을 타입에서 사용하면, Idris는 그것을 암시적으로 묶인 인자로 취급해요. 예를 들어:

append : Vect n ty -> Vect m ty -> Vect (n + m) ty

여기서 n, m, ty는 암시적으로 묶여요. 이 규칙은 이 이름들 중 어떤 것을 가진 함수가 다른 곳에 정의되어 있더라도 적용돼요. 예를 들어 다음을 가질 수도 있어요:

ty : Type
ty = String

이 경우에도 ty는 append의 타입을 다음과 동등하게 만들기보다는, append 정의에서 여전히 암시적으로 묶인 것으로 간주돼요:

append : Vect n String -> Vect m String -> Vect (n + m) String

...이는 아마 의도한 것이 아닐 거예요! 이 규칙의 이유는, 다른 어떤 컨텍스트도 없이 append의 타입만 보는 것으로 암시적으로 묶인 이름이 무엇인지 분명하게 하기 위함이에요.

타입에서 적용되지 않은 이름을 사용하려면 두 가지 선택지가 있어요. 명시적으로 한정할 수 있어요. 예를 들어 ty가 네임스페이스 Main에 정의되어 있다면 다음을 할 수 있어요:

append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty

대신에, 소문자로 시작하지 않는 이름을 사용할 수 있는데, 이는 결코 암시적으로 묶이지 않아요:

Ty : Type
Ty = String

append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty

관례상, 이름이 타입 동의어로 사용되려면 이 제한을 피하기 위해 대문자로 시작하는 것이 가장 좋아요.

분명히 종료하는 프로그램이 있는데 Idris가 아마 전체적이 아닐 수 있다고 해요. 왜죠? (I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?)

Idris는 정지 문제(Halting Problem)의 결정 불가능성 때문에 프로그램이 종료하는지 일반적으로 결정할 수 없어요. 하지만 확실히 종료하는 몇몇 프로그램은 식별할 수 있어요. Idris는 함수에서 자신으로 돌아오는 재귀 경로를 찾는 "크기 변화 종료(size change termination)"를 사용해 이것을 해요. 그런 경로에는 기본 경우로 수렴하는 인자가 적어도 하나 있어야 해요.

  • 상호 재귀 함수가 지원됨

  • 그러나 경로의 모든 함수는 완전히 적용되어야 함. 특히 고차 적용은 지원되지 않음

  • Idris는 입력의 구문상 더 작은 인자에 대한 재귀 호출을 찾아 기본 경우로 수렴하는 인자를 식별함. 예를 들어 k는 S (S k)의 부분식이므로 k가 S (S k)보다 구문상 더 작지만, (k, k)는 (S k, S k)보다 구문상 더 작지 않음.

종료한다고 믿는 함수가 있는데 Idris가 그렇지 않으면, 프로그램을 재구성하거나 assert_total 함수를 사용할 수 있어요.

Idris는 언제 자체 호스팅(self-hosting)이 되나요? (When will Idris be self-hosting?)

우선순위는 아니지만, 장기적으로는 나쁜 생각이 아니에요. 단기적으로는 자체 호스팅을 지원하기 위해 Idris로 라이브러리(인자 파싱, 시스템 상호작용용 POSIX 호환 라이브러리 같은)를 구현하는 것이 가치 있는 노력일 거예요.

Idris는 우주 다형성(universe polymorphism)이 있나요? Type의 타입은 무엇인가요? (Does Idris have universe polymorphism? What is the type of Type?)

우주 다형성보다는 Idris는 축적적인(cumulative) 우주 계층을 가져요: Type : Type 1, Type 1 : Type 2 등.

축적성(cumulativity)은 x : Type n이고 n <= m이면 x : Type m임을 의미해요. 우주 레벨은 항상 Idris가 추론하며, 명시적으로 지정할 수 없어요. REPL 명령 :type Type 1은 오류를 일으킬 거예요. 어떤 타입의 우주 레벨을 지정하려는 시도도 마찬가지로요.

왜 Idris는 Float64 대신 Double을 사용하나요? (Why does Idris use Double instead of Float64?)

역사적으로 C 언어와 많은 다른 언어들은 크기 32와 64의 부동소수점 수를 나타내기 위해 Float와 Double이라는 이름을 사용해왔어요. Rust와 Julia 같은 더 새로운 언어들은 IEEE 부동소수점 산술 표준(IEEE 754)에 기술된 명명 체계를 따르기 시작했어요. 이것은 단정밀도와 배정밀도 수를 Float32와 Float64로 기술하며, 크기가 타입 이름에 기술돼요.

개발자들이 더 오래된 명명 관례에 익숙하고 Idris 개발자들이 선택했기 때문에, Idris는 C 스타일 관례를 사용해요. 즉 Double이라는 이름이 배정밀도 수를 기술하는 데 사용되며, Idris는 현재 32비트 부동소수점수를 지원하지 않아요.

-ffreestanding이 무엇인가요? (What is -ffreestanding?)

freestanding 플래그는 libs와 컴파일러가 상대 경로에 있는 Idris 바이너리를 빌드하는 데 사용돼요. 이것은 빌드 시점에 설치 디렉터리가 알려지지 않은 바이너리를 빌드하는 데 유용해요. 이 플래그를 전달할 때, IDRIS_LIB_DIR 환경 변수를 idris 실행 파일에 상대적인 Idris libs가 있는 경로로 설정해야 해요. IDRIS_TOOLCHAIN_DIR 환경 변수는 선택 사항이며, 설정되면 Idris가 C 컴파일러를 찾기 위해 그 경로를 사용해요. 예를 들어:

IDRIS_LIB_DIR="./libs" \
IDRIS_TOOLCHAIN_DIR="./mingw/bin" \
CABALFLAGS="-fffi -ffreestanding -frelease" \
make

"Idris"라는 이름은 무슨 뜻인가요? (What does the name "Idris" mean?)

특정 연령의 영국인들은 이 노래하는 용을 잘 알 수도 있어요. 그것이 도움이 안 된다면, 적절한 약어를 발명해보세요 :-).

연산자에 유니코드 문자 지원이 있을까요? (Will there be support for Unicode characters for operators?)

유니코드 연산자를 지원하지 말아야 할 이유가 여러 가지 있어요:

  • 입력하기 어려워요 (예를 들어 남의 코드를 사용한다면 중요). 다양한 에디터에 각자 입력 방식이 있지만, 그것이 무엇인지 알아야 해요.

  • 모든 소프트웨어가 쉽게 지원하지는 않아요. 일부 모바일 이메일 클라이언트, 터미널 기반 IRC 클라이언트, 웹 브라우저 등에서 렌더링 문제가 기록됐어요. 이런 렌더링 문제를 해결하는 방법이 있지만 Idris를 사용하는 진입 장벽이 돼요.

  • 표준 라이브러리에서 빼더라도(어차피 뺄 거예요!), 사람들이 자신의 라이브러리 코드에서 사용하기 시작하는 순간 다른 사람들이 그것을 다뤄야 해요.

  • 너무 많은 문자가 너무 비슷하게 보여요. 우리는 0과 O 사이의 혼동에 충분히 애를 먹었는데, 온갖 종류의 콜론과 괄호까지 걱정하고 싶지 않아요.

  • 유니코드를 과하게 사용하는 경향이 있는 것 같아요. 예를 들어 Agda에서 delay와 force에 샤프와 플랫을 사용하는 것은(아니면 그 반대?) 불필요해 보여요. 단어가 종종 더 나을 때 이런 종류의 것을 장려하고 싶지 않아요.

주의하면 유니코드 연산자가 것을 예쁘게 보이게 할 수 있지만, lhs2TeX도 그렇죠. 아마 몇 년 후에는 상황이 달라지고 소프트웨어가 더 잘 대처해 다시 검토하는 것이 말이 되겠죠. 하지만 지금으로서는 Idris가 연산자에서 임의의 유니코드 기호를 제공하지 않을 거예요.

이것은 Wadler의 법칙(Wadler's Law)이 작용하는 사례처럼 보여요.

이 답변은 다음 pull request에서 Edwin Brady의 응답에 기반해요.

Idris 커뮤니티에 대한 커뮤니티 표준은 어디에서 찾을 수 있나요? (Where can I find the community standards for the Idris community?)

Idris 커뮤니티 표준(Community Standards)은 여기 에 명시되어 있어요.

더 많은 답변은 어디에서 찾을 수 있나요? (Where can I find more answers?)

GitHub 위키에 더 기술적인 질문에 답하고 더 자주 갱신될 수 있는 비공식 FAQ(Unofficial FAQ)가 있어요.

더 알아보기 (Learn more)