Freer Effectsが、だいたいわかった: 11-4 DataKinds拡張
目次
(0). 導入
-
Freeモナドの概要
- Freeモナドとは
- FreeモナドでReaderモナド、Writerモナドを構成する
- 存在型(ExistentialQuantification拡張)の解説
- 型シノニム族(TypeFamilies拡張)の解説
- データ族(TypeFamilies拡張)の解説
- 一般化代数データ型(GADTs拡張)の解説
- ランクN多相(RankNTypes拡張)の解説
-
FreeモナドとCoyoneda
- Coyonedaを使ってみる
- FreeモナドとCoyonedaを組み合わせる
- いろいろなモナドを構成する
-
Freerモナド(Operationalモナド)でいろいろなモナドを構成する
- FreeモナドとCoyonedaをまとめて、Freerモナドとする
- Readerモナド
- Writerモナド
- 状態モナド
- エラーモナド
-
モナドを混ぜ合わせる(閉じた型で)
- Freerモナドで、状態モナドとエラーモナドを混ぜ合わせる
- 両方のモナドを一度に処理する
- それぞれのモナドを、それぞれに処理する
- Freerモナドで、状態モナドとエラーモナドを混ぜ合わせる
- 存在型による拡張可能なデータ構造(Open Union)
- 追加の言語拡張
- ScopedTypeVariables拡張
- TypeOperators拡張
- KindSignatures拡張
- DataKinds拡張
- MultiParamTypeClasses拡張
- FlexibleInstances拡張
- OVERLAPSプラグマ
- Open Unionを型によって安全にする
- モナドを混ぜ合わせる(開いた型で)
- FreeモナドとOpen Unionを組み合わせる
- 状態モナドにエラーモナドを追加する
- Freer Effectsで、IOモナドなどの、既存のモナドを使用する
- 関数を保管しておくデータ構造による効率化
- いろいろなEffect
- 関数handleRelayなどを作成する
- NonDetについて、など
はじめに
DataKinds拡張について学ぶ。
値には型がある。型には種類がある。DataKinds拡張を有効にしておくと、「値 - 型」を定義したときに、それに対応する「型 - 種類」が定義される。
と、いうわけだが、ここまで読んで「なるほど、なるほど」となったかたは、続きを読む必要はない。このあとは、具体的な例で説明していく。
言葉について
kindをここでは「種類」と訳した。一般的には「種」と呼ぶ。「種」よりも「種類」のほうが、日常的な言葉なので、とっつきやすいという配慮だ。
タプルでリスト
Lisperにとって、リストは連鎖したコンスだ。コンスというものは、まあだいたい2要素タプルのようなものだ。なので、LisperにとってのリストをHaskellで書くと、つぎのようになる。
ex1 :: (Integer, (Double, (Bool, ())))
ex1 = (123, (3.14, (True, ())))
ついでにcarとcdrを定義しておこう。
car :: (a, b) -> a
car = fst
cdr :: (a, b) -> b
cdr = snd
試してみよう。
> :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
()
「タプルでリスト」の型をまとめる
「タプルでリスト」の型に別名をつけて、ひとつにまとめたい。型の別名には「型のリスト」が必要になる。まずは「型のリスト」を作ってみよう。
{-# 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拡張)で使えるようになった。これらは、値の型付けには使われず、型構築子の引数として使われる。試してみる。
> :load tupleList.hs
> :set -XTypeOperators
> :kind Integer :^ Double :^ Bool :^ Nil
Integer :^ Double :^ Bool :^ Nil :: *
これで、型のリストができた。これを引数とする型シノニムTupleListを定義する。
type family TupleList a where
TupleList Nil = ()
TupleList (a :^ b) = (a, TupleList b)
試してみる。
> :reload
> :kind TupleList
TupleList :: * -> *
> :kind! TupleList (Integer :^ Double :^ Bool :^ Nil)
TupleList (Integer :^ Double :^ Bool :^ Nil) :: *
= (Integer, (Double, (Bool, ())))
ちゃんと期待している型に展開(評価)される。値ex1の型付けに、この型シノニムを使ってみよう。
ex1 :: TupleList (Integer :^ Double :^ Bool :^ Nil)
ex1 = (123, (3.14, (True, ())))
型の種類付けが、ゆるゆるだ
型構築子TupleListや型演算子(:^)といった型の種を、もういちど、みてみよう。
> :kind TupleList
TupleList :: * -> *
> :kind (:^)
(:^) :: * -> * -> *
TupleListは*(スター)種の型をとって、*種の型をかえす。(:^)は*種の型を、ふたつとって、*種の型をかえす。つまり、つぎのような型も種エラーにならない。
> :kind TupleList Integer
TupleList Integer :: *
> :kind Integer :^ Double
Integer :^ Double :: *
型構築子TupleListの引数は「型のリスト」であってほしいし、型演算子(:^)の第2引数もまた、「型のリスト」であってほしい。しかし、それ以外の種類の型を引数としても、種エラーはおこらない。これは、種チェックが期待しているほどに厳密に働いていないことになる。
型に、ちゃんとした種類付けをする
*種ではなく、型のリストを意味する型に、ちゃんとした種類を用意する。ここでDataKinds拡張を利用する。
{-# 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と、引数をふたつとる型構求子(:^)とが定義される。
それぞれを確かめてみよう。
> :load tupleListDK.hs
> :type Nil
Nil :: List a
> :kind Nil
Nil :: List a
「型 - 値」の世界に「Nil - List a」があり、「種類 - 型」の世界にも「Nil - List a」があることがわかる。このような、「型 - 値」に対応して作られた「種類 - 型」を、「昇格された種類 - 昇格された型」のように呼ぶ。型シノニムTupleListや、値ex1の定義はtupleList.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や(:^)に'(クォート)が付いているところだ。これは、この場合にはつけなくても問題ないが、必須のときもあるので、つけておいたほうが混乱しない。「昇格された型」であることの印だ。
(自分への覚え書き: あとで確認すること! 「昇格された型」という言いかたは「昇格された結果としてできた型」の意味で使って問題ないか)
> :kind Nil
Nil :: List a
> :kind (:^)
(:^) :: a -> List a -> List a
> :kind TupleList
TupleList :: List * -> *
> :kind TupleList Integer
(種エラーが生じる)
> :kind Integer :^ Bool
(種エラーが生じる)
種チェックが適切に行われていることがわかる。
デフォルトのリスト([])も昇格している
デフォルトのリスト([])も昇格しているので、わざわざList種を定義する必要はない。また、リストに対する構文糖も「型 - 値」の場合とおなじように、「種類 - 型」の世界でも使うことができる。
{-# 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のリストやタプルも昇格されていて、「型 - 値」の世界とおなじ構文糖を使うこともできる。昇格された型には'(クォート)で印をつけておくと、わかりやすい(リストの場合など必須のこともある)。