Haskell Language
범주 이론

추상화를 구성하는 시스템으로서의 범주 이론

범주 이론은 근대 수학 이론이자 연결성과 관계의 본질에 초점을 둔 추상 대수학의 한 부분입니다. 재사용 가능한 많은 프로그래밍 추상화에 견고한 기반과 공통 언어를 제공하는 데 유용합니다. Haskell은 표준 라이브러리와 몇 가지 인기있는 써드 파티 라이브러리 모두에서 사용할 수있는 핵심 유형 클립에 대한 카테고리 이론을 영감으로 사용합니다.

예제

Functor typeclass는 Type F Functor 인스턴스화하면 ( Functor F 쓰는 경우) 우리는 일반적인 연산

fmap :: (a -> b) -> (F a -> F b)

F 통해 "맵핑"할 수 있습니다. 표준 (그러나 불완전) 직관이다 F a 형의 값으로 가득 찬 컨테이너 a 와 fmap 우리가 요소를 포함 이들 각각에 변환을 적용 할 수 있습니다. 예를 들면 Maybe

instance Functor Maybe where
  fmap f Nothing = Nothing     -- if there are no values contained, do nothing
  fmap f (Just a) = Just (f a) -- else, apply our transformation

이 직관을 감안할 때, 일반적인 질문은 " Mappable Functor Mappable 과 같이 명백하게 호출하는 것이 어떻습니까?"입니다.

카테고리 이론의 힌트

그 이유는 Functor가 범주 이론에서 공통적 인 구조의 세트에 들어 맞기 때문에 Functor "Functor"를 호출함으로써 더 깊은 지식 체계에 어떻게 연결되는지 볼 수 있습니다.

특히 범주 이론은 한 곳에서 다른 곳으로가는 화살표의 개념에 크게 관심이 있습니다. 하스켈에서 가장 중요한 화살표는 기능 화살표 a -> b 입니다. 카테고리 이론에서 연구해야 할 공통점은 한 세트의 화살표가 다른 세트와 어떤 관련이 있는지입니다. 특히 모든 유형 생성자 F 에 대해 F a -> F b 모양의 화살표 집합도 흥미 롭습니다.

따라서 Functor는 정상적인 Haskell 화살표 a -> b 와 F - 특정 화살표 F a -> F b 사이의 연결이있는 임의의 F 입니다. 연결은 fmap 의해 정의되고 우리는 또한 유지해야하는 몇 가지 법칙을 인식합니다

forall (x :: F a) . fmap id x == x

forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)

이러한 모든 법칙은 Functor 대한 범주 이론적 해석에서 자연스럽게 발생하며 "요소를 통한 매핑"과 관련하여 Functor 를 생각한 경우 분명히 필요하지 않습니다.

카테고리 정의

카테고리 C 는 다음과 같이 구성됩니다.

