Haskell Language
유형 대수

대수 형태의 자연수

우리는 하스켈 유형과 자연수 사이의 연결을 그릴 수 있습니다. 이 연결은 모든 유형의 거주자 수를 할당 할 수 있습니다.

유한 조합 유형

유한 타입의 경우 생성자의 수를 기준으로 모든 숫자에 자연 유형을 할당 할 수 있음을 알면 충분합니다. 예 :

type Color = Red | Yellow | Green

3 이 될 것입니다. Bool 타입은 2 입니다.

type Bool = True | False

동형 이성에 대한 독창성

우리는 여러 유형이 하나의 숫자에 해당하는 것을 보았습니다. 그러나이 경우에는 동형이됩니다. 이것은 두 개의 유형을 연결하는 정체성을 가진 한 쌍의 변이 f 와 g 가있을 것이라고합니다.

f :: a -> b
g :: b -> a

f . g == id == g . f

이 경우 유형이 동형 이라고 말할 수 있습니다. 우리는 동형 인 한 우리의 대수에서 두 종류의 동등한 것을 고려할 것입니다.

예를 들어, 2 번 표현의 두 가지 다른 표현은 사소한 동형이다.

type Bit  = I    | O
type Bool = True | False

bitValue :: Bit -> Bool
bitValue I = True
bitValue O = False

booleanBit :: Bool -> Bit
booleanBit True  = I
booleanBit False = O

왜냐하면 우리는 bitValue . booleanBit == id == booleanBit . bitValue 를 볼 수 있기 bitValue . booleanBit == id == booleanBit . bitValue

1과 0

숫자 1 의 표현은 분명히 생성자가 하나 뿐인 유형입니다. Haskell에서,이 유형은 표준 적으로 unit () 이라고 불리는 type () 입니다. 하나의 생성자 만 가진 다른 모든 유형은 () 과 동형입니다.

그리고 0의 우리의 표현은 생성자가없는 유형이 될 것입니다. 이것은 Haskell의 Void 타입으로, Data.Void 정의되어 Data.Void . 이는 데이터 생성자가없는 무인 유형과 동일합니다.

data Void

덧셈과 곱셈

더하기 및 곱셈은이 유형 대수에서 등가물을가집니다. 태그가 지정된 유니온 및 제품 유형에 해당합니다 .

data Sum a b = A a | B b
data Prod a b = Prod a b

우리는 모든 유형의 주민들이 어떻게 대수 연산에 해당 하는지를 볼 수 있습니다.

동등하게, 우리는 덧셈과 곱셈을위한 타입 생성자로서 Either 와 (,) 를 사용할 수 있습니다. 그것들은 이전에 정의한 유형과 동형입니다.

type Sum' a b = Either a b
type Prod' a b = (a,b)

덧셈과 곱셈의 예상 결과는 동형에 이르기까지 유형 대수를 따른다. 예를 들어, 우리는 1 + 2, 2 + 1과 3 사이의 동형 이성을 볼 수 있습니다. 1 + 2 = 3 = 2 + 1이다.

data Color = Red | Green | Blue

f :: Sum () Bool -> Color
f (Left ())     = Red
f (Right True)  = Green
f (Right False) = Blue

g :: Color -> Sum () Bool
g Red   = Left ()
g Green = Right True
g Blue  = Right False

f' :: Sum Bool () -> Color
f' (Right ())   = Red
f' (Left True)  = Green
f' (Left False) = Blue

g' :: Color -> Sum Bool ()
g' Red   = Right ()
g' Green = Left True
g' Blue  = Left False

덧셈과 곱셈의 규칙

commutativity, associativity 및 distributivity의 일반적인 규칙은 다음 유형들 사이에 사소한 동형이 존재하기 때문에 유효합니다.

-- Commutativity
Sum a b           <=> Sum b a
Prod a b          <=> Prod b a
-- Associativity
Sum (Sum a b) c   <=> Sum a (Sum b c)
Prod (Prod a b) c <=> Prod a (Prod b c)
-- Distributivity
Prod a (Sum b c)  <=> Sum (Prod a b) (Prod a c)

재귀 유형

기울기

목록은 다음과 같이 정의 할 수 있습니다.

data List a = Nil | Cons a (List a) 

이것을 우리의 타입 대수로 변환한다면, 우리는

목록 (a) = 1 + a * 목록 (a)

그러나 이제는이 표현식에서 List (a)를 여러 번 대체하여 다음을 얻을 수 있습니다.

목록 (a) = 1 + a + a * a + a * a * a + a * a * a * a + ...

우리가 목록을 [] 처럼 하나의 값만 포함 할 수있는 유형으로 보는 것은 의미가 있습니다. 또는 [x] 에서와 같이 유형 a 의 모든 값; 또는 [x,y] 와 같이 유형 a 의 두 값; 등등. List의 이론적 인 정의는 다음과 같습니다.

-- Not working Haskell code!
data List a = Nil
            | One a
            | Two a a
            | Three a a a 
            ...

나무

예를 들어 이진 트리를 사용하여 동일한 작업을 수행 할 수 있습니다. 우리가 그들을 다음과 같이 정의한다면 :

data Tree a = Empty | Node a (Tree a) (Tree a)

우리는 다음과 같은 표현을 얻습니다.

트리 (a) = 1 + a * 트리 (a) * 트리 (a)

그리고 우리가 동일한 대체물을 반복해서 만들면 다음 순서를 얻게됩니다.

트리 (a) = 1 + a + 2 (a * a) +5 (a * a * a) + 14 (a * a * a * a) + ...

여기서 얻은 계수는 카탈로니아 수열에 해당하며, n 번째 카탈로니아 수는 n 노드가있는 가능한 이진수의 수입니다.

파생 상품

유형의 파생물은 한 가지 유형의 컨텍스트 유형입니다. 타입 변수를 가능한 모든 포인트에서 사라지게하고 결과를 합산하면 얻을 수있는 타입입니다.

예를 들어 트리플 유형 (a,a,a) 가져 와서 파생 할 수 있습니다.

data OneHoleContextsOfTriple = (a,a,()) | (a,(),a) | ((),a,a)

이는 파생에 대한 일반적인 정의와 일관성이 있습니다.

d / da (a * a * a) = 3 * a * a

이 주제에 대한 자세한 내용은 이 기사에서 읽을 수 있습니다.

기능들

함수는 대수학에서 지수 함수로 볼 수 있습니다. 우리가 볼 수 있듯이 우리는 형이 걸릴 경우, a n 개의 인스턴스 및 유형과 b m 인스턴스로, 타입 a -> b n 개의 인스턴스의 힘에 m있을 것이다.

예를 들어, Bool -> Bool 은 (Bool,Bool) 과 동형이며, 2 * 2 = 2²입니다.

iso1 :: (Bool -> Bool) -> (Bool,Bool)
iso1 f = (f True,f False)

iso2 :: (Bool,Bool) -> (Bool -> Bool)
iso2 (x,y) = (\p -> if p then x else y)