Freer Effectsが、だいたいわかった: 11-4 DataKinds拡張

Freer Effectsが、だいたいわかった: 11-4 DataKinds拡張
==========================================================

目次
----

(0). [導入](https://qiita.com/YoshikuniJujo/items/c71644b5af1f5195cbf3)

1. [Freeモナドの概要](https://qiita.com/YoshikuniJujo/items/988ac4b69a27974154fd)
	* Freeモナドとは
	* FreeモナドでReaderモナド、Writerモナドを構成する
2. [存在型(ExistentialQuantification拡張)の解説](
	https://qiita.com/YoshikuniJujo/items/988ac4b69a27974154fd )
3. [型シノニム族(TypeFamilies拡張)の解説](https://qiita.com/YoshikuniJujo/items/17853e423c39409d8dfe)
4. [データ族(TypeFamilies拡張)の解説](https://qiita.com/YoshikuniJujo/items/b3c442d0387a35bfe860)
5. [一般化代数データ型(GADTs拡張)の解説](https://qiita.com/YoshikuniJujo/items/739a1e3abed8c602dba7)
6. [ランクN多相(RankNTypes拡張)の解説](https://qiita.com/YoshikuniJujo/items/4094b5fe5a7a33f3d1e6)
7. [FreeモナドとCoyoneda](https://qiita.com/YoshikuniJujo/items/729ad9830833eacb9d75)
	* Coyonedaを使ってみる
	* FreeモナドとCoyonedaを組み合わせる
		+ いろいろなモナドを構成する
8. [Freerモナド(Operationalモナド)でいろいろなモナドを構成する](
	https://qiita.com/YoshikuniJujo/items/686fedc92fd20ff70ab8 )
	* FreeモナドとCoyonedaをまとめて、Freerモナドとする
	* Readerモナド
	* Writerモナド
	* 状態モナド
	* エラーモナド
9. [モナドを混ぜ合わせる(閉じた型で)](
	https://qiita.com/YoshikuniJujo/items/19a6e9dada698a5ebfb6 )
	* Freerモナドで、状態モナドとエラーモナドを混ぜ合わせる
		+ 両方のモナドを一度に処理する
		+ それぞれのモナドを、それぞれに処理する
10. [存在型による拡張可能なデータ構造(Open Union)](
	https://qiita.com/YoshikuniJujo/items/8dd63c9415ccda20be28 )
11. 追加の言語拡張
	1. [ScopedTypeVariables拡張](
		https://qiita.com/YoshikuniJujo/items/103807ee6692e8c2c48b )
	2. [TypeOperators拡張](
		https://qiita.com/YoshikuniJujo/items/68af70347e61849ccea9 )
	3. [KindSignatures拡張](
		https://qiita.com/YoshikuniJujo/items/0f581acc78d2ba8e3a7c )
	4. DataKinds拡張
	5. [MultiParamTypeClasses拡張](
                https://qiita.com/YoshikuniJujo/items/165460f39f1cae751300 )
	6. FlexibleInstances拡張
	7. OVERLAPSプラグマ
12. Open Unionを型によって安全にする
13. モナドを混ぜ合わせる(開いた型で)
	* FreeモナドとOpen Unionを組み合わせる
	* 状態モナドにエラーモナドを追加する
14. Freer Effectsで、IOモナドなどの、既存のモナドを使用する
15. 関数を保管しておくデータ構造による効率化
16. いろいろなEffect
	* 関数handleRelayなどを作成する
	* NonDetについて、など

はじめに
--------

DataKinds拡張について学ぶ。

値には型がある。型には種類がある。DataKinds拡張を有効にしておくと、「値 - 型」を定義したときに、それに対応する「型 - 種類」が定義される。

と、いうわけだが、ここまで読んで「なるほど、なるほど」となったかたは、続きを読む必要はない。このあとは、具体的な例で説明していく。

### 言葉について

kindをここでは「種類」と訳した。一般的には「種」と呼ぶ。「種」よりも「種類」のほうが、日常的な言葉なので、とっつきやすいという配慮だ。

タプルでリスト
--------------

Lisperにとって、リストは連鎖したコンスだ。コンスというものは、まあだいたい2要素タプルのようなものだ。なので、LisperにとってのリストをHaskellで書くと、つぎのようになる。

```hs:tupleList0.hs
ex1 :: (Integer, (Double, (Bool, ())))
ex1 = (123, (3.14, (True, ())))
```

ついでにcarとcdrを定義しておこう。

```hs:tupleList0.hs
car :: (a, b) -> a
car = fst

cdr :: (a, b) -> b
cdr = snd
```

試してみよう。

```hs
> :load tupleList0.hs
> ex1
(123,(3.14,(True,())))
> car ex1
123
> car . cdr $ ex1
3.14
> car . cdr . cdr $ ex1
True
> cdr . cdr . cdr $ ex1
()
```

「タプルでリスト」の型をまとめる
--------------------------------

「タプルでリスト」の型に別名をつけて、ひとつにまとめたい。型の別名には「型のリスト」が必要になる。まずは「型のリスト」を作ってみよう。

```hs:tupleList.hs
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

data Nil
data a :^ b
infixr 5 :^
```

型Nilや型a :^ bは、値を持たない型だ。このような型はHaskell 98標準では許されず、Haskell 2010(または、GHCのEmptyDataDecls拡張)で使えるようになった。これらは、値の型付けには使われず、型構築子の引数として使われる。試してみる。

```hs
> :load tupleList.hs
> :set -XTypeOperators
> :kind Integer :^ Double :^ Bool :^ Nil
Integer :^ Double :^ Bool :^ Nil :: *
```

これで、型のリストができた。これを引数とする型シノニムTupleListを定義する。

```hs:tupleList.hs
type family TupleList a where
        TupleList Nil = ()
        TupleList (a :^ b) = (a, TupleList b)
```

試してみる。

```hs
> :reload
> :kind TupleList
TupleList :: * -> *
> :kind! TupleList (Integer :^ Double :^ Bool :^ Nil)
TupleList (Integer :^ Double :^ Bool :^ Nil) :: *
= (Integer, (Double, (Bool, ())))
```

ちゃんと期待している型に展開(評価)される。値ex1の型付けに、この型シノニムを使ってみよう。

```hs:tupleList.hs
ex1 :: TupleList (Integer :^ Double :^ Bool :^ Nil)
ex1 = (123, (3.14, (True, ())))
```

型の種類付けが、ゆるゆるだ
------------------------

型構築子TupleListや型演算子(:^)といった型の種を、もういちど、みてみよう。

```hs
> :kind TupleList
TupleList :: * -> *
> :kind (:^)
(:^) :: * -> * -> *
```

TupleListは\*(スター)種の型をとって、\*種の型をかえす。(:^)は\*種の型を、ふたつとって、\*種の型をかえす。つまり、つぎのような型も種エラーにならない。

```hs
> :kind TupleList Integer
TupleList Integer :: *
> :kind Integer :^ Double
Integer :^ Double :: *
```

型構築子TupleListの引数は「型のリスト」であってほしいし、型演算子(:^)の第2引数もまた、「型のリスト」であってほしい。しかし、それ以外の種類の型を引数としても、種エラーはおこらない。これは、種チェックが期待しているほどに厳密に働いていないことになる。

型に、ちゃんとした種類付けをする
--------------------------------

\*種ではなく、型のリストを意味する型に、ちゃんとした種類を用意する。ここでDataKinds拡張を利用する。

```hs:tupleListDK.hs
{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

data List a = Nil | a :^ (List a)
infixr 5 :^
```

List a型の値として、値Nilと、引数をふたつとる値構築子(:^)とを定義した。ここで、DataKinds拡張の力が効果が発動する。すると、「型 - 値」の世界での定義は、「種類 - 型」の世界にも双子の定義を出現させる。つまり、List a種の型として、型Nilと、引数をふたつとる型構求子(:^)とが定義される。

それぞれを確かめてみよう。

```hs
> :load tupleListDK.hs
> :type Nil
Nil :: List a
> :kind Nil
Nil :: List a
```

「型 - 値」の世界に「Nil - List a」があり、「種類 - 型」の世界にも「Nil - List a」があることがわかる。このような、「型 - 値」に対応して作られた「種類 - 型」を、「昇格された種類 - 昇格された型」のように呼ぶ。型シノニムTupleListや、値ex1の定義はtupleList.hsのものと、だいたい、おなじだ。

```hs:tupleListDK.hs
type family TupleList a where
        TupleList 'Nil = ()
        TupleList (a ':^ b) = (a, TupleList b)

ex1 :: TupleList (Integer ':^ Double ':^ Bool ':^ 'Nil)
ex1 = (123, (3.14, (True, ())))
```

tupleList.hsとのちがいは、Nilや(:^)に'(クォート)が付いているところだ。これは、この場合にはつけなくても問題ないが、必須のときもあるので、つけておいたほうが混乱しない。「昇格された型」であることの印だ。

(自分への覚え書き: あとで確認すること! 「昇格された型」という言いかたは「昇格された結果としてできた型」の意味で使って問題ないか)

```hs
> :kind Nil
Nil :: List a
> :kind (:^)
(:^) :: a -> List a -> List a
> :kind TupleList
TupleList :: List * -> *
> :kind TupleList Integer
(種エラーが生じる)
> :kind Integer :^ Bool
(種エラーが生じる)
```

種チェックが適切に行われていることがわかる。

デフォルトのリスト([])も昇格している
------------------------------------

デフォルトのリスト([])も昇格しているので、わざわざList種を定義する必要はない。また、リストに対する構文糖も「型 - 値」の場合とおなじように、「種類 - 型」の世界でも使うことができる。

```hs:tupleListDKL.hs
{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds #-}
{-# OPTIOnS_GHC -Wall -fno-warn-tabs #-}

type family TupleList a where
        TupleList '[] = ()
        TupleList (a ': b) = (a, TList b)

ex1 :: TupleList '[Integer, Double, Bool]
ex1 = (123, (3.14, (True, ())))
```

まとめ
------

型構築子の引数として使うために、値を持たない型を定義することができる。その場合、その型は\*種の型として定義される。ときには、より限定的な種類の型として定義したいこともある。そのようなときに使えるのが、DataKinds拡張だ。「型 - 値」として定義したものとおなじものを、「種類 - 型」の世界でも使えるようになる。このような操作を「昇格」と呼ぶ。Haskellのリストやタプルも昇格されていて、「型 - 値」の世界とおなじ構文糖を使うこともできる。昇格された型には'(クォート)で印をつけておくと、わかりやすい(リストの場合など必須のこともある)。