어렵게 설명한 모나드

2013년 7월 7일 · 태그: haskell, category theory · 원문 · 한국어 번역(원문에서 변경됨)

이 글은 범주론적 관점에서 유도한 Haskell 모나드에 대한 짧고 빠르며 비유를 쓰지 않는 입문입니다. 이 글은 독자가 Haskell과 기초 범주론에 익숙하다고 가정합니다.

범주

대상과 사상으로 이루어진 추상적인 범주 $\mathcal{C}$가 있습니다.

• 대상 : $●$
• 사상 : $●\to ●$

각 대상에는 항등 사상 id가 있고, 사상을 결합적으로 합성하는 합성 규칙 $(\circ )$가 있습니다. 이것은 Haskell에서 카인드 다형성을 이용한 다음 타입 클래스로 모델링할 수 있습니다.

-- Morphisms
type (a ~> b) c = c a b

class Category (c :: k -> k -> *) where
  id :: (a ~> a) c
  (.) :: (y ~> z) c -> (x ~> y) c -> (x ~> z) c

Haskell에서는 Haskell 타입 사이의 함수 타입을 나타내는 타입 생성자 (->) 위의 이 범주를 Hask라고 부릅니다.

type Hask = (->)

instance Category Hask where
  id x = x
  (f . g) x = f (g x)

생성자 (->)는 타입 클래스 시그니처에서 타입 수준 연산자로 읽을 때 때때로 헷갈립니다. 중위 형태에서는 보통 첫 번째 인자가 그 왼쪽에, 두 번째 인자가 오른쪽에 나타나기 때문입니다. 예를 들어 다음은 서로 동등합니다.

(->) ((->) a b) ((->) a c)

(a -> b) -> (a -> c)

함자

두 범주 사이에 $T$로 표기하는 함자를 구성할 수 있습니다. 함자는 범주의 대상과 사상 사이를 사상하며, 사상의 합성과 항등을 보존합니다.

• 대상 : $T(●)$
• 사상 : $T(●\to ●)$

Haskell에서는 다음과 같이 표현됩니다.

class (Category c, Category d) => Functor c d t where
  fmap :: c a b -> d (t a) (t b)

익숙한 함자 법칙은 다음과 같습니다.

fmap id ≡ id
fmap (a . b) ≡ (fmap a) . (fmap b)

범주 $\mathcal{C}$에 대한 항등 함자 $1_{\mathcal{C}}$는 모든 대상을 자기 자신으로, 모든 사상을 자기 자신으로 보내는 함자입니다.

newtype Id a = Id a

instance Functor Hask Hask Id where
  fmap f (Id a) = Id (f a)

instance Functor Hask Hask [] where
  fmap f [] = []
  fmap f (x:xs) = f x : (fmap f xs)

instance Functor Hask Hask Maybe where
  fmap f Nothing = Nothing
  fmap f (Just x) = Just (f x)

자기 함자(endofunctor)는 한 범주에서 그 범주 자신으로 가는 함자, 즉 ($T:\mathcal{C}\to \mathcal{C}$)입니다.

type Endofunctor c t = Functor c c t

두 함자의 합성 역시 그 자체로 함자입니다. 이 사실을 Haskell에 납득시키려면 제약 카인드(constraint kinds)와 범위 지정 타입 변수(scoped type variables)를 이용한 약간의 기교가 필요합니다.

newtype FComp g f x = C { unC :: g (f x) }
newtype Hom (c :: * -> Constraint) a b = Hom (a -> b)

instance (Functor a b f, Functor b c g, c ~ Hom k) => Functor a c (FComp g f) where
  fmap f = (Hom C) . (fmapg (fmapf f) . (Hom unC))
    where
      fmapf = fmap :: a x y -> b (f x) (f y)
      fmapg = fmap :: b s t -> c (g s) (g t)

한 범주 위의 자기 함자를 반복해서 합성한 것은 지수 표기법으로 씁니다.

$$\begin{array}{rlr}{T}^2& =TT:\mathcal{C}\to \mathcal{C}{T}^3& =TTT:\mathcal{C}\to \mathcal{C}\end{array}$$

작은 범주들의 범주 $\text{Cat}$은 범주를 대상으로, 범주 사이의 함자를 사상으로 갖는 범주입니다.

자연 변환

두 범주 $\mathcal{A},\mathcal{B}$ 사이의 두 함자 $F,G$에 대해 다음을 생각합시다.

$$F:\mathcal{A}\to \mathcal{B}G:\mathcal{A}\to \mathcal{B}$$

자연 변환 $\eta$라고 부르는 사상을 구성할 수 있습니다. 이는 함자 사이의 사상 $\eta :F\to G$로서, $\mathcal{A}$의 모든 대상 $X$를 $\mathcal{B}$의 사상에 대응시킵니다.

$${\eta }_X:F(X)\to G(X)$$

이때 임의의 사상 $f:X\to Y$에 대해 다음 자연성 조건이 성립해야 합니다. 이는 다음과 같은 자연성 사각형으로 나타냅니다.

