인터페이스
인터페이스 (Interfaces)
우리는 종종 여러 다른 데이터 타입에 걸쳐 작동하는 함수를 정의하고 싶어해요. 예를 들어 산술 연산자가 최소한 Int, Integer, Double에서 작동하기를 원해요. ==가 대부분의 데이터 타입에서 작동하기를 원해요. 다른 타입들을 균일한 방식으로 표시할 수 있기를 원해요.
이를 위해 인터페이스(interfaces)를 사용해요. 이는 Haskell의 타입 클래스 또는 Rust의 트레이트(traits)와 유사해요. 인터페이스를 정의하려면 오버로드 가능한 함수들의 모음을 제공해요. 간단한 예는 프렐류드에 정의되어 있고 값을 String으로 변환하는 인터페이스를 제공하는 Show 인터페이스예요:
interface Show a where
show : a -> String
이것은 다음 타입의 함수를 생성해요 (이것을 Show 인터페이스의 메서드(method)라고 불러요):
show : Show a => a -> String
이것은 "a가 Show의 구현을 가진다는 제약 아래, 입력 a를 받아 String을 반환한다"로 읽을 수 있어요. 인터페이스의 구현은 인터페이스의 메서드 정의를 제공함으로써 정의돼요. 예를 들어 Nat에 대한 Show 구현은 다음과 같이 정의될 수 있어요:
Show Nat where
show Z = "Z"
show (S k) = "s" ++ show k
Idris> show (S (S (S Z)))
"sssZ" : String
타입에 대해 이름 없는(unnamed) 구현은 하나만 주어질 수 있으며, 구현들은 겹칠 수 없어요. 하지만 아래의 Named Implementations를 참조하세요.
구현 선언 자체가 제약을 가질 수 있어요.
해결(resolution)을 돕기 위해, 구현의 인자는 생성자(데이터 생성자나 타입 생성자) 또는 변수여야 해요 (즉, 함수에 대한 구현을 줄 수 없어요). 예를 들어 벡터에 대한 Show 구현을 정의하려면, 각 원소를 String으로 변환할 때 사용할 것이므로 원소 타입에 대한 Show 구현이 있다는 것을 알아야 해요:
Show a => Show (Vect n a) where
show xs = "[" ++ show' xs ++ "]" where
show' : Vect n a -> String
show' Nil = ""
show' (x :: Nil) = show x
show' (x :: xs) = show x ++ ", " ++ show' xs
출처: 문서
본문
기본 정의 (Default Definitions)
라이브러리는 값의 동등성 또는 부등성을 비교하는 메서드를 제공하고 모든 내장 타입에 대한 구현을 가진 Eq 인터페이스를 정의해요:
interface Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
타입에 대한 구현을 선언하려면 모든 메서드의 정의를 줘야 해요. 예를 들어 Nat에 대한 Eq 구현:
Eq Nat where
Z == Z = True
(S x) == (S y) = x == y
Z == (S y) = False
(S x) == Z = False
x /= y = not (x == y)
/= 메서드가 == 메서드를 적용한 결과의 부정이 아닌 경우를 많이 상상하기는 어려워요. 따라서 인터페이스 선언에서 각 메서드에 대해, 다른 메서드로 표현한 기본 정의를 주는 것이 편리해요:
interface Eq a where
(==) : a -> a -> Bool
(/=) : a -> a -> Bool
x /= y = not (x == y)
x == y = not (x /= y)
Eq의 최소 완전 구현은 == 또는 /= 중 하나를 정의를 요구하지만, 둘 다를 요구하지는 않아요. 메서드 정의가 빠져 있고 그것에 대한 기본 정의가 있다면, 기본이 대신 사용돼요.
인터페이스 확장 (Extending Interfaces)
인터페이스는 확장될 수도 있어요. 동등 관계 Eq로부터의 논리적 다음 단계는 순서 관계 Ord를 정의하는 것이에요. Eq의 메서드를 상속하면서 자신만의 것도 정의하는 Ord 인터페이스를 정의할 수 있어요:
data Ordering = LT | EQ | GT
interface Eq a => Ord a where
compare : a -> a -> Ordering
(<) : a -> a -> Bool
(>) : a -> a -> Bool
(<=) : a -> a -> Bool
(>=) : a -> a -> Bool
max : a -> a -> a
min : a -> a -> a
Ord 인터페이스는 두 값을 비교하고 그 순서를 결정할 수 있게 해줘요. compare 메서드만 요구되며, 다른 모든 메서드는 기본 정의를 가져요. 이것을 사용해 리스트를 증가하는 순서로 정렬하는 함수 sort를 — 리스트의 원소 타입이 Ord 인터페이스에 있다면 — 작성할 수 있어요. 제약은 뚱뚱한 화살표 =>의 왼쪽에, 함수 타입은 뚱뚱한 화살표의 오른쪽에 둬요:
sort : Ord a => List a -> List a
함수, 인터페이스, 구현은 여러 제약을 가질 수 있어요. 여러 제약은 쉼표로 구분된 목록으로 원괄호(괄호) 안에 작성돼요. 예를 들어:
sortAndShow : (Ord a, Show a) => List a -> String
sortAndShow xs = show (sort xs)
참고: 인터페이스와 mutual 블록 (Note: Interfaces and mutual blocks)
Idris는 mutual 블록을 제외하고 엄격히 "사용 전 정의(define before use)"예요. mutual 블록에서 Idris는 두 단계로 정교화(elaborates)해요: 첫 단계에서 타입, 두 번째 단계에서 정의. mutual 블록이 인터페이스 선언을 포함하면, 첫 단계에서 인터페이스 헤더를 정교화하지만 메서드 타입은 정교화하지 않고, 두 번째 단계에서 메서드 타입과 기본 정의를 정교화해요.
펑터와 어플라이커티브 (Functors and Applicatives)
지금까지 우리는 매개변수가 타입 Type인 단일 매개변수 인터페이스를 봤어요. 일반적으로는 임의의 수(심지어 0)의 매개변수가 있을 수 있고, 매개변수는 어떤 타입이든 가질 수 있어요. 매개변수의 타입이 Type이 아니라면 명시적 타입 선언을 줘야 해요. 예를 들어 Functor 인터페이스는 프렐류드에 정의돼 있어요:
interface Functor (f : Type -> Type) where
map : (m : a -> b) -> f a -> f b
펑터는 구조에 걸쳐 함수가 적용되게 해줘요. 예를 들어 List의 모든 원소에 함수를 적용하려면:
Functor List where
map f [] = []
map f (x::xs) = f x :: map f xs
Idris> map (*2) [1..10]
[2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
Functor를 정의한 후, 함수 적용의 개념을 추상화하는 Applicative를 정의할 수 있어요:
infixl 2 <*>
interface Functor f => Applicative (f : Type -> Type) where
pure : a -> f a
(<*>) : f (a -> b) -> f a -> f b
모나드와 do-표기법 (Monads and do-notation)
Monad 인터페이스는 바인딩과 계산을 캡슐화할 수 있게 해주며, "do" 표기법 절에서 소개된 do-표기법의 기초예요. 그것은 위에서 정의한 Applicative를 확장하며, 다음과 같이 정의돼요:
interface Applicative m => Monad (m : Type -> Type) where
(>>=) : m a -> (a -> m b) -> m b
do 블록 안에서는 다음 문법 변환이 적용돼요:
-
x <- v; e는v >>= (\x => e)가 됨 -
v; e는v >>= (\_ => e)가 됨 -
let x = v; e는let x = v in e가 됨
IO는 프리미티브 함수로 정의된 Monad 구현을 가져요. Maybe에 대한 구현도 다음과 같이 정의할 수 있어요:
Monad Maybe where
Nothing >>= k = Nothing
(Just x) >>= k = k x
이것을 사용해, 오류 처리를 캡슐화하도록 모나드를 사용해 두 Maybe Int를 더하는 함수를 정의할 수 있어요:
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = do x' <- x -- Extract value from x
y' <- y -- Extract value from y
pure (x' + y') -- Add them
이 함수는 x와 y가 모두 사용 가능하면 그 값들을 추출하고, 하나 또는 둘 다 아니면 Nothing을 반환해요("fail fast"). Nothing 경우를 관리하는 것은 do 표기법에 숨겨진 >>= 연산자에 의해 이루어져요.
*Interfaces> m_add (Just 20) (Just 22)
Just 42 : Maybe Int
*Interfaces> m_add (Just 20) Nothing
Nothing : Maybe Int
패턴 매칭 바인드 (Pattern Matching Bind)
때로는 do 표기법에서 함수의 결과에 즉시 패턴 매칭하고 싶을 때가 있어요. 예를 들어 콘솔에서 숫자를 읽고, 숫자가 유효하면 형태 Just x의 값을 반환하고 그렇지 않으면 Nothing을 반환하는 함수 readNumber가 있다고 해봅시다:
readNumber : IO (Maybe Nat)
readNumber = do
input <- getLine
if all isDigit (unpack input)
then pure (Just (cast input))
else pure Nothing
그것을 사용해 두 숫자를 읽고, 둘 다 유효하지 않으면 Nothing을 반환하는 함수를 작성한다면, readNumber의 결과에 패턴 매칭하고 싶을 거예요:
readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
do x <- readNumber
case x of
Nothing => pure Nothing
Just x_ok => do y <- readNumber
case y of
Nothing => pure Nothing
Just y_ok => pure (Just (x_ok, y_ok))
오류 처리가 많으면 이것은 매우 빨리 깊게 중첩될 수 있어요!
그래서 대신 바인드와 패턴 매칭을 한 줄에 결합할 수 있어요. 예를 들어 형태 Just x_ok의 값에 패턴 매칭을 시도할 수 있어요:
readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
do Just x_ok <- readNumber
Just y_ok <- readNumber
pure (Just (x_ok, y_ok))
하지만 여전히 문제가 있어요. 이제 Nothing에 대한 경우를 생략했기 때문에 readNumbers는 더 이상 전체적(total)이 아니에요! 다음과 같이 Nothing 경우를 다시 추가할 수 있어요:
readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
do Just x_ok <- readNumber | Nothing => pure Nothing
Just y_ok <- readNumber | Nothing => pure Nothing
pure (Just (x_ok, y_ok))
이 readNumbers 버전의 효과는 첫 번째 버전과 동일해요 (사실 그것의 문법적 설탕이며 직접 그 형태로 다시 번역돼요). 각 문의 첫 부분(Just x_ok <-와 Just y_ok <-)은 선호 바인딩(preferred binding)을 줘요 — 여기에 매치되면 do 블록의 나머지로 실행이 계속돼요. 두 번째 부분은 대안 바인딩들을 주며, 이는 둘 이상일 수 있어요.
!-표기법 (!-notation)
많은 경우, do-표기법을 사용하면 프로그램이 불필요하게 장황해질 수 있어요. 특히 위의 m_add처럼 바인딩된 값이 한 번 즉시 사용되는 경우가 그래요. 이런 경우 다음과 같은 약식 버전을 사용할 수 있어요:
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = pure (!x + !y)
표기법 !expr은 식 expr이 평가된 다음 묵시적으로 바인딩되어야 함을 의미해요. 개념적으로 !를 다음 타입을 가진 접두사 함수로 생각할 수 있어요:
(!) : m a -> a
하지만 그것은 진짜 함수가 아니라 단지 문법이라는 점을 유의하세요! 실제로 부분식 !expr은 가능한 한 현재 범위 안에서 expr을 높이(lift)고, 그것을 새 이름 x에 바인딩하며, !expr을 x로 대체해요. 식은 깊이 우선(depth first), 왼쪽에서 오른쪽으로 높여져요. 실제로 !-표기법은 어떤 식이 모나딕인지에 대한 표기적 단서를 여전히 주면서, 더 직접적인 스타일로 프로그래밍할 수 있게 해줘요.
예를 들어 식:
let y = 42 in f !(g !(print y) !x)
는 다음으로 높여져요:
let y = 42 in do y' <- print y
x' <- x
g' <- g y' x'
f g'
모나드 내포 (Monad comprehensions)
More Expressions 절에서 본 리스트 내포 표기법은 더 일반적이며, Monad와 Alternative 모두의 구현을 가진 무엇이든 적용돼요:
interface Applicative f => Alternative (f : Type -> Type) where
empty : f a
(<|>) : f a -> f a -> f a
일반적으로 내포는 형태 [ exp | qual1, qual2, …, qualn ]을 취하며, quali는 다음 중 하나일 수 있어요:
-
생성자(generator)
x <- e -
타입
Bool의 식인 가드(guard) -
let 바인딩
let x = e
내포 [exp | qual1, qual2, …, qualn]을 번역하려면, 먼저 가드인 어떤 한정자 qual이라도 다음 함수를 사용해 guard qual로 번역돼요:
guard : Alternative f => Bool -> f ()
그 다음 내포가 do 표기법으로 변환돼요:
do { qual1; qual2; ...; qualn; pure exp; }
모나드 내포를 사용하면 m_add에 대한 대안 정의는 다음과 같을 거예요:
m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = [ x' + y' | x' <- x, y' <- y ]
Idiom 괄호 (Idiom brackets)
do 표기법이 순서화(sequencing)에 대안적 의미를 주는 반면, idiom은 적용(application)에 대안적 의미를 줘요. 이 절의 표기법과 더 큰 예제는 Conor McBride와 Ross Paterson의 논문 "Applicative Programming with Effects" [1]에서 영감을 받았어요.
먼저 위의 m_add를 다시 살펴봅시다. 그것이 정말 하고 있는 것은 Maybe Int에서 추출한 두 값에 연산자를 적용하는 것뿐이에요. 적용을 추상화할 수 있어요:
m_app : Maybe (a -> b) -> Maybe a -> Maybe b
m_app (Just f) (Just a) = Just (f a)
m_app _ _ = Nothing
이것을 사용해, m_app에 대한 명시적 호출과 함께 함수 적용의 이 대안적 개념을 사용하는 대안 m_add를 작성할 수 있어요:
m_add' : Maybe Int -> Maybe Int -> Maybe Int
m_add' x y = m_app (m_app (Just (+)) x) y
적용이 있는 곳마다 m_app을 삽입해야 하기보다는, idiom 괄호를 사용해 그 일을 대신하게 할 수 있어요.
이를 위해 Maybe에 Applicative 구현을 다음과 같이 줄 수 있는데, 여기서 <*>는 위의 m_app과 같은 방식으로 정의돼요 (이것은 Idris 라이브러리에 정의되어 있어요):
Applicative Maybe where
pure = Just
(Just f) <*> (Just a) = Just (f a)
_ <*> _ = Nothing
<*>를 사용하면, 함수 적용 [| f a1 …an |]가 pure f <*> a1 <*> … <*> an으로 번역되는 데, 이것을 다음과 같이 사용할 수 있어요:
m_add' : Maybe Int -> Maybe Int -> Maybe Int
m_add' x y = [| x + y |]
오류 처리 인터프리터 (An error-handling interpreter)
Idiom 표기법은 평가기(evaluators)를 정의할 때 일반적으로 유용해요. McBride와 Paterson은 다음 언어와 유사한 언어에 대한 그런 평가기를 기술해요 [1]:
data Expr = Var String -- variables
| Val Int -- values
| Add Expr Expr -- addition
평가는 변수(문자열로 표현)를 Int 값에 매핑하는 컨텍스트에 대해 일어나며, 실패할 수 있어요.
평가기를 감싸는 데이터 타입 Eval을 정의해요:
data Eval : Type -> Type where
MkEval : (List (String, Int) -> Maybe a) -> Eval a
평가기를 데이터 타입에 감싸는 것은 나중에 그것을 위해 인터페이스 구현을 제공할 수 있다는 뜻이에요. 평가 중에 컨텍스트에서 값을 검색하는 함수를 정의하는 것으로 시작해요:
fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
fetchVal : List (String, Int) -> Maybe Int
fetchVal [] = Nothing
fetchVal ((v, val) :: xs) = if (x == v)
then (Just val)
else (fetchVal xs)
언어에 대한 평가기를 정의할 때 우리는 Eval의 컨텍스트에서 함수를 적용할 것이므로, Eval에 Applicative 구현을 주는 것이 자연스러워요. Eval이 Applicative 구현을 가질 수 있으려면 먼저 Eval이 Functor 구현을 가져야 해요:
Functor Eval where
map f (MkEval g) = MkEval (\e => map f (g e))
Applicative Eval where
pure x = MkEval (\e => Just x)
(<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
app : Maybe (a -> b) -> Maybe a -> Maybe b
app (Just fx) (Just gx) = Just (fx gx)
app _ _ = Nothing
이제 식을 평가하는 것은 오류를 처리하기 위해 idiomatic 적용을 활용할 수 있어요:
eval : Expr -> Eval Int
eval (Var x) = fetch x
eval (Val x) = [| x |]
eval (Add x y) = [| eval x + eval y |]
runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e = case eval e of
MkEval envFn => envFn env
이름 붙은 구현 (Named Implementations)
같은 타입에 대한 인터페이스의 여러 구현을 갖는 것이 바람직할 수 있어요. 예를 들어 값의 정렬이나 출력에 대한 대안 메서드를 제공하기 위해서요. 이를 위해 구현은 다음과 같이 이름을 붙일 수 있어요:
[myord] Ord Nat where
compare Z (S n) = GT
compare (S n) Z = LT
compare Z Z = EQ
compare (S x) (S y) = compare @{myord} x y
이것은 구현을 평소처럼 선언하지만, 명시적 이름 myord를 가져요. 문법 compare @{myord}는 compare에 명시적 구현을 줘요. 그렇지 않으면 Nat에 대한 기본 구현을 사용할 거예요. 이 예를 사용해 Nat 리스트를 역순으로 정렬할 수 있어요.
다음 리스트가 주어졌을 때:
testList : List Nat
testList = [3,4,1]
Idris 프롬프트에서 기본 Ord 구현, 그 다음 이름 붙은 구현 myord로 다음과 같이 정렬할 수 있어요:
*named_impl> show (sort testList)
"[sO, sssO, ssssO]" : String
*named_impl> show (sort @{myord} testList)
"[ssssO, sssO, sO]" : String
때로는 이름 붙은 부모 구현에 대한 접근도 필요해요. 예를 들어 프렐류드는 다음 Semigroup 인터페이스를 정의해요:
interface Semigroup ty where
(<+>) : ty -> ty -> ty
그 다음 그것은 "중립(neutral)" 값으로 Semigroup을 확장하는 Monoid를 정의해요:
interface Semigroup ty => Monoid ty where
neutral : ty
Nat에 대한 Semigroup과 Monoid의 두 가지 다른 구현을 — 하나는 덧셈 기반, 하나는 곱셈 기반으로 — 정의할 수 있어요:
[PlusNatSemi] Semigroup Nat where
(<+>) x y = x + y
[MultNatSemi] Semigroup Nat where
(<+>) x y = x * y
덧셈의 중립 값은 0이지만 곱셈의 중립 값은 1이에요. 따라서 Monoid 구현을 정의할 때 올바른 Semigroup 구현을 확장하는 것이 중요해요. 구현에서 using 절로 다음과 같이 할 수 있어요:
[PlusNatMonoid] Monoid Nat using PlusNatSemi where
neutral = 0
[MultNatMonoid] Monoid Nat using MultNatSemi where
neutral = 1
using PlusNatSemi 절은 PlusNatMonoid가 구체적으로 PlusNatSemi를 확장해야 함을 나타내요.
결정 매개변수 (Determining Parameters)
인터페이스가 둘 이상의 매개변수를 가질 때, 구현을 찾는 데 사용되는 매개변수를 제한하면 해결에 도움이 될 수 있어요. 예를 들어:
interface Monad m => MonadState s (m : Type -> Type) | m where
get : m s
put : s -> m ()
이 인터페이스에서 이 인터페이스의 구현을 찾으려면 m만 알면 되고, s는 구현에서 결정될 수 있어요. 이것은 인터페이스 선언 뒤의 | m으로 선언돼요. 우리는 m을 MonadState 인터페이스의 결정 매개변수(determining parameter)라고 불러요. 왜냐하면 그것이 구현을 찾는 데 사용되는 매개변수이기 때문이에요.
[1]
(1, 2) Conor McBride and Ross Paterson. 2008. Applicative programming with effects. J. Funct. Program. 18, 1 (January 2008), 1-13. DOI=10.1017/S0956796807006326 http://dx.doi.org/10.1017/S0956796807006326