문법 안내

문법 안내 (Syntax Guide)

Idris의 전반적인 문법을 한눈에 정리한 문서예요. 이 문서에 나오는 예시들은 대부분 Idris 튜토리얼에서 가져온 것들이에요.

출처: 문서

본문

소스 파일 구조 (Source File Structure)

소스 파일은 다음과 같은 요소들로 구성돼요.

  • 선택적인 모듈 헤더(Module Header)
  • 0개 이상의 import 문(Imports)
  • 0개 이상의 선언(declarations), 예를 들어 변수(Variables), 데이터 타입(Data types) 등

예를 들어:

module MyModule   -- module header

import Data.Vect  -- an import

%default total    -- a directive

foo : Nat         -- a declaration
foo = 5

모듈 헤더 (Module Header)

파일은 module 키워드로 시작하는 모듈 헤더로 시작할 수 있어요.

module Semantics

모듈 이름은 계층적일 수 있으며, 부분들은 .로 구분돼요.

module Semantics.Transform

각 파일은 단 하나의 모듈만 정의할 수 있어요. 이 모듈에는 그 파일에 정의된 모든 것이 포함돼요.

선언에서와 마찬가지로, docstring을 사용해 모듈에 대한 문서를 제공할 수 있어요.

||| Implementation of predicate transformer semantics.
module Semantics.Transform

임포트 (Imports)

import 문은 다른 모듈에 있는 이름들을 현재 모듈에서 사용할 수 있게 해줘요.

import Data.Vect

임포트된 모듈의 모든 선언은 그 파일에서 사용할 수 있어요. 이름이 모호한 경우 — 예를 들어 여러 모듈에서 임포트했거나, 여러 보이는 이름공간(namespace)에 나타나는 경우 — 경상 이름(Qualified Names)을 사용해 모호성을 해결할 수 있어요. (종종 컴파일러가 관련된 타입들을 사용해 모호성을 알아서 해결해주기도 해요.)

임포트된 모듈에는 별칭(alias)을 부여해 경상 이름을 더 간결하게 만들 수 있어요.

import Data.Vect as V

import로 보이게 된 이름들은 기본적으로는 현재 작성 중인 모듈의 사용자에게 재-export되지 않는다는 점을 유의하세요. 이는 import public을 사용하면 가능해요.

import public Data.Vect

변수 (Variables)

변수는 항상 한 줄에 타입을, 다음 줄에 값을 정의하는 방식으로 정의돼요. 문법은 다음과 같아요.

<id> : <type>
<id> = <value>

예시:

x : Int
x = 100
hello : String
hello = "hello"

타입 (Types)

Idris에서 타입은 일급 값(first class value)이에요. 그래서 타입 선언은 단지 타입이 Type인 변수를 선언하는 것과 같아요. Idris에서 타입을 나타내는 변수는 반드시 대문자일 필요는 없어요. 예시:

MyIntType : Type
MyIntType = Int

더 흥미로운 예시:

MyListType : Type
MyListType = List Int

타입을 대문자로 쓰는 것이 필수는 아니지만, 묵시적 인자(implicit argument)를 생성하는 규칙상 종종 대문자로 쓰는 것이 좋아요.

데이터 타입 (Data types)

Idris는 데이터 타입을 정의하는 두 가지 종류의 문법을 제공해요. 처음 것은 Haskell 스타일 문법으로, 일반적인 대수적 데이터 타입(algebraic data type)을 정의해요. 예를 들어:

data Either a b = Left a | Right b

또는

data List a = Nil | (::) a (List a)

두 번째이자 더 일반적인 종류의 데이터 타입은 Agda 또는 GADT 스타일 문법으로 정의돼요. 이 문법은 어떤 값들에 의해 매개변수화(parameterised)된 데이터 타입을 정의해요 (Vect 예시에서는 Nat 타입의 값과 Type 타입의 값으로 매개변수화돼요).

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

타입 생성자의 시그니처는 의존 타입(dependent types)을 사용할 수 있어요.