$${\eta }_Y\circ F(f)=G(f)\circ {\eta }_X$$

자연 변환 자체는 두 함자 사이에서 다음과 같은 도식으로 나타냅니다.

이것은 앞에서 정의한 일반적인 범주 클래스에서 다음과 같은 존재 타입으로 표현할 수 있습니다.

type Nat c f g = forall a. c (f a) (g a)

Hask의 경우에는 다음 시그니처를 갖는 다형 함수들의 족이 있습니다.

type NatHask f g = forall a. (f a) -> (g a)

자연 변환(h)에 대해 자연성 조건은 다음 법칙으로 주어지며, 이는 마침 Haskell 타입 시스템에서의 자유 정리(free theorem)이기도 합니다.

fmap f . h ≡ h . fmap f

대표적인 예는 List 함자와 Maybe 함자 사이의 자연 변환입니다( 여기서 f = List, g = Maybe ).

headMay :: forall a. [a] -> Maybe a
headMay []     = Nothing
headMay (x:xs) = Just x

어느 쪽으로 도식을 따라가든 같은 곳에 도달합니다.

fmap f (headMay xs) ≡ headMay (fmap f xs)

이 사실을 확인하고 싶다면 headMay에 대한 자연성 사각형의 각 경우를 하나씩 따져 보십시오.

fmap f (headMay [])
= fmap f Nothing
= Nothing

headMay (fmap f [])
= headMay []
= Nothing

fmap f (headMay (x:xs))
= fmap f (Just x)
= Just (f x)

headMay (fmap f (x:xs))
= headMay [f x]
= Just (f x)

함자 범주

자연 변환 $\eta :C\to D$는 그 자체로 $\mathcal{C}$와 $\mathcal{D}$ 사이의 함자들로 이루어진 함자 범주 $\text{Fun}(\mathcal{C},\mathcal{D})$의 사상입니다. 범주 $\text{End}$는 한 범주에서 그 자신으로 가는 자기 함자(endofunctor)들의 범주입니다.

-- Functor category
newtype Fun f g a b = FNat (f a -> g b)

-- Endofunctor category
type End f = Fun f f

instance Category (End f) where
  id = FNat id
  (FNat f) . (FNat g) = FNat (f . g)

모나드

이제 마침내 범주 $\mathcal{C}$ 위의 모나드를 다음으로 이루어진 삼중쌍 $(T,\eta ,\mu )$로 정의할 수 있습니다.

1. 자기 함자 $T:\mathcal{C}\to \mathcal{C}$
2. 자연 변환 $\eta :1_{\mathcal{C}}\to T$
3. 자연 변환 $\mu :T^2\to T$

class Endofunctor c t => Monad c t where
  eta :: c a (t a)
  mu  :: c (t (t a)) (t a)

결합성 사각형과 함께:

$$\mu \circ T\mu =\mu \circ \mu T$$

그리고 삼각형 등식과 함께:

$$\mu \circ T\eta =\mu \circ \eta T=1_C$$

또는 이 삼중쌍을 일련의 **문자열 도식(string diagram)**으로 표현할 수도 있습니다. 문자열 도식에서는 선을 사상으로, 점을 대상으로 나타내는 전통적인 가환 도식을 뒤집어, 사상을 점으로, 대상을 선으로 나타냅니다. 이 형태에서 모나드 법칙은 멋진 기하학적 대칭성을 가집니다.

정합성 조건을 도식으로 나타내면 다음과 같습니다.

Bind/Return 정식화

모나드는 mu, eta)로 표현할 수 있는 두 함수((>>=), return)를 사용한 동등한 정식화로도 나타낼 수 있습니다.

Haskell에서는 자연 변환과 기반 함자의 fmap을 사용하여 정의되는 bind 연산자 (>>=)를 정의합니다. join과 return 함수는 mu와 eta를 사용하여 정의할 수 있습니다.

(>>=) :: (Monad c t) => c a (t b) -> c (t a) (t b)
(>>=) f = mu . fmap f

return :: (Monad c t) => c a (t a)
return = eta

이 형태에서는 모나드의 자연 변환에 대한 동등한 자연성 조건에 새 정의를 대입하면 일반적인 모나드 법칙이 나옵니다.

fmap f . return  ≡  return . f
fmap f . join    ≡  join . fmap (fmap f)

그리고 bind와 return으로 표현한 동등한 정합성 조건이 바로 잘 알려진 모나드 법칙입니다.

return a >>= f   ≡  f a
m >>= return     ≡  m
(m >>= f) >>= g  ≡  m >>= (\x -> f x >>= g)

클라이슬리 범주

최종 결과는, 모나드가 주어지면 그 모나드로부터 클라이슬리 범주라는 새로운 범주를 만들 수 있다는 것입니다. 대상은 원래의 c 범주에 들어 있지만, 화살표는 이제 클라이슬리 화살표 a -> T b입니다. 이러한 “동작“들이 주어졌을 때, 우리는 호스트 범주에서 함수를 합성하듯이 이 사상들을 합성하는 연산자를 작성하고자 합니다.

