동형 함수의 중요성

동형 함수의 중요성

---

짧은 질문 : 프로그래밍 (즉, 함수형 프로그래밍)에서 동형 함수의 중요성은 무엇입니까?

긴 질문 : 나는 때때로 듣는 용어의 일부를 기반으로 범주 이론에서 함수형 프로그래밍과 개념 사이의 유사점을 그리려고합니다. 본질적으로 나는 그 용어를 내가 확장 할 수있는 구체적인 무언가로 "패키지 해제"하려고합니다. 그런 다음 내가 무슨 말을하는지 이해하면서이 용어를 사용할 수있을 것입니다. 항상 좋습니다.

내가 항상 듣는이 용어 중 하나는 Isomorphism입니다 . 저는 이것이 기능 또는 기능 구성 간의 동등성에 대한 추론에 관한 것이라고 생각합니다. 나는 누군가가 isomorphism의 속성이 (함수 프로그래밍에서) 유용한 일반적인 패턴과 동형 함수에 대한 추론에서 얻은 컴파일러 최적화와 같은 부산물에 대한 통찰력을 제공 할 수 있는지 궁금합니다.

---

동형의 범주 이론 정의가 객체에 대해 아무것도 말하지 않기 때문에 동형에 대한 찬성 답변에 약간의 문제가 있습니다. 이유를 알아보기 위해 정의를 검토해 보겠습니다.

정의

동형은 한 쌍의 형태 (즉, 함수) f이며 g, 다음과 같습니다.

f . g = id
g . f = id

이러한 형태를 "이소"형태라고합니다. 많은 사람들이 동 형사상에서 "모피 즘"이 객체가 아니라 기능을 의미한다는 것을 이해하지 못합니다. 그러나 그들이 연결하는 객체는 "동형"이라고 말하고 다른 대답이 설명하는 것입니다.

동 형사상 정의는 ( .) id,, 또는 =되어야 하는 것을 말하지 않습니다 . 유일한 요구 사항은 그것이 무엇이든간에 카테고리 법률을 충족한다는 것입니다.

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

컴포지션 (즉 ( .))은 두 가지 형태를 하나의 형태로 결합 id하고 일종의 "정체성"전환을 나타냅니다. 이것은 우리의 동형이 정체성 형태로 상쇄된다면 id서로의 역으로 ​​생각할 수 있음을 의미합니다 .

형태가 함수 인 특정 경우에 id대해 식별 함수로 정의됩니다.

id x = x

... 구성은 다음과 같이 정의됩니다.

(f . g) x = f (g x)

... 그리고 두 함수는 id구성 할 때 항등 함수로 취소되는 경우 동형 입니다.

모피 즘 대 객체

그러나 두 개체가 동형이 될 수있는 여러 가지 방법이 있습니다. 예를 들어 다음 두 가지 유형이 주어집니다.

data T1 = A | B
data T2 = C | D

그들 사이에는 두 가지 동형이 있습니다.

f1 t1 = case t1 of
    A -> C
    B -> D
g1 t2 = case t2 of
    C -> A
    D -> B

(f1 . g1) t2 = case t2 of
    C -> C
    D -> D
(f1 . g1) t2 = t2
f1 . g1 = id :: T2 -> T2

(g1 . f1) t1 = case t1 of
    A -> A
    B -> B
(g1 . f1) t1 = t1
g1 . f1 = id :: T1 -> T1

f2 t1 = case t1 of
    A -> D
    B -> C
g2 t2 = case t2 of
    C -> B
    D -> A

f2 . g2 = id :: T2 -> T2
g2 . f2 = id :: T1 -> T1

따라서 동 형사상 법칙을 충족하는 두 개체 사이에 고유 한 함수 쌍이 반드시있을 필요는 없기 때문에 두 개체보다는 두 개체와 관련된 특정 기능의 관점에서 동 형사상을 설명하는 것이 더 좋습니다.

또한 기능을 반전 할 수있는 것만으로는 충분하지 않습니다. 예를 들어 다음 함수 쌍은 동형이 아닙니다.

f1 . g2 :: T2 -> T2
f2 . g1 :: T2 -> T2

를 작성할 때 정보가 손실 f1 . g2되지 않더라도 최종 상태의 유형이 동일하더라도 원래 상태로 돌아 가지 않습니다.

또한 동형이 구체적인 데이터 유형 사이에있을 필요는 없습니다. 여기에 두 개의 정규 isomorphisms의 예 콘크리트 대수 데이터 유형 사이되지 않습니다 그리고 대신에 단순히 기능을 관련 : curry및 uncurry:

curry . uncurry = id :: (a -> b -> c) -> (a -> b -> c)
uncurry . curry = id :: ((a, b) -> c) -> ((a, b) -> c)

Isomorphisms에 대한 용도

교회 인코딩

동형의 한 가지 용도는 데이터 유형을 함수로 교회 인코딩하는 것입니다. 예를 들어 Bool는 다음과 같은 동형입니다 forall a . a -> a -> a.

f :: Bool -> (forall a . a -> a -> a)
f True  = \a b -> a
f False = \a b -> b

g :: (forall a . a -> a -> a) -> Bool
g b = b True False