• 객체 컬렉션 Obj(C) ;
• 이 객체들 사이의 모폴로지 컬렉션 ( Hom(C) 라고 함 Hom(C) . 경우 및 a b 에 Obj(C) 다음 morphism에의 f 에서 Hom(C) 일반적으로 표시되는 f : a -> b , 사이 모두 morphism에 수집 및 a b 나타낸다 hom(a,b) ;
• 정체성 모폴로지 ( identity morphism)라고 불리는 특수한 모 플리즘 - 모든 a : Obj(C) 에는 변이가 있습니다. id : a -> a ;
• 조성물 연산자 ( . 두 morphisms 복용) f : a -> b , g : b -> c 및 morphism에의 제조 a -> c

이는 다음 법률을 준수합니다.

For all f : a -> x, g : x -> b, then id . f = f and g . id = g

For all f : a -> b, g : b -> c and h : c -> d, then h . (g . f) = (h . g) . f

다른 말로하면, 정체성 모프 즘을 가진 구성 (왼쪽 또는 오른쪽)은 다른 모 플리즘을 변화시키지 않으며 구성은 연관 적입니다.

Haskell에서, Category 는 Control.category 의 typeclass로 정의됩니다.

-- | A class for categories.
--   id and (.) must form a monoid.
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

이 경우, cat :: k -> k -> * 는 morphism 관계를 구체화합니다 - cat ab 가 살고있는 경우에만 (즉, 값이있는 경우) 변태 cat ab 가 존재합니다. a , b 및 c 는 모두 Obj(C) 있습니다. Obj(C) 자체는 종류 k 표시됩니다. 예를 들어 k ~ * 가 대개의 경우와 같이 객체는 유형입니다.

하스켈에서 카테고리의 표준적인 예는 함수 카테고리입니다 :

instance Category (->) where
  id = Prelude.id
  (.) = Prelude..

또 다른 일반적인 예는 Monad 대한 Kleisli Category 의 화살표입니다.

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

class Monad m => Category (Kleisli m) where
  id = Kleisli return
  Kleisli f . Kleisli g = Kleisli (f >=> g)

하스켈은 카테고리로 타이핑한다.

카테고리의 정의

하스켈 유형과 유형 간의 함수 (거의 †)가 범주를 형성합니다. 우리는 모든 객체 (유형) a 대해 항등 변위 (함수) ( id :: a -> a )를가집니다. 카테고리 법칙에 따르는 변이 형 ( (.) :: (b -> c) -> (a -> b) -> a -> c )

f . id = f = id . f
h . (g . f) = (h . g) . f 

우리는 일반적으로이 카테고리를 Hask 라고 부릅니다 .

동형 이의어

범주 이론에서 우리는 역행렬을 갖는 형태론을 가질 때 동형 성을 가지고 있습니다. 다시 말하면, 정체성을 창출하기 위해 그것과 함께 구성 될 수있는 변이가 있다는 것입니다. Hask에서 이것은 다음과 같은 한 모핑 f , g 가지게됩니다 :

 f . g == id == g . f

두 가지 유형 사이에 한 쌍의 변형을 발견하면, 그것들 을 서로 동형 이라고 부릅니다.

두 가지 동형 유형의 예는 ((),a) 이고 a 는 a 입니다. 우리는 두 가지 형태를 만들 수 있습니다 :

f :: ((),a) -> a
f ((),x) = x

g :: a -> ((),a)
g x = ((),x)

그리고 우리는 이것을 확인할 수 있습니다 f . g == id == g . f .

펑터

범주 이론에있는 펑터는 범주에서 다른 객체, 모핑을 매핑합니다. 우리는 하나 개의 범주, 하스켈 유형의 범주 Hask에 최선을 다하고 있습니다, 그래서 우리는 Hask에서 출발지와 목적지 카테고리 동일이라고 endofunctors은 Hask, 그 펑, 만 펑터를 볼 것입니다. 우리의 endofunctors는 타입을 취하고 다른 타입을 반환하는 다형 타입입니다 :

F :: * -> *

범주화 된 펑터 법칙 (정체성과 구성 보존)은 Haskell 펑터 법칙을 준수하는 것과 같습니다.

fmap (f . g) = (fmap f) . (fmap g)
fmap id = id

예를 들어 [] , Maybe 또는 (-> r) 은 Hask의 펑터입니다.

모나드

범주 이론의 모나드 는 내관 의 범주에 대한 단조입니다. 이 범주는 관상어를 객체 F :: * -> * 및 자연 변형 (모든 forall a . F a -> G a 변환 forall a . F a -> G a )으로 변환합니다.

monoid 객체는 monoidal 카테고리에 정의 될 수 있으며, 두 개의 morphisms을 갖는 타입입니다 :

zero :: () -> M
mappend :: (M,M) -> M

이것을 Hask의 endofunctors의 카테고리로 대략 번역 할 수 있습니다 :

return :: a -> m a
join :: m (m a) -> m a 

그리고 모나드 법칙에 복종하는 것은 범주 형 모노 객체 법칙을 준수하는 것과 같습니다.

사실, 유형 사이의 함수 클래스와 함께 모든 유형의 클래스는 undefined 존재로 인해 하스켈에서 엄격하게 카테고리를 형성하지 않습니다 . 전형적으로 Hask 범주의 객체를 종결 값이없는 유형으로 정의하고 종결되지 않는 함수와 무한 값 (코드 타당구)을 제외하면됩니다. 이 주제에 대한 자세한 내용은 여기를 참조 하십시오 .

Hask에있는 유형의 제품

범주 형 제품

카테고리 이론에서, 두 객체 X , Y의 결과 는 두 개의 투영을 갖는 또 다른 객체 Z 입니다 : π1 : Z → X 와 π2 : Z → Y ; 다른 물체의 다른 두 가지 형태는 그 투영법을 통해 고유하게 분해됩니다. 다시 말해, f1 : W → X 와 f2 : W → Y 가 존재한다면, π1 → g = f1 과 π2 → g = f2 가되는 고유 한 변이 g : W → Z 가 존재한다.

하스크의 제품

이것은 다음과 같이 Haskell 타입의 Hask 카테고리로 변환됩니다. Z 는 A , B .

-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g  :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2

위에서 언급 한 법칙을 따르는 A , B 두 가지 유형의 제품 유형은 두 가지 유형 (A,B) 의 튜플 이며 두 투영은 fst 및 snd 입니다. 우리는 f1 :: W -> A 와 f2 :: W -> B 두 가지 함수가있는 경우 위의 규칙을 따르는 지 확인할 수 있습니다. 다음과 같이 고유하게 분해 할 수 있습니다.

decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))

