curry,(&&&),(|||)の型が，指数法則と対応している

カリーハワード対応

3つの指数法則

  1. c^{\left(a\times b\right)} = \left(c^b\right)^a
  2. b^a\times c^a = \left(b\times c\right)^a
  3. c^a\times c^b = c^{\left(a+b\right)}

指数法則を数式から型に書き換える

数式 型
a^b b -> a
a+b Either a b
a\times b (a, b)

この表の通りに指数法則を書き換えると，こうなります。

  1. (a, b) -> c = a -> (b -> c)
  2. (a -> b, a -> c) = a -> (b, c)
  3. (a -> c, b -> c) = (Either a b -> c)

これらは，curry,(&&&),(|||)の型とよく似ています。

関数型
curry(a, b) -> c -> (a -> b -> c)
(&&&)(a -> b) -> (a -> c) -> (a -> (b, c))
(|||)(a -> c) -> (b -> c) -> (Either a b -> c)