Haskell에서 장르를 쫓고 있어요.

소개하다.
Haskell의 유형 추적은 함수 형식만 서명하는 함수에 대한 정의입니다.
대부분의 상황에서 매개 변수 다중 함수의 실제 정의는 서명에 의해 결정될 뿐만 아니라 유형은 실제적으로 유일하게 합리적이고 효과적인 해결 방안을 향해 나아가도록 추진할 수 있다(효과적이지만 불합리한 해결 방안이 있을 수 있다).정의된 모든 구성 부분은 서명에서 확인할 수 있으며, 이것은 보통 등식 오른쪽에 성명된 매개 변수이다.외부(예를 들어 전주곡) 기능이 필요하지 않다고 가정하면 (가장 흔히 볼 수 있는 경우) 등식 왼쪽에 정확한 정의를 쓰는 모든 필수 성분이 생긴다.너는 단지 어떤 방식으로 그것들을 결합시켜 간단한 조작 집합을 사용할 수 있다. 기능 응용, 패턴 일치 (간혹).

하나의 예
이것이 바로 내가 줄곧 정확하게 정의하지 못한 함수의 특징이다.

kapp :: (((a -> b) -> r) -> r)    -- ContT r m (a -> b)
     -> ((a -> r) -> r)           -- ContT r m a
     -> ((b -> r) -> r)           -- ContT r m b

kapp의 서명은 실제적으로 응용 프로그램(<*>) 방법의 독립된 버전으로 ContT를 포함하지 않는다. here와 같다.

-- ContT monad transformer
newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r }

-- ContT's Applicative instance
instance Applicative (ContT r m) where
  (<*>) :: ContT r m (a -> b) 
        -> ContT r m a
        -> ContT r m b
  f <*> v = ContT $ \ c -> runContT f $ \ g -> runContT v (c . g)