그리고 우리는 분해가 올바른지 확인할 수 있습니다 :

fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2

동형 이성에 대한 독창성

A 와 B 의 곱으로서의 (A,B) 의 선택은 고유하지 않다. 논리적이고 동등한 또 다른 선택은 다음과 같습니다.

data Pair a b = Pair a b

또한, (B,A) 를 제품으로 선택하거나 심지어 (B,A,()) 로 선택할 수 있으며, 규칙과 동일한 분해 함수를 찾을 수 있습니다.

decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))

이것은 제품이 유일하지는 않지만 동형에 속하기 때문 입니다. A 와 B 의 두 곱 모두는 같을 필요는 없지만 동형이어야합니다. 예를 들어 방금 정의한 두 개의 다른 제품 (A,B) 과 (B,A,()) 는 동형입니다.

iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())

iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)

분해의 고유성

분해 함수도 고유해야한다는 점에 주목하는 것이 중요합니다. 제품으로 요구되는 모든 규칙을 따르는 유형이 있지만 분해는 고유하지 않습니다. 예를 들어, (A,(B,Bool)) 을 투영 fst fst . snd 로 사용하려고 할 수 있습니다 fst . snd A 와 B 의 곱으로서의 fst . snd :

decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))

우리는 그것이 작동하는지 확인할 수 있습니다 :

fst         . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x

그러나 여기서의 문제는 우리가 또 다른 분해를 작성할 수 있다는 것입니다.

decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))

그리고, 분해가 유일하지 않기 때문에 , (A,(B,Bool)) 는 Hask 의 A 와 B 의 산물이 아닙니다

한스에있는 유형의 Coproduct

직관

A 와 B 의 두 가지 유형의 범주 형 제품에는 A 유형 또는 B 유형 의 인스턴스 내부를 포함하는 데 필요한 최소한의 정보가 들어 있어야합니다. 이제 우리는 두 가지 유형의 직관적 인 공동 생성물이 Either ab 이어야 함을 알 수 있습니다. Either a (b,Bool) 와 같은 다른 후보는 불필요한 정보의 일부를 포함 할 것이고 최소한의 정보는 아닙니다.

공식 정의는 공동 생산물의 범주 적 정의에서 파생됩니다.

범주 형 공동 제작물

범주 형 공동 제품은 범주 형 제품의 이중 개념입니다. 이것은 제품 정의의 모든 화살표를 반대로하여 직접 얻을 수 있습니다. 두 객체의 부산물 X, Y는 두 개의 흠 다른 오브젝트 Z는 다음 i_1 : X → Z 및 I_2 : Y → Z의; X 와 Y 에서 다른 대상으로의 다른 두 가지 형태는 그 포함을 통해 고유하게 분해됩니다. 즉, f1 : X → W 와 f2 : Y → W의 두 가지 변이가 존재한다면, g → i1 = f1 , g → i2 = f2

하스크의 제품

Hask 범주로의 번역은 제품 번역과 유사합니다.

-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g  :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2

Hask의 A 와 B 의 두 가지 유형의 coproduct 유형은 Either ab 이거나 다른 동형 유형입니다.

-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b

-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x)  = f1 x
decompose f1 f2 (Right y) = f2 y 

범주 이론의 관점에서 하스켈 응용

하스켈의 Functor 는 어떤 타입 a ( Hask 의 객체)를 타입 F a 에 매핑 할 수있게 해주 며 또한 a -> b ( Hask 의 morphism)를 타입 F a -> F b 의 함수로 매핑 합니다. 이것은 펑터가 기본 범주 구조를 보존한다는 의미에서 범주 이론 정의에 해당합니다.

모노 도형 범주 는 몇 가지 추가 구조가있는 범주입니다.

• 텐서 산물 ( Hask의 산물 유형 참조)
• 텐서 단위 (단위체)

쌍을 우리 제품으로 사용하면이 정의는 다음과 같은 방식으로 하스켈로 번역 될 수 있습니다.

class Functor f => Monoidal f where
    mcat :: f a -> f b -> f (a,b)
    munit :: f ()

Applicative 클래스는이 Monoidal 클래스와 동등하므로 다음과 같이 구현할 수 있습니다.

instance Monoidal f => Applicative f where
    pure x = fmap (const x) munit
    f <*> fa = (\(f, a) -> f a) <$> (mcat f fa)