Haskell에서 Profunctor Equipment 구현하기

범주론(Category theory)은 구체적인 구현에 기반을 두지 않으면 종종 추상적으로 느껴집니다. 최근의 탐구에서 Bartosz Milewski는 정교한 범주적 구조인 "Profunctor Equipment"를 Haskell 내에서 구현하는 방법을 보여줍니다. 완전한 구현을 위해서는 이상적으로 의존 타입 언어(dependently typed language)가 필요하겠지만, Haskell의 타입 시스템은 프로그래머가 컴파일러를 통해 이러한 수학적 직관을 검증할 수 있는 장난감 수준의 구현(toy implementation)을 제공하기에 충분히 강력합니다.

Profunctor Equipment의 핵심 구성 요소

Haskell에서 Profunctor Equipment를 구현하려면 범주적 개념을 Haskell의 타입 시스템으로 매핑해야 합니다. 이 구현은 단일 범주(타입과 함수의 Haskell 범주)에 집중하며, endo-functors와 endo-profunctors로 제한됩니다.

0-Cells, 1-Cells, 그리고 2-Cells

이 프레임워크에서 구성 요소는 다음과 같이 정의됩니다:

  • 0-Cells: 타입과 함수의 Haskell 범주.
  • Vertical 1-Cells: 표준 라이브러리의 Functor를 사용하여 구현됩니다.
  • Horizontal 1-Cells: Profunctor를 사용하여 구현됩니다.
  • 2-Cells: 이는 자연 변환(natural transformations)으로 구현됩니다. Haskell에서 이는 다음과 같은 다형성 함수로 표현됩니다:
type Cell f g h j = forall a c . h a c -> j (f a) (g c)

여기서 forall은 보편 양화사(universal quantifier) 역할을 하여, 변환이 모든 타입 a와 c에 대해 성립함을 보장합니다.

합성(Composition)과 단위(Units)

Equipment를 구현할 때 주요 과제 중 하나는 수평(horizontal) 및 수직(vertical)이라는 서로 다른 합성 모드를 처리하는 것입니다.

수평 합성(Horizontal Composition)

수평 합성은 두 셀을 결합하여 합성된 펑터에 작용하는 새로운 셀을 생성합니다. 펑터 합성을 위해 Compose newtype을 사용하면 구현은 다음과 같습니다:

hcomp :: (Functor f, Functor f', Functor g, Functor g'
         , Profunctor h, Profunctor j, Profunctor k) =>
    Cell f g h j -> Cell f' g' j k 
                 -> Cell (Compose f' f) (Compose g' g) h k

hcomp fg_hj fg_jk hac = dimap getCompose Compose $ fg_jk (fg_hj hac)

수직 합성(Vertical Composition)과 Coends

수직 합성은 더 복잡하며 profunctor 합성을 필요로 합니다. 이는 coend를 사용하여 구현되며, Haskell에서는 실존 타입(existential type)으로 표현됩니다:

data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

이 정의에서 x는 실존 타입입니다. 즉, 인자 목록에 나타나지 않으므로 외부 세계로부터 숨겨져 있으며, 이는 범주론에서 coends가 작동하는 방식과 정확히 일치합니다.

단위 셀(Unit Cells)

Equipment의 법칙을 만족시키기 위해, 두 차원 모두에 대해 단위 셀이 정의되어야 합니다:

  • Horizontal Unit: type Hunit p = Cell Identity Identity p p
  • Vertical Unit: type Vunit f a b = Cell f f (->) (->)

Companion과 Conjoint

이 구현은 companion과 conjoint 개념으로 더 확장되는데, 이는 본질적으로 Haskell 생태계에서 발견되는 Costar와 Star 타입의 동의어입니다.

  • Companion: Costar f d c로 표현되며, newtype Costar f d c = Costar { runCostar :: f d -> c }로 정의됩니다.
  • Conjoint: Star f d c로 표현되며, newtype Star f d c = Star { runStar :: d -> f c }로 정의됩니다.

이들은 unit 및 counit 셀을 갖추고 있습니다. 예를 들어, companion unit과 counit은 다음과 같이 정의됩니다:

type CompUnit f   = Cell Identity f (->) (Costar f)
compUnit :: Functor f => CompUnit f
compUnit h = Costar (fmap (h . runIdentity))

type CompCoUnit f = Cell f Identity (Costar f) (->)
compCoUnit (Costar h) = Identity . h

기술적 성찰 및 한계

이 Haskell 구현은 추상적인 수학과 실행 가능한 코드 사이의 가치 있는 가교 역할을 하지만, 한계가 있습니다. 저자는 이러한 타입들 사이의 관계를 더 엄격하게 강제하고 증명할 수 있는, 의존 타입 언어(예: Lean)와 같은 더 적절한 구현이 필요하다고 언급합니다.

이러한 의견은 커뮤니티에서도 공감대를 형성하고 있으며, 일부는 의존 타입 언어가 이 정도 수준의의 형식적 검증(formal verification)에 더 적합하다고 제안합니다. 그러나 이 "장난감" 구현의 유용성은 여전합니다. 프로그래머가 Haskell 컴파일러를 범주적 구조에 대한 건전성 검사(sanity check)로 사용할 수 있게 해주기 때문입니다.

이론적 깊이에도 불구하고, 일부 실무자들은 이러한 구조와 실제 응용 사이의 간극을 주목합니다. 이러한 고수준의 범주적 equipment를 개발자에게 실질적인 이점을 제공하는 일상적인 소프트웨어 엔지니어링 패턴으로 변환하는 것이 여전히 과제로 남아 있습니다.

Sources