haskell - 하스켈 - 함수형 프로그래밍 나무 위키



하스켈 타입은 오직 하나의 함수에 의해서만 존재한다는 것을 어떻게 보여줄 수 있습니까? (1)

연속적인 미적분을 적용 할 수 있습니다.

간단한 예를 들어, a -> a 형을 사용 a -> a \x -> (\y -> y) x 와 같은 용어를 만들 수 있지만 여전히 \x -> xid 정상화됩니다. 연속적인 미적분학에서는 시스템이 "축소 가능한"증명을 만드는 것을 금지합니다.

비공식적으로 귀하의 유형은 (b -> a) -> (a -> b -> c) -> b -> c .

f: b -> a
g: a -> b -> c
x: b
--------------
Goal: c

계속할 수있는 방법이 많지 않습니다.

apply g

f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0: a
Subgoal1: b


apply f

f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0': b
Subgoal1: b


-- For both
apply x

그래서 결국 g (fx) x 가 그 유형의 유일한 주민으로 보인다.

요네다 보조 정리 접근법은 실제로 forall x 갖도록 조심해야합니다!

 (b -> a) -> (a -> b -> c) -> b -> c
 forall b a. (b -> a) -> b -> forall c. (a -> b -> c) -> c

끝까지 집중하자.

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

그것은 (a, b) 와 동형이기 때문에 전체 형은

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

가져 오기 f = Compose (Reader b) (,b)

(b -> a) -> f a ~ f b ~ b -> (b,b)

그리고 그것은 HP a = (a,a) functor를 취함으로써 독특합니다 :

b -> (b,b) ~ (() -> b) -> HP b ~ HP () ~ ()

첫 번째 접근 방식을 수정 하면 손을 물결 모양으로 조금 더 느끼지만 어떻게 든 더 직접적으로 느껴집니다 : 제한된 규칙 집합, 증명을 구성하는 방법, 생성 할 수있는 교정본은 몇 개나 있습니까?

이 대답 에서 가브리엘 곤잘레스 (Gabriel Gonzalez)는 id 가 유일하게 forall a. a -> a 거주자임을 보여주는 법을 보여줍니다 forall a. a -> a forall a. a -> a . 그렇게하기 위해 (증명의 가장 공식적인 반복에서), 그는 형식이 요 네다 보조 정리를 사용하여 () 동형임을 보여줍니다. () 에는 하나의 값만이 있으므로이 유형의 id 있어야합니다. 요약하면, 그의 증거는 다음과 같다.

Yoneda는 말합니다 :

Functor f => (forall b . (a -> b) -> f b) ~ f a

a = ()f = Identity 인 경우이 값은 다음과 같습니다.

(forall b. (() -> b) -> b) ~ ()

그리고 trivially () -> b ~ b 이후 LHS는 기본적으로 id 유형입니다.

이것은 id 잘 작동하는 약간의 "마술 트릭"처럼 느껴집니다. 좀 더 복잡한 함수 유형에 대해서도 동일한 작업을 수행하려고합니다.

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

하지만 어디서부터 시작해야할지 모르겠습니다. 나는 그것이 \fgx = g (fx) x 의해 존재한다는 것을 안다. 만약 당신이 못생긴 / undefined 것들을 무시한다면, 나는이 유형의 다른 함수가 없다고 확신한다.

나는 가브리엘의 속임수가 내가 그 유형을 선택하는 방식으로 즉시 적용될 것이라고 생각하지 않는다. 이 유형과 () 사이의 동형을 보여줄 수있는 다른 접근법 (똑같이 형식적입니다!)이 있습니까?





type-theory