$$\begin{array}{rlr}& (b\to Tc)\to (a\to Tb)\to (a\to Tc)& (b\to c)\to (a\to b)\to (a\to c)\end{array}$$

알고 보니 $\mu$와 기반 함자를 사용하여 표현되는 특정 함수 (<=<)를 만들 수 있으며, 이 함수는 클라이슬리 화살표의 결합적 합성 연산자가 됩니다. 클라이슬리 범주는 “동작의 합성“을 모델링하며, 매우 일반적인 계산 모델을 이룹니다.

범주 $\mathcal{C}$로부터 구성된 클라이슬리 범주에서의 대응은 다음과 같습니다:

1. 클라이슬리 범주의 대상은 기반 범주의 대상입니다.
2. 사상은 다음 형태의 클라이슬리 화살표입니다: $f:A\to TB$
3. 클라이슬리 범주의 항등 사상은 정확히 기반 범주의 $\eta$입니다.
4. 호스트 범주의 관점에서 사상의 합성 $f\circ g$는 다음 대응으로 정의됩니다:

$$f\circ g=\mu (Tf)g$$

-- Kleisli category
newtype Kleisli c t a b = K (c a (t b))

-- Kleisli morphisms ( c a (t b) )
type (a :~> b) c t = Kleisli c t a b

-- Kleisli morphism composition
(<=<) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z)
f <=< g = mu . fmap f . g

instance Monad c t => Category (Kleisli c t) where
  -- id :: (Monad c t) => c a (t a)
  id = K eta

  -- (.) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z)
  (K f) . (K g) = K ( f <=< g )

c = (->)인 Hask의 경우에는 익숙한 인스턴스를 볼 수 있습니다:

-- Kleisli category
newtype Kleisli m a b = K (a -> m b)

-- Kleisli morphisms ( a -> m b )
type (a :~> b) m = Kleisli m a b

(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
f <=< g = mu . fmap f . g

instance Monad m => Category (Kleisli m) where
  id            = K return
  (K f) . (K g) = K (f <=< g)

class Functor t where
  fmap :: (a -> b) -> t a -> t b

class Functor t => Monad t where
  eta :: a -> (t a)
  mu  :: t (t a) -> (t a)

(>>=) :: Monad t => t a -> (a -> t b) -> t b
ma >>= f = join . fmap f

간단히 말해 위의 모나드 법칙은 클라이슬리 범주에서의 범주 법칙일 뿐이며, 구체적으로 모나드 m의 클라이슬리 범주의 관점에서 모나드 법칙은 다음과 같습니다:

(f >=> g) >=> h ≡ f >=> (g >=> h)
return >=> f ≡ f
f >=> return ≡  f

예를 들어 Just는 Maybe 모나드의 클라이슬리 범주에서 항등 사상일 뿐입니다.

Just >=> f = f
f >=> Just = f

just :: (a :~> a) Maybe
just = K Just

left :: forall a b. (a :~> b) Maybe -> (a :~> b) Maybe
left f = just . f

right :: forall a b. (a :~> b) Maybe -> (a :~> b) Maybe
right f = f . just

Haskell 모나드

예를 들어 List 모나드는 다음을 갖습니다:

1. $\eta$는 하나의 원소로부터 단일 원소 리스트를 반환합니다.
2. $\mu$는 중첩된 리스트를 평탄한 리스트로 바꿉니다.
3. $\mathtt{fmap}$은 리스트의 원소들에 함수를 적용합니다.

instance Functor [] where
  -- fmap :: (a -> b) -> [a] -> [b]
  fmap f (x:xs) = f x : fmap f xs

instance Monad [] where
  -- eta :: a -> [a]
  eta x = [x]

  -- mu :: [[a]] -> [a]
  mu = concat

Maybe 모나드는 다음을 갖습니다:

1. $\eta$는 Just 생성자입니다.
2. $\mu$는 두 겹의 Just 생성자를 합쳐 안쪽 값 또는 Nothing을 내놓습니다.
3. $\mathtt{fmap}$은 Just 생성자 아래에서 함수를 적용하고, Nothing에 대해서는 아무것도 하지 않습니다.

instance Functor [] where
  -- fmap :: (a -> b) -> Maybe a -> Maybe b
  fmap f (Just x) = Just (f x)
  fmap f Nothing = Nothing

instance Monad Maybe where
  -- eta :: a -> Maybe a
  eta x = Just x

  -- mu :: (Maybe (Maybe a)) -> Maybe a
  mu (Just (Just x)) = Just x
  mu (Just Nothing) = Nothing

IO 모나드는 직관적으로 다음과 같은 구현을 갖습니다:

1. $\eta$는 순수한 값을 계산의 문맥 안에 있는 값으로 반환합니다.
2. $\mu$는 일련의 IO 연산을 하나의 IO 연산으로 바꿉니다.
3. $\mathtt{fmap}$은 계산의 결과에 함수를 적용합니다.

instance Functor IO where
  -- fmap :: (a -> b) -> IO a -> IO b

instance Monad Maybe where
  -- eta :: a -> IO a
  -- mu :: (IO (IO a)) -> IO a