GADTs使ってみた - Faith and Brave

このエントリは、Haskell Advent Calendar 2011の参加記事です。

今回は、HaskellのGHC拡張であるGADTs(Generalized Algebraic Data Types : 一般化代数データ型)を調べて使ってみたという内容を書いてみました。

最初に、GADTsはGHC拡張なので、使用するには以下のようにして拡張を有効にする必要があります：

{-#LANGUAGE GADTs #-}

まずは構文的な違いを、Maybeを例にして見てみましょう。
通常の代数データ型では、Maybeは以下のように書きます：

data Maybe a = Nothing | Just a

GADTsでは以下のように書きます：

data Maybe a where
    Nothing :: Maybe a
    Just    :: a -> Maybe a

通常の代数データ型では、データコンストラクタを | で区切って記述しますが、GADTsでは、それぞれのデータコンストラクタを関数のように表記し、 -> で繋いだ最後の型がデータコンストラクタの結果型となります。
Maybeの例では、まだGADTsらしさというのは特に何もありません。

では、GADTsらしい例を見てみましょう。
GADTsでは、データコンストラクタを関数のように表記できるようになったことで、データコンストラクタごとに型を付けることができます。
以下は、簡単な値型です：

data ZeroValue
data OtherValue

data Value x tag where
    Zero  :: Value Int ZeroValue
    Other :: Int -> Value Int OtherValue

代数データ型自体を定義する前に空の型(ZeroValue, OtherValue)を定義してますが、これは代数データ型のどのデータコンストラクタを使用しているかのタグとして使います。
これによって、従来の代数データ型がデータコンストラクタが異なっても同じ型になるのに対し、GADTsによる代数データ型ではデータコンストラクタごとに型を付けることができます。

ちなみに、GADTsのデータコンストラクタは、型を返す関数と見なすことができます。つまり型の型(type of type)です。Haskellではこれを種(kind)と呼びます。
GHCiには、関数の型を取得する「:type」コマンドの他に、種を取得する「:kind」コマンドがあります。Valueの種を確認してみましょう。

> :kind Value
Value :: * -> * -> *

型を2つ受け取って型を返す型ですね。

本題に戻ります。
GADTsの代数データ型を引数にとる関数は、通常の代数データ型と同様、その代数データ型で定義されたデータコンストラクタを受け付けることができます。

-- この関数は、Valueのあらゆるデータコンストラクタを許可する
valueToInt :: Value a tag -> Int
valueToInt Zero      = 0
valueToInt (Other x) = x

main = do
        print $ valueToInt Zero
        print $ valueToInt (Other 3)

0
3

また、GADTsの場合は、データコンストラクタごとに型が付いているので、特定のデータコンストラクタの値のみを受け取る関数というのも定義することができます。

zeroToInt :: Value a ZeroValue -> Int
zeroToInt Zero = 0

main = do
        print $ zeroToInt Zero
--      print $ zeroToInt (Other 3) -- コンパイルエラー！

これは、代数データ型を扱う関数が、「この値しか受け付けない」という強い保証ができるようになったことを意味します。

GADTsの代表的な例として、空のリストと非空のリストを型コンストラクタで分けて、「非空リストしか受け付けない関数」を定義するものがあります。

data Empty
data NonEmpty

data StrongList x y where
     Nil  :: StrongList a Empty
     Cons :: a -> StrongList a b -> StrongList a NonEmpty

safeHead:: StrongList x NonEmpty -> x
safeHead (Cons a b) = a

main = do
        print $ safeHead (Cons 1 (Cons 2 Nil))
--      print $ safeHead Nil -- コンパイルエラー！

リストの先頭要素を取得するhead関数や、先頭要素を除いたリストを取得するtail関数は、空リストが渡された場合に実行時エラーとなってしまいますが、GADTsを使えば、空リストが渡されないことが保証できるので、決してエラーにならないhead関数やtail関数を定義することができます。

このあたりでまとめましょう。
GADTsは、データコンストラクタを型付けすることができる代数データ型です。
これによって、従来のあらゆるデータコンストラクタを許可する関数を定義できるだけでなく、特定のデータコンストラクタのみを許可する関数を定義できるようになり、さらなる柔軟性と、実行時エラーに対するさらなる強い保証を手にすることができるようになります。
GADTsは、型の新たな可能性として他の言語のユーザーにもこの機会に知っていただければと思います。
Scalaでもできるみたいですね(参照：gadts.scala)。

Haskell Advent Calendar、2日目のid:ruiccさんに続きます。