이 해결 방안, 즉 그들이 <*>에 대한 정의를 보고 나는 그들이 거기에 lambda(c 파라미터가 있는 lambda)를 도입한 것을 알았지만 끝에 가까운 곳에서 그것을 응용한 것은 매우 낙담스러웠다.또 다른 lambda (g 파라미터가 있습니다.그 밖에 합성c . g은 세 번째 lambda를 의미하는데 그 중에서 은식 파라미터(x를 성명하여 합성점을 완전하게 한다:c (g x).
바로 이런 lambda의 소개는 명제 논리에서의 추리 규칙을 떠올리게 했다. 함축된 규칙을 도입하여 호화드의 방향으로 나아가게 했다.

논리적 유도
인용론을 포함하는 추리 규칙은 만약에 당신이 ap를 가설하고 자신의 방식으로 aq를 얻어낸다면 당신은 결론을 얻을 수 있다p => q.우리는 의미를 도입한 예를 제시하지 않고 주어진 문제로 돌아가서 그곳에서 시범을 보이는 것이 가장 좋다.

kapp :: (((a -> b) -> r) -> r)    -- h
     -> ((a -> r) -> r)           -- k
     -> (b -> r)                  -- g
     -> r
kapp h k g = -- how now brown cow?

요약:

우리는 3개의 함수 매개 변수를 매개 변수h에 귀속시켰다k,g

h :: ((a -> b) -> r) -> r

k :: (a -> r) -> r

g :: b -> r

생산이 필요합니다.

r형

이 세 가지 논점은 세 가지 주어진 명제이므로 우리는 결론을 얻어야 한다r.이 함수의 형식은 명예 스타일로 전환하는 증명 유도에 적합하다. 왜냐하면 그것을 해결하는 데 필요한 모든 것이 이미 존재하기 때문이다. 즉, (해결 방안을 엿보기) 우리는 임의의 (전주) 함수와 관련이 없고, 해결 방안에 필요한 모든 것이 표지부의 형식으로 제공되기 때문에, 우리는 어떤 방식으로 그것들을 다시 배열하기만 하면 된다.관련된 유형은 함수 유형이기 때문에 그것들은 직접적으로 의미로 바뀐다.
명예 스타일맵:

┌──┬──────────────────────┬────────────────────────┐
│1 │ ((a -> b) -> r) -> r │ proposition            │
│2 │ (a -> r) -> r        │ proposition            │
│3 │ b -> r               │ proposition            │
╞══╪══════════════════════╪════════════════════════╡
│4 │ ┌ (a -> b)¹          │ assumption¹            │
│5 │ │ ┌ a²               │ assumption²            │
│6 │ │ │ b                │ MP 4,5                 │
│7 │ │ │ r                │ MP 3,6                 │
│8 │ │ a² -> r            │ ->I 5-7 (discharging²) │
│9 │ │ r                  │ MP 2,8                 │
│10│ (a -> b)¹ -> r       │ ->I 4-9 (discharging¹) │
│11│ r                    │ MP 1,10                │
└──┴──────────────────────┴────────────────────────┘

우리는 결론을 얻어야 한다r.1-3행을 제시했다.그러니까 우리 4행부터 해결하자.

가정(a -> b)

우리는 또 다른 가설을 한다a

(a -> b)(4)와a(5)가 있다면 b

방식: (b -> r)(3)과b(6)로 결론을 내렸습니다r

가설 해제 2, 우리는 (a -> r)

방식: (a -> r) -> r(2)와(a -> r)(8), 생산r

가설 해제 1, 획득((a -> b) -> r)

방식: ((a -> b) -> r) -> r(1) 및 이상(10) 제시r

이것r이 바로 우리가 찾은 결론이다.QED.
나는 함수 정의의 실현을 일련의 강제 절차로 압축하기 위해 이런 파생 형식이 더 많은 정보를 제시할 수 있기를 바란다.그러나 어쨌든, 당신이 등식에 빠졌을 때, 그것은 유용한 도움인 것 같다.
유도할 때, 너는 어떤 것도 가설할 수 있다.모든 가설은 오른쪽으로 한 단계 축소되어 이 가설과 같은 등급의 주어진 명제와 공식만 사용할 수 있음을 알립니다.그 밖에 가설을 해제해야 한다는 것을 일깨워 주었다.
특정한 가설을 이행할 때 한 줄에 쓴 형식은 항상 같다. 먼저 이 가설을 쓴 다음에 은밀한 기호를 쓴 다음에 앞줄에 쓴 공식(은밀한 인용문 바로 위의 그 줄)을 쓴다.제시한 이유를 의미소개, 줄임말->I, 그리고 그 범위를 나타내는 범위라고 한다.
함축 해소 또는 ->E 또는 MP(modus ponens)는 함수 응용에 해당한다. 함축 하나a -> b와 하나a가 있으면 하나b를 얻을 수 있다a.

함수 실현으로 돌아가기

kapp :: (((a -> b) -> r) -> r)    -- h
     -> ((a -> r) -> r)           -- k
     -> (b -> r)                  -- g
     -> r
kapp h k g = h (\f -> k (\x -> g (f x)))
-- i.e.
kapp h k g = h \f -> k \x -> g $ f x
kapp h k g = h \f -> k (g . f)

코드 참조가 있는 파생:

4 │ ┌(a -> b)¹     assumption¹            . a -> b      :: f
5 │ │ ┌a²          assumption²            . . a         :: x
6 │ │ │b           MP 4,5                 . . b         :: f x
7 │ │ │r           MP 3,6                 . . r         :: g (f x)
8 │ │ a² -> r      ->I 5-7 (discharging²) . a -> r      :: c
9 │ │ r            MP 2,8                 . r           :: k c
10│(a -> b)¹ -> r  ->I 4-9 (discharging¹) (a -> b) -> r :: d
11│r               MP 1,10                r             :: h d

처음에는 잘 알지 못했을 수도 있지만, 몇몇 연습을 통해 많은 함수들이 배후의 절차를 실현하는 것이 더욱 쉽게 증명되었다.
(응, 첫 번째 가설이 a라면?)

kapp :: (((a -> b) -> r) -> r)
     -> ((a -> r) -> r)
     -> (b -> r)
     -> r

kapp h k g = h $ \f -> k $ \a -> g $ f a
-- vs
kapp h k g = k $ \a -> h $ \f -> g $ f a

같은 서명, 다른 유도

┌──┬──────────────────────┬────────────────────────┐
│1 │ ((a -> b) -> r) -> r │ proposition            │
│2 │ (a -> r) -> r        │ proposition            │
│3 │ b -> r               │ proposition            │
╞══╪══════════════════════╪════════════════════════╡
│4 │ ┌ a¹                 │ assumption¹            │
│5 │ │ ┌ (a -> b)²        │ assumption²            │
│6 │ │ │ b                │ MP 5,4                 │
│7 │ │ │ r                │ MP 3,6                 │
│8 │ │ (a -> b)² -> r     │ ->I 5-7 (discharging²) │
│9 │ │ r                  │ MP 1,8                 │
│10│ a¹ -> r              │ ->I 4-9 (discharging¹) │
│11│ r                    │ MP 2,10                │
└──┴──────────────────────┴────────────────────────┘

kapp h k g = k $ \a -> h $ \f -> g $ f a

첫 번째와 달리 이 파생은 코드의 실현과 일치한다. 그림과 코드에서 a -> b는 첫 번째 것으로 가정되고 kapp는 두 번째 것으로 가정되기 때문이다.그런데 뭔가 문제가 생겼을 거야(!?)

매핑 지속
현재 상기 두 가지 애매모호한 fmap 실현 (진행 중인 조사에 방해가 되지 않도록) 을 논의하지 않고, 먼저 소개해야 할 것 kmap 과 유사하지만 kmap 으로 이름이 바뀐 독립 함수를 실현함으로써 하나의 연장을 비추는 것을 살펴보자.k의 서명은 쉽게 이해할 수 있다. 함수a에 전달된 리셋이 함수에 전달된 리셋 값f과 전달a에 적용되는 리셋 함수k.따라서 함수의 원시 반환값은continuation에 전달되고 비추기 전에 포획된다.

제1판
이전과 마찬가지로, 아래의 서명은 오른쪽에 있는 추가 괄호를 삭제해서 간소화할 수 있기 때문에, 우리는 3개의 정확한 매개 변수를 얻을 수 있다.실제로 우리가 방정식의 LHS에서 3개의 파라미터를 성명하든지, RHS에서 lambda로 모든 파라미터를 포착하든지, 아니면 둘 사이의 어떠한 분포든지 모두 등가이다.그러나 k의 첫 번째 버전에 대해 모든 3개 파라미터는 해당하는 프로퍼, 즉 LHS가 성명한 파라미터가 있을 것이다.

-- v.1
kmap :: (a -> b) -> ((a -> r) -> r) -> (b -> r) -> r
-- just to make it more readable
kmap :: (a -> b)            -- f
     -> ((a -> r) -> r)     -- k
     -> (b -> r)            -- g
     -> r
kmap f k g = k $ \a -> g (f a)

해당 혜택 차트에 따라 다음과 같은 작업을 원활하게 수행할 수 있습니다.

a -> b, (a -> r) -> r, b -> r ⊢ r

1 │ a -> b          proposition            | f
2 │ (a -> r) -> r   proposition            | k
3 │ b -> r          proposition            | g
--|----------------------------------------|------------------
4 │ ┌ a¹            assumption¹            | \a -> (
5 │ │ b             MP 1,4                 |   f a
6 │ │ r             MP 3,5                 |   g (f a)
7 │ (a¹ -> r)       =>I 4-6 (discharging¹) | )
8 │ r               MP 2,7                 | k $ \a -> g (f a)

제2판kmap의 또 다른 버전이지만 이번에 세 번째 파라미터는 LHS에 해당하는 파라미터가 없고 추가적인 lambda를 도입함으로써 그것을 제약한다.new type에 포장된continuations (및 기타 유형) 를 처리할 때, 보통 이런 상황이 발생한다. 데이터 구조 함수가 방해가 되기 때문에, lambda를 도입하여 그것을 처리하도록 강요한다. (보통 마지막, 보통 세 번째 인자)또는 사용자가 정의한 함수에 접미사를 붙이는 것을 더 좋아하기 때문일 수도 있습니다. 이 경우 LHS의 2개 파라미터가 (예: kmap 보다 f 'kmap' k = \g -> … 정확합니다.
현재 우리는 3개가 아니라 2개의 전제가 있기 때문에 우리가 찾는 것은 kmap f k g = …이 아니라 r이다.그러나 이렇게 하는 모든 효과는 다른 가설을 도입한 것이다. 이것은 추가 lambda(그 주체는 첫 번째 버전을 봉인하는 실현)를 도입한 것을 의미한다. 아래와 같다.

a -> b, (a -> r) -> r ⊢ (b -> r) -> r

1 │ a -> b          proposition            | f
2 │ (a -> r) -> r   proposition            | k
--|----------------------------------------|--------------------
3 │ ┌ (b -> r)¹     assumption¹            | \g -> (
4 │ │ ┌ a²          assumption²            |   \a -> (
5 │ │ │ b           MP 1,4                 |        f a
6 │ │ │ r           MP 3,5                 |     g (f a)
7 │ │ (a² -> r)     =>I 4-6 (discharging²) |   )
8 │ │ r             MP 2,7                 |   k $ \a -> g (f a)
9 | (b -> r)¹ -> r  =>I 3-8 (discharging¹) | )

이제 그림이 다음과 같이 변환됩니다.

-- v.2
kmap :: (a -> b) -> ((a -> r) -> r) -> ((b -> r) -> r)
-- making the dig more readable
kmap :: (a -> b)            -- f
     -> ((a -> r) -> r)     -- k
     -> ((b -> r) -> r)
kmap f k = \g -> (k $ \a -> g (f a))

링크 지속
이 세 가지 절차를 완성하기 위해서, 다음은continuations를 연결하는 (b -> r) -> r 클래스 함수의 정의입니다.

kbind :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r)
-- rearranged sig
kbind :: ((a -> r) -> r)
      -> (a -> ((b -> r) -> r))
      -> ((b -> r) -> r)

-- removing redundant parens
kbind :: ((a -> r) -> r)        -- k
      -> (a -> (b -> r) -> r)   -- h
      -> b -> r                 -- g
      -> r
kbind k h g = k \a -> (h a g)

이 실현 과정은 그림에서 순조롭게 완성되었다.

(a -> r) -> r, a -> (b -> r) -> r, b -> r ⊢ r

1 | (a -> r) -> r        proposition    | k
2 | a -> (b -> r) -> r   proposition    | h
3 | b -> r               proposition    | g
--|-------------------------------------|-----------------
4 | ┌ a¹                 assumption¹    | \a -> (
5 | │ (b -> r) -> r      MP 2,4         |    h a
6 | │ r                  MP 5,3         |   (h a) g
7 | a¹ -> r              =>I 4-6 (dis¹) | )
8 | r                    MP 1,7         | k (\a -> h a g)