을 확인 f . g = id하고 g . f = id.

Church 인코딩 데이터 유형의 이점은 때때로 더 빠르게 실행되고 (Church 인코딩이 연속 전달 스타일이기 때문에) 대수 데이터 유형에 대한 언어 지원조차 전혀 제공하지 않는 언어로 구현 될 수 있다는 것입니다.

구현 번역

때로는 한 라이브러리의 일부 기능 구현을 다른 라이브러리의 구현과 비교하려고 시도합니다. 동형임을 증명할 수 있다면 똑같이 강력하다는 것을 증명할 수 있습니다. 또한 동 형사상은 한 라이브러리를 다른 라이브러리로 변환하는 방법을 설명합니다.

예를 들어, functor의 서명에서 모나드를 정의하는 기능을 제공하는 두 가지 접근 방식이 있습니다. 하나는 free패키지 에서 제공하는 무료 모나드이고 다른 하나는 operational패키지 에서 제공하는 작동 의미 체계 입니다.

If you look at the two core data types, they look different, especially their second constructors:

-- modified from the original to not be a monad transformer
data Program instr a where
    Lift   :: a -> Program instr a
    Bind   :: Program instr b -> (b -> Program instr a) -> Program instr a
    Instr  :: instr a -> Program instr a

data Free f r = Pure r | Free (f (Free f r))

... but they are actually isomorphic! That means that both approaches are equally powerful and any code written in one approach can be translated mechanically into the other approach using the isomorphisms.

Isomorphisms that are not functions

Also, isomorphisms are not limited to functions. They are actually defined for any Category and Haskell has lots of categories. This is why it's more useful to think in terms of morphisms rather than data types.

For example, the Lens type (from data-lens) forms a category where you can compose lenses and have an identity lens. So using our above data type, we can define two lenses that are isomorphisms:

lens1 = iso f1 g1 :: Lens T1 T2
lens2 = iso g1 f1 :: Lens T2 T1

lens1 . lens2 = id :: Lens T1 T1
lens2 . lens1 = id :: Lens T2 T2

Note that there are two isomorphisms in play. One is the isomorphism that is used to build each lens (i.e. f1 and g1) (and that's also why that construction function is called iso), and then the lenses themselves are also isomorphisms. Note that in the above formulation, the composition (.) used is not function composition but rather lens composition, and the id is not the identity function, but instead is the identity lens:

id = iso id id

Which means that if we compose our two lenses, the result should be indistinguishable from that identity lens.

---

An isomorphism u :: a -> b is a function that has an inverse, i.e. another function v :: b -> a such that the relationships

u . v = id
v . u = id

are satisfied. You say that two types are isomorphic if there is an isomorphism between them. This essentially means that you can consider them to be the same type - anything that you can do with one, you can do with the other.

Isomorphism of functions

The two function types

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

are isomorphic, since we can write

u :: ((a,b) -> c) -> a -> b -> c
u f = \x y -> f (x,y)

v :: (a -> b -> c) -> (a,b) -> c
v g = \(x,y) -> g x y

You can check that u . v and v . u are both id. In fact, the functions u and v are better known by the names curry and uncurry.

Isomorphism and Newtypes

We exploit isomorphism whenever we use a newtype declaration. For example, the underlying type of the state monad is s -> (a,s) which can be a little confusing to think about. By using a newtype declaration:

newtype State s a = State { runState :: s -> (a,s) }

we generate a new type State s a which is isomorphic to s -> (a,s) and which makes it clear when we use it, we are thinking about functions that have modifiable state. We also get a convenient constructor State and a getter runState for the new type.

Monads and Comonads

For a more advanced viewpoint, consider the isomorphism using curry and uncurry that I used above. The Reader r a type has the newtype declaration

newType Reader r a = Reader { runReader :: r -> a }

In the context of monads, a function f producing a reader therefore has the type signature

f :: a -> Reader r b

which is equivalent to

f :: a -> r -> b

which is one half of the curry/uncurry isomorphism. We can also define the CoReader r a type:

newtype CoReader r a = CoReader { runCoReader :: (a,r) }

which can be made into a comonad. There we have a function cobind, or =>> which takes a function that takes a coreader and produces a raw type:

g :: CoReader r a -> b

which is isomorphic to

g :: (a,r) -> b

But we already saw that a -> r -> b and (a,r) -> b are isomorphic, which gives us a nontrivial fact: the reader monad (with monadic bind) and the coreader comonad (with comonadic cobind) are isomorphic as well! In particular, they can both be used for the same purpose - that of providing a global environment that is threaded through every function call.

---

Think in terms of datatypes. In Haskell for example you can think of two data types to be isomorphic, if there exists a pair of functions that transform data between them in a unique way. The following three types are isomorphic to each other:

data Type1 a = Ax | Ay a
data Type2 a = Blah a | Blubb
data Maybe a = Just a | Nothing

You can think of the functions that transform between them as isomorphisms. This fits with the categorical idea of isomorphism. If between Type1 and Type2 there exist two functions f and g with f . g = g . f = id, then the two functions are isomorphisms between those two types (objects).

참고URL : https://stackoverflow.com/questions/11245183/importance-of-isomorphic-functions