私のためのHaskell〜ひたすら原点回帰〜その１　値、演算、型

まだすらすらコードは書けないけれど、Haskellが実装しようとしていることと、それがどれくらいの徹底度で実装が進んできているのかのイメージはつかめた。
イントロ
- Haskellは(関数型言語として)、こういうことがやりたい、という『何か』のためにある
- 『何か』とは『値と演算』
- それをどう実現するかを「実装してみた」１形態がHaskell。なので、『こうやりたい』のすべてが実装されているわけでもないし、『理念に沿ってこう実装するのがよい』という理念通りに実装されているわけでもない
- また、そのHaskellの『実装』は、考え方としての実装だが、それをどのように書き表すか、書き表した情報をどのように文字列として見せるか、という部分はHaskellの『気持ち』とは別(である部分もある)
さて。原点回帰。
- 原点から始めるけれど、Monadも現れるはずだし、さらにその先のArrowとかも現れるはず。逆に言うと、MonadとかArrowとかは「やりたい何か」から生じる世界のある一部分を亜集合として取り出したものであって、『こうやりたい』の中で実装されている一部に過ぎない。けれど、どうしてMonadがHaskellで前面に出ているか、といえば、「現在のHaskell」ではMonadを使ってプログラムをするのが主流だから(もしくは、現在のプログラムというのが、Monadが持つ機能で実現可能な実体だから)
値と演算
- 値を次のように決める
  - 「もの」でも「こと」でも何でもよし。とにかく、「それ」と指し示せる対象、意識できる何か
- 演算を次のように決める
  - 0個以上の値を取って0個以上の値を返すこと
- ただし、「演算」も「それ」と指し示せる対象、意識できる何か、なので、「演算」もある種の「値」であるとする
- ただし、0個の値を取る「演算」を「演算機能のない値」であるとみなせば、すべての「値」はある種の「演算」であることになる
- 結局、「値・演算」を同一視して次のように決める
  - 「もの」でも「こと」でも何でもよし。とにかく、「それ」と指し示せる対象、意識できる何か、のことを「値・演算」と呼び、「値・演算」は0個以上の「値・演算」取って、0個以上の「値・演算」を返すもの
  - ただし、「何かを取る」「何かを返す」という「意識の対象」は「値・演算」なのかどうか？「0個を取って、0個を返す」というのは、「取りもしなければ返しもしない」ので、「取る・返す」を意識しなくてもよい、とし、「取る」「返す」のいずれかが１個以上になると、「aを取るもの」「aを返すもの」という対象になる
簡単なところからやってみる
「値・演算」を「あ」と呼ぶことにする
- 「あ」が0個ある世界
  - ここは意識対象がない世界。無意識の世界。空集合もない世界
- 「あ」が1個ある世界
  - 1個の「あ」を取ったり返したりすることはできない。なぜなら「…を1個取る」のは「…」とは異なるが、今、「あ」は1個しかないから。
  - HaskellでPreludeも使わず、GHCの最小構成でやってみる

ghci -XNoImplicitPrelude

- - １個の「あ」として"a"を定義した。Haskellでは"a"単独では存在しえなくて、"a"は"A"という型をもち、"A"という型は要素として"a"しかない、と定義される。この"a"は型Aの唯一の要素である"A"という値を取る、ということが "a = A"という式からわかる。"A"は型IDであり、型Aの値コンストラクタである。"data A = A"の左辺の"A"は型ID、右辺の"A"は値コンストラクタ
  - "a"には型があり、:type問い合わせで調べられる。"A"にはkindがあり、:kind問い合わせで調べられる。"A"のkindは、値を受け取ったり返したりしない、存在そのものなので "*"となっている。"* -> *" というkindなども後で出てくる
  - もちろん、"a"は引数を取れないから(a a) にはタイプもなくエラーになる

data A = A
let a :: A; a = A
:type a
:kind A
:type (a a)

> data A = A
> let a :: A; a = A
> :type a
a :: A
> :kind A
A :: *
> :type (a a)

<interactive>:1:2:
    Couldn't match expected type ‘A -> t’ with actual type ‘A’
    The function ‘a’ is applied to one argument,
    but its type ‘A’ has none
    In the expression: (a a)

- - こうもできる。この場合、"a"は型Aであり、0個の引数を取って、自身を返す関数、とも読める。自身を返す(0とって1返す)は、自身に値を持つ、ということと「違う」定義の仕方に相当するが、「同じ」ようにHaskellでは取り扱われる、ということに相当するのだろう

data A = A
let a :: A; a = a
:type a
:kind A

