정수 값을 받으면, 문자열이 된다. -- stringify :: Int -> String

(Some<Int>이거나 None)인 값을 받으면, 정수가 된다. -- unwrap_or_zero :: (Some<Int> | None) -> Int

(좌하단 점과 우상단 점) 값을 받으면, 정수가 된다. -- distance_squared :: (Pos * Pos) -> Int

함수 타입-함의, 합 타입-논리합, 곱 타입-논리곱을 대응쌍을 마주했다. 그렇다면, 부정 은 어떻게 나타낼까? P가 아니다 는 다시 말해, P이면 거짓이다 와 동치다.

우리는 타입으로 말할 때, 값이 주어짐을 참 으로 해석했다. 다시 말해, 값이 없다면(never, ⊥) 거짓 이다.

다시 말해 "정수를 0으로 나눌 수 없다" = "정수를 0으로 나눌 수 있다는 거짓이다" = "정수를 0으로 나누면, 그 결과는 없다".

⇒ div_by_zero :: Int -> ⊥; div_by_zero x = x / 0

이 진술을 좀 더 구체적으로 보완하면 커리-하워드 대응에 닿으며, 우리는 타입 체계와 명제 논리가 대응한다는 결론을 얻을 수 있다.