Freer Effectsが、だいたいわかった: 4. データ族(TypeFamilies拡張)の解説

目次

(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モナドで、状態モナドとエラーモナドを混ぜ合わせる
存在型による拡張可能なデータ構造(Open Union)
追加の言語拡張
モナドを混ぜ合わせる(開いた型で)
- FreeモナドとOpen Unionを組み合わせる
- 状態モナドにエラーモナドを追加する
Open Unionを型によって安全にする
Freer Effectsで、IOモナドなどの、既存のモナドを使用する
関数を保管しておくデータ構造による効率化
いろいろなEffect
- 関数handleRelayなどを作成する
- NonDetについて、など

データ族

データ族とは

型シノニムに対して、型シノニム族があるように、代数的データ型の定義に対しては、データ族がある。データ族は型シノニム族とおなじように、TypeFamilies拡張で使えるようになる。

型シノニム族とデータ族のちがいは、型シノニムの定義と、代数的データ型の定義とのちがいとおなじだ。それぞれのインスタンスが、型シノニム族では既存の型に対する別名となるのに対して、データ族では新しい型になるということだ。

それぞれの型に対して、それぞれに専用のデータ型を用意したいようなときに、使うことができる。

データ族の例

データ族の定義の書きかたは、型シノニム族の定義と、あまり変わらない。データ族を定義してみよう。ファイルdataFamily.hsを、つぎのように作成する。

dataFamily.hs

{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

data family Foo x

data instance Foo Int = FooInt Bool Char
data instance Foo Char = FooChar Double Integer

値構築子の型をみてみよう。

> :load dataFamily.hs
> :type FooInt
FooInt :: Bool -> Char -> Foo Int
> :type FooChar
FooChar :: Double -> Integer -> Foo Char

このような定義は、つぎのような定義とよく似ている。ファイルnoDataFamily.hsを作成する。

noDataFamily.hs

{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

data Foo
        = FooInt Bool Char
        | FooChar Double Integer

値構築子の型をみてみよう。

> :load noDataFamily.hs
> :type FooInt
FooInt :: Bool -> Char -> Foo
> :type FooChar
FooChar :: Double -> Integer -> Foo

これらは、よく似ているが、データ族では値構築子の追加に対して、開かれている。つまりFoo BoolやFoo Integerなどが追加される可能性がある。よって、つぎのように、クラスに属さない関数を書くことはできない。

useFoo :: Foo a -> ...
useFoo (FooInt x y) = ...
useFoo (FooChar x y) = ...

データ属Fooを利用する関数は、クラス関数として書く必要がある。ファイルdataFamily.hsに追加する。

dataFamily.hs

class UseFoo a where
        useFoo :: a -> Foo a -> String

instance UseFoo Int where
        useFoo x (FooInt y z) = show x ++ " " ++ show y ++ " " ++ show z

instance UseFoo Char where
        useFoo x (FooChar y z) = show x ++ " " ++ show y ++ " " ++ show z

試してみよう。

> :load dataFamily.hs
> useFoo 123 (FooInt True 'c')
"123 True 'c'"
> useFoo 'c' (FooChar pi 12345)
"'c' 3.141592653598979 12345"

型クラスに関連づけられたデータ族

データ族は、たいてい、クラス関数によって処理される。なので、データ族を型クラスに関連づける書きかたが用意されている。うえの例では、つぎのようになる。

class UseFoo a where
        data Foo a
        useFoo :: a -> Foo a -> String

instance UseFoo Int where
        data Foo Int = FooInt Bool Char
        useFoo x (FooInt y z) = show x ++ " " ++ show y ++ " " ++ show z

だいたいにおいて、こちらの書きかたのほうが、コードがわかりやすくなる。ここでは「書きかた」をみるために意味のない例を挙げた。データ族の意味のある使用例は「決定性有限オートマトンを実装する」を参照のこと。

閉じたデータ族?

さて、データ族を処理するには型クラスが必要になる。それは、データ族が値構築子の追加に対して開いている、つまり、値構築子の追加がどこでも、モジュールをまたいででも、できるからだ。値構築子を列挙することができないので、通常の関数ではあつかえない。

それならば閉じたデータ族ならばどうか。値構築子が列挙できるので、通常の関数であつかえるはずだ。たとえば、つぎのような定義ができるはずだ。

data family Foo where
        Foo Int = FooInt Bool Char
        Foo Char = FooChar Double Integer

useFoo :: a -> Foo a -> String
useFoo x (FooInt y z) = ...
useFoo x (FooChar y z) = ...

しかし、このような書きかたは許されていない。この、「閉じたデータ族」と同等な定義ができるようにするのが、GADTs拡張である。

まとめ

型シノニム族、データ族について解説した。これらは、おもに型クラスのインスタンスを定義するときに、インスタンスとなる型に関連づけられる型を指定するために使われる。型シノニムの追加に対して、閉じた型シノニム族を定義することができる。同様な値構築子の追加に対して閉じたデータ族は定義できないが、GADTsが、だいたい、おなじことを実現している。

参考

Wikibooks: GHC/Type families