시작하기

시작하기 (Getting Started)

사전 요구사항 (Prerequisites)

Idris를 설치하기 전에 필요한 라이브러리와 도구를 모두 갖추고 있는지 확인해야 해요. 필요한 것:

  • 비교적 최신 버전의 GHC. 현재 우리가 테스트하는 가장 이른 버전은 7.10.3이에요.

  • GNU 다중 정밀 산술 라이브러리(GMP, GNU Multiple Precision Arithmetic Library). MacPorts/Homebrew와 모든 주요 Linux 배포판에서 구할 수 있어요.

다운로드와 설치 (Downloading and Installing)

사전 요구사항을 모두 갖췄다면 Idris를 설치하는 가장 쉬운 방법은 다음과 같이 입력하는 것이에요:

cabal update; cabal install idris

이 명령은 Hackage에 공개된 최신 버전을 종속성과 함께 설치해요. 다만 가장 최신 개발 버전을 원한다면, 빌드 지침과 함께 GitHub의 https://github.com/idris-lang/Idris-dev 에서 찾을 수 있어요.

이전에 Cabal로 아무것도 설치한 적이 없다면 Idris가 경로(path)에 없을 수 있어요. Idris 실행 파일이 발견되지 않으면 ~/.cabal/bin을 $PATH 환경 변수에 추가했는지 확인해야 해요. Mac OS X 사용자는 대신 ~/Library/Haskell/bin을 추가해야 할 수 있고, Windows 사용자는 일반적으로 Cabal이 %HOME%\AppData\Roaming\cabal\bin에 프로그램을 설치하는 것을 발견할 거예요.

설치가 성공했는지 확인하고 첫 Idris 프로그램을 작성하려면, hello.idr라는 파일을 만들어 다음 내용을 넣어보세요:

module Main

main : IO ()
main = putStrLn "Hello world"

Haskell에 익숙하다면 그 프로그램이 무엇을 하고 어떻게 작동하는지 꽤 분명할 거예요. 하지만 아니라면 나중에 세부 사항을 설명할게요. 셸 프롬프트에서 idris hello.idr -o hello를 입력하면 프로그램을 실행 파일로 컴파일할 수 있어요. 그러면 실행할 수 있는 hello라는 실행 파일이 생성돼요:

$ idris hello.idr -o hello
$ ./hello
Hello world

달러 기호 $가 셸 프롬프트를 나타낸다는 점에 유의하세요!

Idris 명령의 유용한 옵션 몇 가지:

  • -o prog — prog라는 실행 파일로 컴파일함.

  • --check — 대화형 환경을 시작하지 않고 파일과 그 종속성을 타입 검사함.

  • --package pkg — 패키지를 종속성으로 추가함. 예: contrib 패키지를 사용하려면 --package contrib.

  • --help — 사용 요약과 명령줄 옵션을 표시함.

대화형 환경 (The Interactive Environment)

셸 프롬프트에서 idris를 입력하면 대화형 환경이 시작돼요. 대략 다음과 같은 내용이 보일 거예요:

$ idris
    ____    __     _
   /  _/___/ /____(_)____
   / // __  / ___/ / ___/     Version 1.3.3
 _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
/___/\__,_/_/  /_/____/       Type :? for help

Idris>

이것은 식의 평가와 타입 검사, 정리 증명(theorem proving), 컴파일, 편집, 그리고 다양한 다른 작업을 허용하는 ghci 스타일 인터페이스를 제공해요. :? 명령은 지원되는 명령 목록을 보여줘요. 아래에서 hello.idr가 로드되고 main의 타입이 검사된 다음 프로그램이 hello 실행 파일로 컴파일되는 예시 실행을 볼 수 있어요. 파일의 타입 검사가 성공하면 파일의 바이트코드 버전(이 경우 hello.ibc)이 생성되어 나중에 로딩을 빠르게 해줘요. 소스 파일이 바뀌면 바이트코드가 재생성돼요.

$ idris hello.idr
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.3.3
  _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Type checking ./hello.idr
*hello> :t main
Main.main : IO ()
*hello> :c hello
*hello> :q
Bye bye
$ ./hello
Hello world

출처: 문서