- 「あ」が2個ある
  - 1個から2個に増やすパターンは複数ある
  - (1) 型の数は１つ。型が持つ値も１つ。実体として同一のものが２つ。

data A = A
let a1 :: A; a1 = A
let a2 :: A; a2 = A
:type a1
:type a2

> data A = A
> let a1 :: A; a1 = A
> let a2 :: A; a2 = A
> :type a1
a1 :: A
> :type a2
a2 :: A

- - (2) 型の数は１つ。型が持つ値は２つ。実体として異なる値を持つものが１つずつ

data A = A1 | A2
let a1 :: A; a1 = A1
let a2 :: A; a2 = A2
:type a1
:type a2

> data A = A1 | A2
> let a1 :: A; a1 = A1
> let a2 :: A; a2 = A2
> :type a1
a1 :: A
> :type a2
a2 :: A

- - (3) 型の数は2つ。型が持つ値はそれぞれ１つずつ。実体として異なる型に属するものが１つずつ。２つの型は無関係

data A = A
data B = B
let a = A
let b = B

- - (4) 型の数は2つ。型が持つ値はそれぞれ１つずつ。実体として異なる型に属するものが１つずつ。第２の型は第１の型を１つとって、第１の型を１つ返すような型
    - A -> A なる型には「ID・呼び名」はついていないが、そういうものが「A -> A」型として存在している
    - a, b a, b (b a), b (b (b a))と表記は変わるが、それらが実体としては、A型であることは、:kindの結果が同じこととして示される
    - aに複数回bを適用して

data A = A
let a :: A; a = A
let b :: A -> A; b = \ x -> x
:type a
:type b
:type b a
:type b ( b a )
:kind A
:kind A -> A
:kind A -> A -> A

> data A = A
> let a :: A; a = A
> let b :: A -> A; b = \ x -> x
> :type a
a :: A
> :type b
b :: A -> A
> :type b a
b a :: A
> :type b ( b a )
b ( b a ) :: A
> :kind A
A :: *
> :kind A -> A
A -> A :: *
> :kind A -> A -> A
A -> A -> A :: *

- 型の数は2つ。型が持つ値はそれぞれ１つずつ。実体として異なる型に属するものが１つずつ。第２の型は第１の型を２つとってもよく、第１の型を１つ返すような型
  - こうなると、第１の型があって、それをn個とって第１の型を返すような関数が定義されても、同様にうまく行く

data A = A
let a :: A; a = A
let b :: A -> A -> A; b = \ x _ -> x
:type a
:type b
:type b a
:type b a a
:type b (b a a)
:type b (b a a) a

> data A = A
> let a :: A; a = A
> let b :: A -> A -> A; b = \ x _ -> x
> :type a
a :: A
> :type b
b :: A -> A -> A
> :type b a
b a :: A -> A
> :type b a a
b a a :: A
> :type b (b a a)
b (b a a) :: A -> A
> :type b (b a a) a
b (b a a) a :: A

- - 自然な発想として、第１の型があって、それを0個、1個、2個…、任意個とって第１の型を返すような世界も作りたくなる
一般化して考える
群
- 集合と、その集合に二項演算が一つ定義されているとき、一定の条件を満たすと群と呼ばれる
- 「あ」としては、２つの型の集まりとなる。片方の型は演算で、もう片方の型が値集合である。値集合は１個かもしれないし、無限個かもしれない
  - 整数を使いたいのでPrelude付きでGHCiを起動して型と演算を定義する

type A = Int
let b :: A -> A -> A; b = \ x y -> x * y

「あ」に２種類あって、片方の種類は要素の集合、もう片方の種類はその要素を取ってその要素を返す演算という場合のうち、要素の数がいろいろで演算の数が一つのものを考えた
「あ」の２種類がそれぞれ、型であって、２つの型の間に関係がないときは静的。関係を入れるためにはその演算に対応する第３の種類を定義する必要がある
複数の要素集合と、その間を行き来する演算とがある場合

data A = A1 | A2
data B = B1 | B2
let c :: A -> B; c = \ _ -> B1
let a1 = A1
let a2 = A2
let b1 = B1
let b2 = B2
:type c
:type c a1

Prelude> data A = A1 | A2
Prelude> data B = B1 | B2
Prelude> let c :: A -> B; c = \ _ -> B1
Prelude> let a1 = A1
Prelude> let a2 = A2
Prelude> let b1 = B1
Prelude> let b2 = B2
Prelude> :type c
c :: A -> B
Prelude> :type c a1
c a1 :: B

まとめてみる
- 「値・演算」を「あ」にまとめる
- 「演算」がないと「静的」、あると「動的」になる
- １つの型の値の集合の中で閉じた演算と、型を横断する演算とがある