2017-05-14

私のためのHaskell〜ひたすら原点回帰〜その３　関数の具体的な行為と抽象的な機能

Haskell 演算数学

値を２個取って値を返すことを考える。たとえば足し算
- 2+3 = 5 は、具体的な2と3を足して5を得る。この具体的な式で表されたものを「関数の具体的な行為」と呼ぶことにする
- x+y = z は、値xと値yとを足して値zを得る、という「この関数の抽象的な機能」を表していると考える
- 次のfaはA型の引数を２つ取って、A型を返す。ただし、返すのは必ずA1という値、という関数である

data A = A1 | A2
let fa :: A -> A -> A; fa = \ x -> \ y -> A1

- このfaが定めているのは、「関数の抽象的な機能」である。変数 x yを使って定義されているから、それとわかる
では、型を引数にして、型を作ったときにはどうやっていただろうか？
- 前の記事で作った型FAは以下の通り

data A =A1 | A2
data FA = FA1 A A| FA2 A A
let fa1 :: FA; fa1 = FA1 A1 A1
let pick1st :: FA -> A; pick1st (FA1 x y)  = x

- 型FAを作るのに、「具体的な型であるA」を引数にしていた
- Aは確かに、「A型」という要素を取りまとめた抽象的なものだが、型A、型B…と、たくさんの型が集まってきて、その型の集合を考えるときには、型集合の具体的な要素にすぎなくて、data FA = FA1 A A | FA2 A A とやるのは、いちいち、「具体的な要素を使った 2 + 2, 2 * 3のような式」の羅列をしていることになる。小学校の算数のようだ。やはり中学校で習う変数にするには、「一段階、上に登る」必要がある
型変数を使って、「型の代数」をすることにする
- リスト型 [] を見る。
  - :type で調べているのは、値の入っていない空のリストという具体的なものの型であって、それは何かの型tを要素としたリスト [t] である、と示されている
  - :kind で調べているのは、[]と表記されるリスト型の特徴 (kind)である。
    - * -> * というのは、二つの型変数を使って表されることを意味している。新しい型の作成には１つの型を取り入れる、ということ
  - :info (の１行目)には、型変数 a を用いて、空のリストか、型aの要素と、型aを要素とするリストとの連結( (:)演算処理)でできるリストかのいずれかであることが示されている

Prelude Control.Arrow> :type []
[] :: [t]
Prelude Control.Arrow> :kind []
[] :: * -> *
Prelude Control.Arrow> :info []
data [] a = [] | a : [a]        -- Defined in ‘GHC.Types’

- - 自作の型Aの場合には、型を作るときに、型変数を引数でとっていないので、:kindの結果は単なる * である
  - Int型も、data Int の定義行で、型変数を引数で取ってないないので、:kindの結果は単なる * である

Prelude Control.Arrow> :kind A
A :: *
Prelude Control.Arrow> :info A
data A = A1 | A2        -- Defined at <interactive>:196:1
Prelude Control.Arrow> :kind Int
Int :: *
Prelude Control.Arrow> :info Int
data Int = GHC.Types.I# GHC.Prim.Int#   -- Defined in ‘GHC.Types’