data DPair : (a : Type) -> (a -> Type) -> Type where
  MkDPair : {P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P

레코드 (Records)

생성자가 하나이고 필드가 여럿인 데이터 타입을 위한 특별한 문법이 있어요.

record A a where
  constructor MkA
  foo, bar : a
  baz : Nat

이것은 생성자뿐만 아니라 각 필드에 대한 getter와 setter 함수도 정의해요.

MkA : a -> a -> Nat -> A a
foo : A a -> a
set_foo : a -> A a -> A a

레코드 필드의 타입은 다른 필드의 값에 의존할 수 있어요.

record Collection a where
  constructor MkCollection
  size : Nat
  items : Vect size a

Setter 함수는 의존 타입을 사용하지 않는 필드에 대해서만 제공돼요. 위 예시에서 set_size와 set_items는 둘 다 정의되지 않아요.

공-데이터 (Co-data)

무한 데이터 구조는 codata 키워드로 도입할 수 있어요.

codata Stream : Type -> Type where
  (::) a -> Stream a -> Stream a

이것은 다음 형태의 문법적 설탕(syntactic sugar)이에요. 그리고 보통 이 형태가 더 선호돼요.

data Stream : Type -> Type where
  (::) a -> Inf (Stream a) -> Stream a

정의된 타입의 모든 발생은 생성자 인자에서 Inf 타입 생성자로 감싸져요(wrapped). 이는 데이터 생성자가 적용될 때 두 번째 인자의 평가를 지연(delay)시키는 효과가 있어요.

Inf 인자는 Delay를 사용해 구성되고 (Delay는 Idris가 묵시적으로 삽입해줘요), Force를 사용해 평가돼요 (역시 묵시적으로 삽입돼요). 게다가 Delay 아래의 재귀 호출은 전체성 검사기(totality checker)를 통과하려면 생성자로 보호되어야 해요.

연산자 (Operators)

산술 (Arithmetic)

x + y
x - y
x * y
x / y
(x * y) + (a / b)

동등과 관계 (Equality and Relational)

x == y
x /= y
x >= y
x > y
x <= y
x < y

조건 (Conditional)

x && y
x || y
not x

조건문 (Conditionals)

If Then Else

if <test> then <true> else <false>

Case 표현식 (Case Expressions)

case <test> of
    <case 1>  => <expr>
    <case 2>  => <expr>
    ...
    otherwise => <expr>

함수 (Functions)

이름 있는 함수 (Named)

이름 있는 함수는 타입 다음에 정의가 오는 방식으로 변수와 같은 방법으로 정의돼요.

<id> : <argument type> -> <return type>
<id> arg = <expr>

예시:

plusOne : Int -> Int
plusOne x = x + 1

함수는 여러 입력을 가질 수도 있어요. 예를 들어:

makeHello : String -> String -> String
makeHello first last = "hello, my name is " ++ first ++ " " ++ last

함수는 이름 있는 인자(named arguments)를 가질 수도 있어요. docstring에서 매개변수에 주석을 달려면 이것이 필요해요. 다음은 위와 같은 makeHello 함수지만, 이름 있는 매개변수를 사용하고 docstring에도 주석을 단 형태예요.

||| Makes a string introducing a person
||| @first The person's first name
||| @last The person's last name
makeHello : (first : String) -> (last : String) -> String
makeHello first last = "hello, my name is " ++ first ++ " " ++ last

Haskell처럼 Idris 함수는 패턴 매칭으로 정의할 수 있어요. 예를 들어:

sum : List Int -> Int
sum []        = 0
sum (x :: xs) = x + (sum xs)

마찬가지로 case 분석은 다음과 같이 생겼어요.

answerString : Bool -> String
answerString False = "Wrong answer"
answerString True = "Correct answer"

의존 함수 (Dependent Functions)

의존 함수는 반환 값의 타입이 입력 값에 의존하는 함수예요. 의존 함수를 정의하려면 이름 있는 매개변수를 사용해야 해요. 그 이유는 매개변수가 반환 타입에 나타나기 때문이에요. 예를 들어:

zeros : (n : Nat) -> Vect n Int
zeros Z     = []
zeros (S k) = 0 :: (zeros k)

이 예시에서 반환 타입은 Vect n Int인데, 이는 입력 매개변수 n에 의존하는 표현식이에요.

익명 함수 (Anonymous)

익명 함수의 인자들은 쉼표로 구분돼요.

(\x => <expr>)
(\x, y => <expr>)

수식어 (Modifiers)

가시성 (Visibility)

public export
export
private

전체성 (Totality)

total
partial
covering

패턴 매칭이 어느 정도까지 종료(terminating)되고/또는 철저(exhaustive)한지 명시적으로 설정해요. partial 패턴 매칭은 아무 가정도 하지 않아요. covering 패턴 매칭은 패턴 매칭이 모든 절(clause)에 대해 철저함을 보장해요. 게다가 total 패턴 매칭은 절의 평가의 철저성과 종료 둘 다를 강제해요.

묵시적 강제 변환 (Implicit Coercion)

implicit

옵션 (Options)

%export
%hint
%no_implicit
%error_handler
%error_reverse
%reflection
%specialise [<name list>]

기타 (Misc)

경상 이름 (Qualified Names)

같은 이름을 가진 여러 선언이 보이면, 그 이름을 사용하는 것은 모호한 상황을 만들 수 있어요. 컴파일러는 관련된 타입들을 사용해 모호성을 해결하려 시도해요. 그것이 불가능하다면 — 예를 들어 같은 이름을 가진 선언들이 동일한 타입 시그니처를 가져서 — 경상 이름을 사용해 상황을 해결할 수 있어요.

경상 이름은 심볼의 이름공간(namespace)이 접두사로 붙고 .로 구분된 형태예요.

Data.Vect.length

이것은 Data.Vect에서 온 length 선언을 구체적으로 참조해요.

경상 이름은 두 가지 서로 다른 약어(shorthand)로 쓸 수 있어요.

  • 별칭으로 임포트된 모듈의 이름들은 그 별칭으로 한정할 수 있어요.
  • 이름은 해당 이름공간의 가장 짧은 유일한 접미사(suffix)로 한정할 수 있어요. 예를 들어 위의 length 경우는 아마 Vect.length로 줄일 수 있어요.

주석 (Comments)

-- Single Line
{- Multiline -}
||| Docstring (goes before definition)

여러 줄 문자열 리터럴 (Multi line String literals)

foo = """
this is a
string literal"""

지시어 (Directives)

%lib <path>
%link <path>
%flag <path>
%include <path>
%hide <function>
%freeze <name>
%access <accessibility>
%default <totality>
%logging <level 0--11>
%dynamic <list of libs>
%name <list of names>
%error_handlers <list of names>
%language <extension>

더 알아보기 (Learn more)