타입과 함수
타입과 함수 (Types and Functions)
출처: 문서
본문
원시 타입 (Primitive Types)
Idris는 여러 원시 타입을 정의해요: 수치 연산을 위한 Int, Integer, Double, 텍스트 조작을 위한 Char와 String, 그리고 외부 포인터를 나타내는 Ptr이에요. 값 True와 False를 가진 Bool을 포함해 라이브러리에 선언된 여러 데이터 타입도 있어요. 이 타입들로 일부 상수를 선언할 수 있어요. 다음을 파일 Prims.idr에 입력하고 idris Prims.idr를 입력해 Idris 대화형 환경으로 로드해요:
module Prims
x : Int
x = 42
foo : String
foo = "Sausage machine"
bar : Char
bar = 'Z'
quux : Bool
quux = False
Idris 파일은 선택적 모듈 선언(여기서 module Prims) 뒤에 선택적 import 목록과 선언·정의 모음으로 구성돼요. 이 예에서는 import가 지정되지 않았어요. 하지만 Idris 프로그램은 여러 모듈로 구성될 수 있으며 각 모듈의 정의는 각자 고유한 네임스페이스를 가져요. 이는 Modules and Namespaces 절에서 더 논의돼요. Idris 프로그램을 작성할 때 정의가 주어지는 순서와 들여쓰기 모두가 중요해요. 함수와 데이터 타입은 사용 전에 정의되어야 해요. 부수적으로 각 정의는 타입 선언을 가져야 해요. 예를 들어 위 목록의 x : Int, foo : String을 보세요. 새 선언은 앞선 선언과 같은 들여쓰기 수준에서 시작해야 해요.
대안으로 세미콜론 ;을 사용해 선언을 끝낼 수 있어요.
라이브러리 모듈 prelude가 모든 Idris 프로그램에 자동으로 import되는데, IO, 산술, 데이터 구조, 다양한 공통 함수를 위한 기능을 포함해요. 프렐류드는 여러 산술·비교 연산자를 정의하며, 프롬프트에서 사용할 수 있어요. 프롬프트에서 무언가를 평가하면 답과 답의 타입을 줘요. 예를 들어:
*prims> 6*6+6
42 : Integer
*prims> x == 6*6+6
True : Bool
일반적인 산술·비교 연산자는 모두 원시 타입에 대해 정의돼요. 그것들은 Interfaces 절에서 논의할 인터페이스를 사용해 오버로드되며, 사용자 정의 타입에서 작동하도록 확장될 수 있어요. 불리언 식은 if...then...else 구성물로 테스트할 수 있어요. 예를 들어:
*prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
"The answer!" : String
데이터 타입 (Data Types)
데이터 타입은 Haskell과 유사한 방식과 문법으로 선언돼요. 예를 들어 자연수와 리스트는 다음과 같이 선언될 수 있어요:
data Nat = Z | S Nat -- Natural numbers
-- (zero and successor)
data List a = Nil | (::) a (List a) -- Polymorphic lists
위의 선언들은 표준 라이브러리에서 가져온 것이에요. 단항(unary) 자연수는 0(Z)이거나 다른 자연수의 후임자(S k)일 수 있어요. 리스트는 비어 있거나(Nil), 다른 리스트의 앞에 값이 추가된 것(x :: xs)일 수 있어요.
데이터 타입은 생성자들의 타입만 줘도 선언될 수 있어요. 다음 정의들은 위의 것들과 동등해요:
data Nat : Type where
Z : Nat
S : Nat -> Nat
data List : Type -> Type where
Nil : List a
(::) : a -> List a -> List a
이 문법은 더 장황하지만 더 유연하며, 더 단순한 문법으로는 기술할 수 없는 타입에 사용돼요.
List 선언에서 우리는 중위(infix) 연산자 ::를 사용했어요. 이것 같은 새 연산자는 다음과 같이 고정성(fixity) 선언으로 추가될 수 있어요:
infixr 10 ::
함수, 데이터 생성자, 타입 생성자는 모두 이름으로 중위 연산자를 가질 수 있어요. 그것들은 괄호로 감싸면 접두사(prefix) 형태로 사용될 수 있어요. 예: (::). 중위 연산자는 다음 기호들을 사용할 수 있어요:
:+-*\/=.?|&><!@$%^~#
이 기호들로 만든 일부 연산자는 사용자 정의할 수 없어요. 그것들은 :, =>, ->, <-, =, ?=, |, **, ==>, \, %, ~, ?, !이에요.
함수 (Functions)
함수는 역시 Haskell과 유사한 문법으로 패턴 매칭에 의해 구현돼요. 주요 차이점은 Idris가 모든 함수에 대해 (Haskell의 이중 콜론 ::보다는) 단일 콜론 :을 사용해 타입 선언을 요구한다는 것이에요. 자연수 산술 함수 몇 가지는, 다시 표준 라이브러리에서 가져온 것으로, 다음과 같이 정의될 수 있어요:
-- Unary addition
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
-- Unary multiplication
mult : Nat -> Nat -> Nat
mult Z y = Z
mult (S k) y = plus y (mult k y)
표준 산술 연산자 +와 *도 Nat에 의해 사용되도록 오버로드되며, 위의 함수들을 사용해 구현돼요.
Haskell과 달리 타입과 함수 이름이 대문자로 시작해야 하는지에 대한 제한은 없어요. 함수 이름(위의 plus와 mult), 데이터 생성자(Z, S, Nil, ::), 타입 생성자(Nat, List)가 모두 같은 네임스페이스의 일부예요. 하지만 관례상 데이터 타입과 생성자 이름은 전형적으로 대문자로 시작해요.
이 함수들을 Idris 프롬프트에서 테스트할 수 있어요:
Idris> plus (S (S Z)) (S (S Z))
4 : Nat
Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
12 : Nat
참고 (Note)
(S (S (S (S Z)))) 같은 Nat 원소를 표시할 때 Idris는 그것을 4로 표시해요. plus (S (S Z)) (S (S Z))의 결과는 실제로는 (S (S (S (S Z))))이며, 이는 자연수 4예요. 이것은 Idris 프롬프트에서 확인할 수 있어요:
Idris> (S (S (S (S Z))))
4 : Nat
산술 연산처럼 정수 리터럴도 인터페이스를 사용해 오버로드돼요. 즉 함수를 다음과 같이 테스트할 수도 있다는 뜻이에요:
Idris> plus 2 2
4 : Nat
Idris> mult 3 (plus 2 2)
12 : Nat
그건 그렇고, 컴퓨터에 완벽하게 훌륭한 정수 산술이 내장되어 있는데 왜 단항 자연수가 있느냐고 궁금할 수도 있어요. 그 이유는 주로 단항 숫자가 추론하기 쉬운 매우 편리한 구조를 갖고, 나중에 보게 될 다른 데이터 구조와 연관시키기 쉽기 때문이에요. 하지만 우리는 이 편의가 효율성을 희생하는 것을 원하지 않아요. 다행히 Idris는 Nat(그리고 유사하게 구조화된 타입)와 숫자 사이의 관계를 알고 있어요. 이것은 표현과 plus·mult 같은 함수를 최적화할 수 있다는 뜻이에요.
where 절 (where clauses)
함수는 where 절을 사용해 지역적으로도 정의될 수 있어요. 예를 들어 리스트를 뒤집는 함수를 정의하려면, 새 뒤집힌 리스트를 축적하고 전역적으로 보일 필요가 없는 보조 함수를 사용할 수 있어요:
reverse : List a -> List a
reverse xs = revAcc [] xs where
revAcc : List a -> List a -> List a
revAcc acc [] = acc
revAcc acc (x :: xs) = revAcc (x :: acc) xs
들여쓰기가 중요해요 — where 블록의 함수는 바깥 함수보다 더 들여써야 해요.
참고 (Note)
범위 (Scope)
바깥 범위에서 보이는 어떤 이름이든 (여기서 xs처럼 재정의되지 않았다면) where 절에서도 보여요. 타입에만 나타나는 이름은 타입 중 하나의 매개변수라면 — 즉 전체 구조에 걸쳐 고정되어 있다면 — where 절에서 범위 안에 있을 거예요.
함수뿐 아니라 where 블록은 로컬 데이터 선언도 포함할 수 있어요. 다음에서 MyLT는 foo 정의 밖에서는 접근할 수 없어요:
foo : Int -> Int
foo x = case isLT of
Yes => x*2
No => x*4
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
일반적으로 where 절에서 정의된 함수는 최상위 함수처럼 타입 선언이 필요해요. 하지만 함수 f의 타입 선언은 다음의 경우 생략될 수 있어요:
-
f가 최상위 정의의 오른쪽에 나타남 -
f의 타입이 첫 번째 적용에서 완전히 결정될 수 있음
따라서 예를 들어 다음 정의들은 합법적이에요:
even : Nat -> Bool
even Z = True
even (S k) = odd k where
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c Z, d (S Z)]
where c x = 42 + x
d y = c (y + 1 + z y)
where z w = y + w
홀 (Holes)
Idris 프로그램은 프로그램의 불완전한 부분을 나타내는 홀(holes)을 포함할 수 있어요. 예를 들어 "Hello world" 프로그램에서 인사말에 대한 홀을 남길 수 있어요:
main : IO ()
main = putStrLn ?greeting
문법 ?greeting은 아직 쓰지 않은 프로그램의 일부를 나타내는 홀을 도입해요. 이것은 유효한 Idris 프로그램이며, greeting의 타입을 확인할 수 있어요:
*Hello> :t greeting
--------------------------------------
greeting : String
홀의 타입을 확인하는 것은 범위 안에 있는 변수들의 타입도 보여줘요. 예를 들어 even의 불완전한 정의가 주어졌을 때:
even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs
even_rhs의 타입을 확인하고 기대 반환 타입과 변수 k의 타입을 볼 수 있어요:
*Even> :t even_rhs
k : Nat
--------------------------------------
even_rhs : Bool
홀은 함수를 점진적으로 작성하는 데 도움이 되므로 유용해요. 전체 함수를 한 번에 작성하기보다는 일부를 쓰지 않고 남겨 두고 Idris가 정의를 완성하기 위해 무엇이 필요한지 알려주게 할 수 있어요.
의존 타입 (Dependent Types)
일급 타입 (First Class Types)
Idris에서 타입은 일급(first class)이에요. 즉 다른 언어 구성물처럼 계산되고 조작되며(그리고 함수에 전달될 수 있으며) 타입이 다른 어떤 것과 마찬가지로 취급될 수 있다는 뜻이에요. 예를 들어 타입을 계산하는 함수를 작성할 수 있어요:
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
이 함수는 타입이 singleton이어야 하는지 아닌지를 나타내는 Bool에서 적절한 타입을 계산해요. 이 함수를 사용해 타입이 사용될 수 있는 어디에서든 타입을 계산할 수 있어요. 예를 들어 반환 타입을 계산하는 데 사용될 수 있어요:
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
또는 다양한 입력 타입을 갖는 데 사용될 수 있어요. 다음 함수는 singleton 플래그가 참인지에 따라, 자연수 리스트의 합을 계산하거나 주어진 Nat을 반환해요:
sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs
벡터 (Vectors)
의존 데이터 타입의 표준 예는 "길이를 가진 리스트" 타입으로, 의존 타입 문헌에서는 관례적으로 벡터(vectors)라고 불러요. 그것들은 Data.Vect를 import해 Idris 라이브러리의 일부로 사용할 수 있고, 다음과 같이 선언할 수도 있어요:
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
List와 같은 생성자 이름을 사용했음을 유의하세요. 이와 같은 임시(ad-hoc) 이름 오버로딩은, 이름들이 다른 네임스페이스(실제로는 보통 다른 모듈)에 선언되어 있다면, Idris가 받아들여요. 모호한 생성자 이름은 보통 컨텍스트에서 해결될 수 있어요.
이것은 타입들의 계열(family)을 선언하므로, 선언의 형태는 위의 단순 타입 선언과는 상당히 달라요. 우리는 타입 생성자 Vect의 타입을 명시적으로 진술해요 — 그것은 인자로 Nat과 타입을 취하며, 여기서 Type은 타입들의 타입을 나타내요. 우리는 Vect가 Nat에 대해 인덱싱되고 Type에 대해 매개변수화된다고 말해요. 각 생성자는 타입 계열의 다른 부분을 목표로 해요. Nil은 길이 0인 벡터를 만드는 데만 사용될 수 있고, ::는 길이가 0이 아닌 벡터를 만드는 데 사용돼요. ::의 타입에서 우리는 타입 a의 원소와 타입 Vect k a(즉 길이 k의 벡터)의 꼬리가 길이 S k의 벡터를 만들기 위해 결합한다고 명시적으로 진술해요.
우리는 패턴 매칭으로 Vect 같은 의존 타입에 대한 함수를, 위의 List·Nat 같은 단순 타입과 같은 방식으로 정의할 수 있어요. Vect에 대한 함수의 타입은 관련된 벡터들의 길이에 무슨 일이 일어나는지 기술해요. 예를 들어 다음과 같이 정의된 ++는 두 Vect를 이어붙여요:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ ys
(++)의 타입은 결과 벡터의 길이가 입력 길이들의 합일 것임을 진술해요. 만약 이 성질이 성립하지 않도록 정의를 잘못 작성한다면 Idris는 그 정의를 받아들이지 않아요. 예를 들어:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
이것을 Idris 타입 검사기에 통과시키면 다음이 발생해요:
$ idris VBroken.idr --check
VBroken.idr:9:23-25:
When checking right hand side of Vect.++ with expected type
Vect (S k + m) a
When checking an application of constructor Vect.:::
Type mismatch between
Vect (k + k) a (Type of xs ++ xs)
and
Vect (plus k m) a (Expected type)
Specifically:
Type mismatch between
plus k k
and
plus k m
이 오류 메시지는 두 벡터 사이에 길이 불일치가 있음을 시사해요 — 길이 k + m의 벡터가 필요했지만 길이 k + k의 벡터를 제공했어요.
유한 집합 (The Finite Sets)
이름이 암시하듯 유한 집합은 유한한 수의 원소를 가진 집합이에요. 그것들은 Data.Fin을 import해 Idris 라이브러리의 일부로 사용할 수 있고, 다음과 같이 선언할 수도 있어요:
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
시그니처에서 이것이 Nat을 받아 타입을 만드는 타입 생성자임을 볼 수 있어요.
그래서 이것은 객체의 컨테이너인 모음이라는 의미의 집합이 아니라, "5개 원소의 집합"처럼 이름 없는 원소들의 정준(canonical) 집합이에요. 사실상, Fin 타입을 인스턴스화하는 데 사용된 인자 n에 대해 0에서 (n-1)까지의 범위에 속하는 정수들을 포착하는 타입이에요.
예를 들어 Fin 5는 0과 4 사이의 정수들의 타입으로 생각될 수 있어요.
생성자들을 더 자세히 살펴봅시다.
FZ는 S k개의 원소를 가진 유한 집합의 0번째 원소이고, FS n은 S k개의 원소를 가진 유한 집합의 n+1번째 원소예요. Fin은 집합의 원소 수를 나타내는 Nat에 대해 인덱싱돼요. 빈 집합의 원소는 구성할 수 없으므로, 어느 생성자도 Fin Z를 목표로 하지 않아요.
위에서 언급했듯, Fin 계열의 유용한 응용은 경계가 있는 자연수(bounded natural numbers)를 나타내는 것이에요. 처음 n개의 자연수는 n개의 원소를 가진 유한 집합을 형성하므로, 우리는 Fin n을 0보다 크거나 같고 n보다 작은 정수들의 집합으로 취급할 수 있어요. 예를 들어 Fin n으로 주어진 경계 인덱스로 Vect에서 원소를 찾는 다음 함수는 프렐류드에 정의돼 있어요:
index : Fin n -> Vect n a -> a
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs
이 함수는 벡터의 주어진 위치에서 값을 찾아요. 위치는 벡터의 길이(각 경우에 n)로 경계 지어져 있어 런타임 경계 검사가 필요 없어요. 타입 검사기는 위치가 벡터의 길이보다 크지 않고, 물론 0보다 작지 않다고 보장해요.
또한 여기에는 Nil에 대한 경우가 없다는 점을 유의하세요. 그 경우가 불가능하기 때문이에요. Fin Z의 원소가 없고 위치가 Fin n이므로, n은 Z일 수 없어요. 결과적으로 빈 벡터에서 원소를 찾으려는 시도는 컴파일 타임 타입 오류를 주는데, n이 Z가 되도록 강제하기 때문이에요.
묵시적 인자 (Implicit Arguments)
index의 타입을 더 자세히 살펴봅시다:
index : Fin n -> Vect n a -> a
그것은 두 인자를 취해요 — n개 원소의 유한 집합의 원소와 타입 a의 n개 원소를 가진 벡터. 하지만 명시적으로 선언되지 않은 두 이름 n과 a도 있어요. 이것들은 index의 묵시적 인자예요. index의 타입을 다음과 같이 쓸 수도 있어요:
index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
타입 선언에서 중괄호 {}로 주어지는 묵시적 인자는 index의 적용에서 주어지지 않아요; 그것들의 값은 Fin n과 Vect n a 인자의 타입에서 추론될 수 있어요. 타입 선언에서 매개변수 또는 인덱스로 나타나고 어떤 인자에도 적용되지 않는, 소문자로 시작하는 어떤 이름이든 항상 자동으로 묵시적 인자로 묶일 거예요. 묵시적 인자는 {a=value}와 {n=value}를 사용해 적용에서 여전히 명시적으로 주어질 수 있어요. 예를 들어:
index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
사실 어떤 인자든 — 묵시적이든 명시적이든 — 이름이 주어질 수 있어요. index의 타입을 다음과 같이 선언할 수 있었어요:
index : (i:Fin n) -> (xs:Vect n a) -> a
이것을 하고 싶은지는 취향의 문제예요 — 때로는 인자의 목적을 더 분명하게 만들어 함수를 문서화하는 데 도움이 될 수 있어요.
게다가 {}는 왼쪽에서 패턴 매칭에 사용될 수 있어요. 즉 {var = pat}는 묵시적 변수를 얻고 "pat"에 패턴 매칭을 시도해요. 예를 들어:
isEmpty : Vect n a -> Bool
isEmpty {n = Z} _ = True
isEmpty {n = S k} _ = False
"using" 표기법 ("using" notation)
때로는 묵시적 인자의 타입을 제공하는 것이 유용해요. 특히 의존 순서(dependency ordering)가 있거나, 묵시적 인자 자체가 의존성을 가질 때요. 예를 들어, 벡터에 대한 술어를 정의하는 다음 정의(이것은 Data.Vect에 Elem이라는 이름으로도 정의돼 있음)에서 묵시적 인자의 타입을 진술하고 싶을 수 있어요:
data IsElem : a -> Vect n a -> Type where
Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
IsElem x xs의 인스턴스는 x가 xs의 원소임을 진술해요. 요구된 원소가 벡터의 머리인 Here이거나, 벡터의 꼬리에 있는 There이면 그런 술어를 구성할 수 있어요. 예를 들어:
testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil
inVect : IsElem 5 Main.testVec
inVect = There (There Here)
중요 (Important)
묵시적 인자와 범위 (Implicit Arguments and Scope)
타입 시그니처 안에서 타입 검사기는 소문자로 시작하고 다른 것에 적용되지 않는 모든 변수를 묵시적 변수로 취급해요. 위의 코드 예제를 컴파일하려면 testVec에 대한 한정 이름을 제공해야 해요. 위 예에서 코드가 Main 모듈 안에 있다고 가정했어요.
같은 묵시적 인자가 많이 사용되면 정의를 읽기 어렵게 만들 수 있어요. 이 문제를 피하기 위해, using 블록은 블록 안에 나타날 수 있는 묵시적 인자들의 타입과 순서를 줘요:
using (x:a, y:a, xs:Vect n a)
data IsElem : a -> Vect n a -> Type where
Here : IsElem x (x :: xs)
There : IsElem x xs -> IsElem x (y :: xs)
참고: 선언 순서와 mutual 블록 (Note: Declaration Order and mutual blocks)
일반적으로 함수와 데이터 타입은 사용 전에 정의되어야 해요. 의존 타입이 함수가 타입의 일부로 나타나게 허용하고, 타입 검사가 특정 함수의 정의 방식에 의존할 수 있기 때문이에요 (비록 이것은 전체 함수에 대해서만 참이지만; Totality Checking 절 참조). 하지만 이 제한은 데이터 타입과 함수가 동시에 정의될 수 있게 하는 mutual 블록으로 완화될 수 있어요:
mutual
even : Nat -> Bool
even Z = True
even (S k) = odd k
odd : Nat -> Bool
odd Z = False
odd (S k) = even k
mutual 블록에서, 먼저 모든 타입 선언이 추가되고, 그 다음 함수 본문이 추가돼요. 결과적으로 어떤 함수 타입도 블록 안의 어떤 함수의 축소 동작에 의존할 수 없어요.
I/O
컴퓨터 프로그램은 사용자나 시스템과 어떤 식으로든 상호작용하지 않으면 거의 쓸모가 없어요. Idris 같은 순수 언어 — 즉 식이 부수 효과(side-effects)를 갖지 않는 언어 — 의 어려움은 I/O가 본질적으로 부수 효과를 갖는다는 것이에요. 따라서 Idris에서 그러한 상호작용은 타입 IO에 캡슐화돼요:
data IO a -- IO operation returning a value of type a
우리는 IO의 정의를 추상으로 남겨둘 거지만, 사실상 그것은 I/O 동작을 어떻게 실행하는지보다는 실행될 I/O 동작이 무엇인지를 기술해요. 결과 동작은 런타임 시스템에 의해 외부적으로 실행돼요. 우리는 이미 하나의 IO 프로그램을 봤어요:
main : IO ()
main = putStrLn "Hello world"
putStrLn의 타입은 그것이 문자열을 받고 I/O 동작을 통해 단위 타입 ()의 원소를 반환함을 설명해요. 새 줄 없이 문자열을 출력하는 변형 putStr이 있어요:
putStrLn : String -> IO ()
putStr : String -> IO ()
사용자 입력에서 문자열을 읽을 수도 있어요:
getLine : IO String
다른 많은 I/O 동작이 프렐류드에 정의돼 있어요. 예를 들어 파일 읽기·쓰기가 있어요:
data File -- abstract
data Mode = Read | Write | ReadWrite
openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
closeFile : File -> IO ()
fGetLine : (h : File) -> IO (Either FileError String)
fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
fEOF : File -> IO Bool
여러 개가 Either를 반환한다는 점을 유의하세요. 실패할 수 있기 때문이에요.
"do" 표기법 ("do" notation)
I/O 프로그램은 전형적으로 동작을 순서화해, 한 계산의 출력을 다음 계산의 입력에 공급해야 해요. 하지만 IO는 추상 타입이므로 계산의 결과에 직접 접근할 수 없어요. 대신 do 표기법으로 동작을 순서화해요:
greet : IO ()
greet = do putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ name)
문법 x <- iovalue는 타입 IO a의 I/O 동작 iovalue를 실행하고, 타입 a의 결과를 변수 x에 넣어요. 이 경우 getLine은 IO String을 반환하므로, name은 타입 String을 가져요. 들여쓰기가 중요해요 — do 블록의 각 문은 같은 열에서 시작해야 해요. pure 연산은 값을 IO 동작에 직접 주입할 수 있게 해줘요:
pure : a -> IO a
나중에 보게 되겠지만, do 표기법은 이것보다 더 일반적이며 오버로드될 수 있어요.
느슨함 (Laziness)
보통 함수의 인자는 함수 자체보다 먼저 평가돼요 (즉, Idris는 조급 평가(eager evaluation)를 사용해요). 하지만 이것이 항상 최선의 접근은 아니에요. 다음 함수를 고려해보세요:
ifThenElse : Bool -> a -> a -> a
ifThenElse True t e = t
ifThenElse False t e = e
이 함수는 t 또는 e 인자 중 하나를 사용하지만 둘 다는 아니에요 (사실 이것은 나중에 보게 될 if...then...else 구성물을 구현하는 데 사용돼요). 우리는 사용된 인자만 평가되는 것을 선호할 거예요. 이를 위해 Idris는 평가를 정지(suspend)시킬 수 있는 Lazy 데이터 타입을 제공해요:
data Lazy : Type -> Type where
Delay : (val : a) -> Lazy a
Force : Lazy a -> a
타입 Lazy a의 값은 Force에 의해 강제될 때까지 평가되지 않아요. Idris 타입 검사기는 Lazy 타입을 알고 있으며, 필요할 때 Lazy a와 a 사이에, 그리고 그 반대 방향으로 변환을 삽입해요. 따라서 Force나 Delay를 명시적으로 사용하지 않고 ifThenElse를 다음과 같이 쓸 수 있어요:
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e
코데이터 타입 (Codata Types)
코데이터 타입은 재귀 인자를 잠재적으로 무한하다고 표시함으로써 무한 데이터 구조를 정의할 수 있게 해줘요. 코데이터 타입 T에 대해, 타입 T의 각 생성자 인자는 Inf T 타입의 인자로 변환돼요. 이것은 각 T 인자를 느슨하게 만들고, 타입 T의 무한 데이터 구조가 만들어질 수 있게 해줘요. 코데이터 타입의 한 예는 Stream이며, 다음과 같이 정의돼요.
codata Stream : Type -> Type where
(::) : (e : a) -> Stream a -> Stream a
이것은 컴파일러에 의해 다음으로 번역돼요.
data Stream : Type -> Type where
(::) : (e : a) -> Inf (Stream a) -> Stream a
다음은 코데이터 타입 Stream이 무한 데이터 구조를 형성하는 데 어떻게 사용될 수 있는지의 예시예요. 이 경우 우리는 무한한 1들의 스트림을 만들고 있어요.
ones : Stream Nat
ones = 1 :: ones
코데이터는 무한한 상호 재귀 데이터 구조의 생성을 허용하지 않는다는 점을 유의하는 것이 중요해요. 예를 들어 다음은 무한 루프를 만들어 스택 오버플로를 일으킬 거예요.
mutual
codata Blue a = B a (Red a)
codata Red a = R a (Blue a)
mutual
blue : Blue Nat
blue = B 1 red
red : Red Nat
red = R 1 blue
mutual
findB : (a -> Bool) -> Blue a -> a
findB f (B x r) = if f x then x else findR f r
findR : (a -> Bool) -> Red a -> a
findR f (R x b) = if f x then x else findB f b
main : IO ()
main = do printLn $ findB (== 1) blue
이것을 고치려면 생성자 매개변수 타입에 명시적 Inf 선언을 추가해야 해요. 코데이터가 정의되는 타입과 다른 타입의 생성자 매개변수에는 그것을 추가하지 않기 때문이에요. 예를 들어 다음은 1을 출력해요.
mutual
data Blue : Type -> Type where
B : a -> Inf (Red a) -> Blue a
data Red : Type -> Type where
R : a -> Inf (Blue a) -> Red a
mutual
blue : Blue Nat
blue = B 1 red
red : Red Nat
red = R 1 blue
mutual
findB : (a -> Bool) -> Blue a -> a
findB f (B x r) = if f x then x else findR f r
findR : (a -> Bool) -> Red a -> a
findR f (R x b) = if f x then x else findB f b
main : IO ()
main = do printLn $ findB (== 1) blue
유용한 데이터 타입 (Useful Data Types)
Idris는 여러 유용한 데이터 타입과 라이브러리 함수를 포함해요 (배포판의 libs/ 디렉터리와 문서를 보세요). 이 절은 그중 일부를 기술해요. 여기서 기술하는 함수들은 Prelude.idr의 일부로 모든 Idris 프로그램에 자동으로 import돼요.
List와 Vect (List and Vect)
우리는 이미 List와 Vect 데이터 타입을 봤어요:
data List a = Nil | (::) a (List a)
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
생성자 이름이 각각에 대해 같다는 점을 유의하세요 — 생성자 이름(사실 일반적인 이름)은 다른 네임스페이스에 선언되어 있다면(M odules and Namespaces 절 참조) 오버로드될 수 있고, 전형적으로 그 타입에 따라 해결돼요. 문법적 설탕으로서, 생성자 이름 Nil과 ::을 가진 어떤 타입이든 리스트 형식으로 쓸 수 있어요. 예를 들어:
-
[]는Nil을 의미함 -
[1,2,3]은1 :: 2 :: 3 :: Nil을 의미함
라이브러리는 또한 이 타입들을 조작하는 여러 함수를 정의해요. map은 List와 Vect 모두에 대해 오버로드되며, 함수를 리스트나 벡터의 모든 원소에 적용해요.
map : (a -> b) -> List a -> List b
map f [] = []
map f (x :: xs) = f x :: map f xs
map : (a -> b) -> Vect n a -> Vect n b
map f [] = []
map f (x :: xs) = f x :: map f xs
예를 들어 다음 정수 벡터와 정수를 두 배로 하는 함수가 주어졌을 때:
intVec : Vect 5 Int
intVec = [1, 2, 3, 4, 5]
double : Int -> Int
double x = x * 2
map 함수는 벡터의 모든 원소를 두 배로 하는 데 다음과 같이 사용될 수 있어요:
*UsefulTypes> show (map double intVec)
"[2, 4, 6, 8, 10]" : String
List와 Vect에서 사용 가능한 함수들에 대한 더 많은 세부 사항은 라이브러리 파일에서 보세요:
-
libs/prelude/Prelude/List.idr -
libs/base/Data/List.idr -
libs/base/Data/Vect.idr -
libs/base/Data/VectType.idr
함수에는 필터링, 이어붙이기, 뒤집기 등이 포함돼요.
곁가지: 익명 함수와 연산자 섹션 (Aside: Anonymous functions and operator sections)
위의 식을 쓰는 더 깔끔한 방법이 실제로 있어요. 한 가지 방법은 익명 함수를 사용하는 것이에요:
*UsefulTypes> show (map (\x => x * 2) intVec)
"[2, 4, 6, 8, 10]" : String
표기법 \x => val은 하나의 인자 x를 받고 식 val을 반환하는 익명 함수를 만드는 것이에요. 익명 함수는 쉼표로 구분되어 여러 인자를 취할 수 있어요. 예: \x, y, z => val. 인자에 명시적 타입을 줄 수도 있어요. 예: \x : Int => x * 2, 그리고 패턴 매칭도 할 수 있어요. 예: \(x, y) => x + y. 연산자 섹션(operator section)을 사용할 수도 있어요:
*UsefulTypes> show (map (* 2) intVec)
"[2, 4, 6, 8, 10]" : String
(*2)는 숫자에 2를 곱하는 함수의 약식이에요. 그것은 \x => x * 2로 펼쳐져요. 비슷하게 (2*)는 \x => 2 * x로 펼쳐질 거예요.
Maybe
Maybe는 선택적 값(optional value)을 기술해요. 주어진 타입의 값이 있거나 없거나 둘 중 하나예요:
data Maybe a = Just a | Nothing
Maybe는 실패할 수 있는 연산에 타입을 주는 한 가지 방법이에요. 예를 들어 (벡터가 아닌) 리스트에서 무언가를 찾는 것은 경계를 벗어난(out of bounds) 오류를 초래할 수 있어요:
list_lookup : Nat -> List a -> Maybe a
list_lookup _ Nil = Nothing
list_lookup Z (x :: xs) = Just x
list_lookup (S k) (x :: xs) = list_lookup k xs
maybe 함수는 값이 있으면 함수를 적용하거나, 없으면 기본 값을 제공함으로써 Maybe 타입의 값을 처리하는 데 사용돼요:
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
처음 두 인자의 타입이 Lazy로 감싸져 있다는 점을 유의하세요. 두 인자 중 하나만 실제로 사용되므로, 그것들이 계산하고 나서 버리면 낭비일 큰 식일 수 있는 경우를 대비해 Lazy로 표시해요.
튜플 (Tuples)
값은 다음 내장 데이터 타입으로 쌍을 이룰 수 있어요:
data Pair a b = MkPair a b
문법적 설탕으로서 (a, b)를 쓸 수 있으며, 이는 컨텍스트에 따라 Pair a b 또는 MkPair a b를 의미해요. 튜플은 임의의 수의 값을 포함할 수 있으며, 중첩된 쌍으로 표현돼요:
fred : (String, Int)
fred = ("Fred", 42)
jim : (String, Int, String)
jim = ("Jim", 25, "Cambridge")
*UsefulTypes> fst jim
"Jim" : String
*UsefulTypes> snd jim
(25, "Cambridge") : (Int, String)
*UsefulTypes> jim == ("Jim", (25, "Cambridge"))
True : Bool
의존 쌍 (Dependent Pairs)
의존 쌍은 쌍의 두 번째 원소의 타입이 첫 번째 원소의 값에 의존할 수 있게 해줘요:
data DPair : (a : Type) -> (P : a -> Type) -> Type where
MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P
다시 이것에 대한 문법적 설탕이 있어요. (a : A ** P)는 A와 P의 쌍의 타입이며, 이름 a가 P 안에 나타날 수 있어요. ( a ** p )는 이 타입의 값을 구성해요. 예를 들어 숫자를 특정 길이의 Vect와 쌍으로 만들 수 있어요:
vec : (n : Nat ** Vect n Int)
vec = (2 ** [3, 4])
원한다면 길게 적을 수도 있는데, 둘은 정확히 동등해요:
vec : DPair Nat (\n => Vect n Int)
vec = MkDPair 2 [3, 4]
물론 타입 검사기는 벡터의 길이에서 첫 원소의 값을 추론할 수 있어요. 타입 검사기가 채우기를 기대하는 값 대신 밑줄 _을 쓸 수 있으므로, 위의 정의는 다음과 같이도 쓸 수 있어요:
vec : (n : Nat ** Vect n Int)
vec = (_ ** [3, 4])
또 다시 추론될 수 있으므로 쌍의 첫 원소의 타입을 생략하는 것을 선호할 수도 있어요:
vec : (n ** Vect n Int)
vec = (_ ** [3, 4])
의존 쌍의 한 용도는 인덱스가 미리 알려지지 않은 의존 타입의 값을 반환하는 것이에요. 예를 들어 어떤 술어에 따라 Vect에서 원소를 필터링하면, 결과 벡터의 길이가 미리 무엇인지 알 수 없어요:
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
Vect가 비어 있으면 결과는 쉽지만:
filter p Nil = (_ ** [])
:: 경우에는, filter에 대한 재귀 호출의 결과를 검사해 길이와 벡터를 결과에서 추출해야 해요. 이를 위해 중간 값에 패턴 매칭을 허용하는 with 표기법을 사용해요:
filter p (x :: xs) with (filter p xs)
| ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
with 표기법에 대해서는 나중에 더 볼 거예요.
의존 쌍은 때때로 "시그마 타입(Sigma types)"이라고 불려요.
레코드 (Records)
레코드는 여러 값(레코드의 필드)을 함께 모으는 데이터 타입이에요. Idris는 레코드 정의와 필드 접근·갱신 함수의 자동 생성을 위한 문법을 제공해요. 데이터 구조에 사용되는 문법과 달리, Idris의 레코드는 Haskell에서 보이는 것과 다른 문법을 따라요. 예를 들어 사람의 이름과 나이를 레코드로 나타낼 수 있어요:
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30
생성자 이름은 constructor 키워드로 제공되고, 필드는 where 키워드 뒤의 들여쓰기된 블록에 주어져요 (여기서 firstName, middleName, lastName, age). 한 줄에 여러 필드를 선언할 수 있어요 — 같은 타입을 갖는다면요. 필드 이름은 필드 값에 접근하는 데 사용될 수 있어요:
*Record> firstName fred
"Fred" : String
*Record> age fred
30 : Int
*Record> :t firstName
firstName : Person -> String
필드 이름을 사용해 레코드를 갱신할 수도 있어요 (더 정확히는, 주어진 필드가 갱신된 레코드의 사본을 만든다는 뜻):
*Record> record { firstName = "Jim" } fred
MkPerson "Jim" "Joe" "Bloggs" 30 : Person
*Record> record { firstName = "Jim", age $= (+ 1) } fred
MkPerson "Jim" "Joe" "Bloggs" 31 : Person
문법 record { field = val, ... }은 레코드의 주어진 필드를 갱신하는 함수를 생성해요. =는 필드에 새 값을 할당하고, $=는 함수를 적용해 그 값을 갱신해요.
각 레코드는 자신의 네임스페이스에 정의되며, 이는 필드 이름이 여러 레코드에서 재사용될 수 있다는 뜻이에요.
레코드와 레코드 안의 필드는 의존 타입을 가질 수 있어요. 갱신은 결과가 잘 타입되기만 하면 필드의 타입을 바꾸는 것이 허용돼요.
record Class where
constructor ClassInfo
students : Vect n Person
className : String
필드의 타입에 영향을 주지 않으므로 students 필드를 다른 길이의 벡터로 갱신하는 것은 안전해요:
addStudent : Person -> Class -> Class
addStudent p c = record { students = p :: students c } c
*Record> addStudent fred (ClassInfo [] "CS")
ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
$=를 사용해 addStudent를 더 간결하게 정의할 수도 있어요:
addStudent' : Person -> Class -> Class
addStudent' p c = record { students $= (p ::) } c
중첩 레코드 갱신 (Nested record update)
Idris는 중첩 레코드에 접근하고 갱신하기 위한 편리한 문법도 제공해요. 예를 들어 식 c (b (a x))로 필드에 접근할 수 있다면, 다음 문법으로 갱신할 수 있어요:
record { a->b->c = val } x
이것은 경로 a->b->c로 접근되는 필드가 val로 설정된 새 레코드를 반환해요. 이 문법은 일급(first class)이에요. 즉 record { a->b->c = val } 자체가 함수 타입을 가져요. 대칭적으로, 필드는 다음 문법으로 접근될 수도 있어요:
record { a->b->c } x
$= 표기법도 중첩 레코드 갱신에 유효해요.
의존 레코드 (Dependent Records)
레코드는 값에 의존할 수도 있어요. 레코드에는 다른 필드처럼 갱신될 수 없는 매개변수가 있어요. 매개변수는 결과 타입의 인자로 나타나며, 레코드 타입 이름 뒤에 쓰여져요. 예를 들어 쌍 타입은 다음과 같이 정의될 수 있어요:
record Prod a b where
constructor Times
fst : a
snd : b
앞서의 Class 레코드를 사용해, Vect로 클래스의 크기를 제한하고 크기를 레코드에 매개변수화해 타입에 포함시킬 수 있어요. 예를 들어:
record SizedClass (size : Nat) where
constructor SizedClassInfo
students : Vect size Person
className : String
이제 앞서의 addStudent 함수를 더 이상 사용할 수 없다는 점을 유의하세요 — 그것이 클래스의 크기를 바꾸기 때문이에요. 학생을 추가하는 함수는 이제 타입에서 클래스의 크기가 1만큼 증가했음을 명시해야 해요. 크기가 자연수로 지정되므로, 새 값은 S 생성자로 증가될 수 있어요:
addStudent : Person -> SizedClass n -> SizedClass (S n)
addStudent p c = SizedClassInfo (p :: students c) (className c)
더 많은 식 (More Expressions)
let 바인딩 (let bindings)
중간 값은 let 바인딩으로 계산될 수 있어요:
mirror : List a -> List a
mirror xs = let xs' = reverse xs in
xs ++ xs'
let 바인딩에서 간단한 패턴 매칭도 할 수 있어요. 예를 들어 최상위에서 패턴 매칭하는 것뿐 아니라, 레코드에서 다음과 같이 필드를 추출할 수 있어요:
data Person = MkPerson String Int
showPerson : Person -> String
showPerson p = let MkPerson name age = p in
name ++ " is " ++ show age ++ " years old"
리스트 내포 (List comprehensions)
Idris는 리스트를 만드는 편리한 약식으로 내포 표기법(comprehension notation)을 제공해요. 일반적인 형태는:
[ expression | qualifiers ]
이것은 쉼표로 구분된 한정자(qualifiers)가 주는 조건에 따라 식을 평가해 만들어지는 값들의 리스트를 생성해요. 예를 들어 피타고라스 삼중쌍의 리스트를 다음과 같이 만들 수 있어요:
pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
x*x + y*y == z*z ]
[a..b] 표기법은 a와 b 사이의 수들의 리스트를 만드는 또 다른 약식이에요. 대안으로 [a,b..c]는 a와 c 사이의 수들의 리스트를 a와 b의 차이로 지정된 증가분으로 만들어요. 이것은 프렐류드의 enumFromTo와 enumFromThenTo 함수를 사용해 타입 Nat, Int, Integer에 대해 작동해요.
case 식 (case expressions)
단순 타입의 중간 값을 검사하는 또 다른 방법은 case 식을 사용하는 것이에요. 예를 들어 다음 함수는 주어진 문자에서 문자열을 둘로 나눠요:
splitAt : Char -> String -> (String, String)
splitAt c x = case break (== c) x of
(x, y) => (x, strTail y)
break는 주어진 함수가 참을 반환하는 지점에서 문자열을 문자열 쌍으로 나누는 라이브러리 함수예요. 그런 다음 반환된 쌍을 분해하고, 두 번째 문자열의 첫 문자를 제거해요.
case 식은 여러 경우에 매치할 수 있어요. 예를 들어 타입 Maybe a의 중간 값을 검사하려면요. 리스트에서 인덱스를 찾아, 인덱스가 경계를 벗어나면 Nothing을 반환하는 list_lookup을 떠올려보세요. 이것을 사용해, 인덱스를 찾고 인덱스가 경계를 벗어나면 기본 값을 반환하는 lookup_default를 작성할 수 있어요:
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
Nothing => def
Just x => x
인덱스가 경계 안에 있으면 그 인덱스의 값을 얻고, 그렇지 않으면 기본 값을 얻어요:
*UsefulTypes> lookup_default 2 [3,4,5,6] (-1)
5 : Integer
*UsefulTypes> lookup_default 4 [3,4,5,6] (-1)
-1 : Integer
제한: case 구성물은 보조 함수를 작성할 필요를 피하기 위한 중간 식의 단순 분석을 위한 것이며, 패턴 매칭 let과 lambda 바인딩을 구현하기 위해 내부적으로도 사용돼요. 그것은 다음의 경우에만 작동해요:
-
각 분기가 같은 타입의 값에 매치하고, 같은 타입의 값을 반환함.
-
결과의 타입이 "알려져" 있음. 즉 case-식 자체를 타입 검사하지 않고도 식의 타입이 결정될 수 있음.
전체성 (Totality)
Idris는 전체 함수와 부분 함수를 구분해요.
전체 함수(total function)는 다음 중 하나인 함수예요:
-
모든 가능한 입력에 대해 종료함, 또는
-
어쩌면 무한한 결과의 비어 있지 않은 유한 접두사를 만들어냄
함수가 전체적이면, 우리는 그 타입을 그 함수가 무엇을 할지의 정밀한 기술로 간주할 수 있어요. 예를 들어 반환 타입 String을 가진 함수가 있다면, 그것이 전체적인지 아닌지에 따라 다른 것을 알게 돼요:
-
전체적이라면, 유한한 시간 안에 타입
String의 값을 반환할 것임; -
부분적이라면, 충돌하거나 무한 루프에 들어가지 않는 한
String을 반환할 것임.
Idris는 이 구분을 해서, 타입 검사 중에 어떤 함수를 평가해도 안전한지 알게 돼요 (First Class Types에서 본 것처럼). 결국 타입 검사 중에 종료하지 않는 함수를 평가하려 하면 타입 검사도 종료하지 않을 거예요!
따라서 타입 검사 중에는 전체 함수만 평가될 거예요. 부분 함수는 타입에서 여전히 사용될 수 있지만, 더 이상 평가되지 않을 거예요.