2017-05-14

私のためのHaskell〜ひたすら原点回帰〜その４　Haskellで大きな仕事をする[], Functor, Monad は * -> *

Haskell 演算数学

意識される対象は、要素それ自体だったり、要素の連なりそれ自体だったりしたし
要素の集合を意識して、それを型と呼んだりした
関数は不特定の要素に定めた処理ルールであったが
そのときの不特定要素というのは、型集合の要素であった
型そのものを要素として考えるとすると、型を要素とする集合(型集合)を考え、不特定の型に定めたルールが生じる
不特定の型を*と表した時、それは、*, * -> * , * -> * -> * …となる
その１例がリストという型だと、前の記事で書いた
リスト、というのは、確かに型だが
- Intのリスト、Floatのリスト、Charのリスト、「Intのリスト」のリスト…のように、「何かしらの-リスト」という型である。そして「何かしらの-」は、型であって、入れ子になった複雑なものであってもよい
- :infoを使えば、Eq型クラスに属する型の、Ord型クラスに属する方のなどがあることがわかる
- data a の、と aとが左辺にあるので、 *　が２つ、ということである。

Prelude Control.Arrow> :info []
data [] a = [] | a : [a]        -- Defined in ‘GHC.Types’
instance Eq a => Eq [a] -- Defined in ‘GHC.Classes’
instance Ord a => Ord [a] -- Defined in ‘GHC.Classes’
instance Read a => Read [a] -- Defined in ‘GHC.Read’
instance Show a => Show [a] -- Defined in ‘GHC.Show’

- 他に「何かしらの-○○」というものがあるか、というと、Functor型クラスには、MaybeのFunctor、[]リストのFunctor…というものがある
  - ここで、リストが　* -> * なる「型」であって、[1.0]が「Float型のリストという型」であったのに対して、Functor型クラスが「型クラス」と呼ばれ、MaybeのFunctorが、* -> * なる「型」である、という、この違いは、(たぶん、FunctorはClass宣言して定義され、ある関数を持つという制約を付けて作られているのに対して、リストの方は、dataで宣言され、その制約は　[] | a: [a] とdata 宣言のみでまかなわれている点が違うのだろう。
  - ちなみに、型クラス宣言、その遵守関数制約があることが、(* -> *) -> Constraint という表記の、「制約されているよ」という表示にも反映しているようだ
  - また、このように型変数を使い、その型変数で守るべき関数制約を定めた「型」は「型変数」に何を取るかで変わってくるから、「型クラス」と呼ばれる。あまた定義される/定義可能な型の部分集合を指すものである
  - 以下に見えるように。

Prelude Control.Arrow> :kind Functor
Functor :: (* -> *) -> Constraint
Prelude Control.Arrow> :info Functor
class Functor (f :: * -> *) where
instance Functor Maybe -- Defined in ‘Data.Maybe’
instance Functor [] -- Defined in ‘GHC.Base’
instance Functor IO -- Defined in ‘GHC.Base’
instance Functor ((->) r) -- Defined in ‘GHC.Base’
instance Functor ((,) a) -- Defined in ‘GHC.Base’

- Hakellではこの型変数を１つだけとって作る型がGHC.Baseモジュールなどで定義されている
- このようにHaskellの仕様では　* -> * , (* -> *) -> Constraint な型を作ることは、「元来」できるわけだが、GHC.Baseを作り、取り込むことによって初めて「使える」ようになることもわかる
- 逆に言えば、Haskellがその仕様を駆使してできることの一部が、使いやすい形で型・型クラス化しているだけだ、ということでもある
* -> * 的な型として定義可能な型は、型引数にとる型の場合分け、制約関数の取り方のバリエーションから、非常に多くなり得ていて、「とても有用な型・型クラス」がまだ見出されていない可能性もあるのだろう
また、 * -> * は「入れ子」にできるので、引数としてとる型が ( * -> * ) であるようにすれば、複雑にできる
そのような例がStateMonadである
- 以下にあるように、* -> (* -> *) -> Constraint である。これは ( * -> ● ) を守っているが、●が ( * -> * )であるということから、入れ子の　( * -> * )である
- 実際、

Prelude Control.Arrow Control.Category Control.Monad.State> :kind MonadState
MonadState :: * -> (* -> *) -> Constraint

Prelude Control.Arrow Control.Category> import Control.Monad.State
Prelude Control.Arrow Control.Category Control.Monad.State> :info MonadState
class Monad m => MonadState s (m :: * -> *) | m -> s where
  get :: m s
  put :: s -> m ()
  state :: (s -> (a, s)) -> m a
        -- Defined in ‘Control.Monad.State.Class’
instance Monad m => MonadState s (StateT s m)
  -- Defined in ‘Control.Monad.State.Class’

さらに、* -> * -> * にへと拡張できることも想像がつく
- 以下にその例を示す。Category型クラス、Arrow型クラスなどがある

Prelude Control.Arrow> :kind Arrow
Arrow :: (* -> * -> *) -> Constraint
Prelude Control.Arrow> :info Arrow
class Control.Category.Category a => Arrow (a :: * -> * -> *) where
  arr :: (b -> c) -> a b c
  first :: a b c -> a (b, d) (c, d)
  second :: a b c -> a (d, b) (d, c)
  (***) :: a b c -> a b' c' -> a (b, b') (c, c')
  (&&&) :: a b c -> a b c' -> a b (c, c')
        -- Defined in ‘Control.Arrow’
instance Monad m => Arrow (Kleisli m) -- Defined in ‘Control.Arrow’
instance Arrow (->) -- Defined in ‘Control.Arrow’
Prelude Control.Arrow> import Control.Category
Prelude Control.Arrow Control.Category> :kind Category
Category :: (k -> k -> *) -> Constraint

さらに拡張できるだろうか？
- ここまで、値があったときにそれを値変数にして、関数を作った。値と関数とが入れ子構造になった。値と値コンストラクタとが入れ子構造になって、統一的にとらえられた。
- ついで、型の集合を考えて、型変数を使うことにより、型の入れ子構造を作った。型と型コンストラクタとが入れ子世界になったということでもある。
- 値とその入れ子→型とその入れ子→「型とその入れ子」の塊を「超型」とすることができる
  - そこに、「超型」の変数：「超型変数」を作り、超型と超型コンストラクタとの入れ子世界
- さらに「超超…」
そして、この「超」を一段ずつ登って行くのも、かったるいので、これ全体を包んだ概念を入れて…とするのも、数学としてはお手の物のはず。
有限群の中にモンスターが居たような感じで、この中にも「とても有用なものが隠れている」とか、その「有用なもの探しはとても探索空間が広いので、遺伝的プログラミングが向いていたから、生物がどこかにみつけて利用していかも」とか、そんな風に考えるのも面白いかもしれません。