GADTとは

Generalized Algebraic DataTypes（GADT）と言うHaskellの記法(?)を知りました

Haskellの入門書などで出てくるMaybe型は以下のような定義になっています

data Maybe a = Nothing | Just a

これをGADTで書くと以下のようになるそうです

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

GADTで面白いのは、値コンストラクタがただの関数へと変化し、
戻り値型のMaybe型が直和型ではなくなっている（ように見える）ところです

またGADTの本来の特徴は多相型における値コンストラクタ（や一部の関数）
の戻り値型の取る型引数を任意の型に固定できる点です

先ほどのMaybe型を改造します
改造箇所は2型引数を取り、第1引数ではコンストラクタ毎の
識別用の型（いわゆる型tag）を付けるようにできます

--tag型
data NothingT
data JustT

--改・Maybe型
data Maybe' t a where
    Nothing :: Maybe' NothingT a 
    Just    :: a -> Maybe' JustT a

こんな事ができると何がうれしいのでしょう？

まずパターンマッチを考えます
通常のMaybe型では以下のようになります

func :: (Show a) => Maybe a -> String
func (Just x)    = "just " ++ show x
func Nothing     = "Nothing"

これがMaybe'型では以下のようになります

func :: (Show a) => Maybe' tag a -> String
func (Just x)    = "Just " ++ show x
func Nothing     = "Nothing!"

あれ？変わってなくね？

と、思いがちになるのですが
Maybe'型であればWarningを出さずに
pattern matchを制限する事ができるようになります

例えば

func :: (Show a) => Maybe' t a -> String
func (Just x)    = "Just " ++ show x
--func Nothing     = "Nothing!"

のようにNothingをコメントアウトします
するとGHCでは

prog.hs:11:1: Warning: 
                Pattern match(es) are non-exhaustive
                In an equation for ‘func’: Patterns not matched: Nothing'

のように警告がでて怒られます

引数のMaybe型がJust aなのかNothingなのかはMaybe型の引数で判別できないため
Nothingで生成したMaybe型を関数に渡すところまでは
コンパイル時にチェックして問題なく通る（※）
→実行時に死ぬと言う事になります

となるとpattern matchにない値コンストラクタは
コンパイル時に検出して欲しいという要求がありそうです
GADTではこれを実現できます

先ほどの関数を以下のように書き換えます

func :: (Show a) => Maybe' JustT a -> String
func (Just x)    = "Just " ++ show x
--func Nothing     = "Nothing!"

何処が変わったかというと、1行目のMaybe' t aがMaybe' JustT aに変わっています
これでWarningが出なくなります。
（この状態でコメントアウトを解除してもNothingが型エラーになります）

このようにパターンマッチ時にそもそも選択したくないマッチ条件を
排除するために利用されるようです

（※）ちなみにMaybe型はもともとshow Nothingでaの型が判別できないので
（こちらの意図とは異なるものの）ちゃんとコンパイルエラーになります
（Phantom-typeというコンパイル時型チェックの記法のようです）

本題

このGADT記法＋tagのMaybeをC++で再現してみます

{-#LANGUAGE GADTs #-}

--tag
data NothingT
data JustT

-- data Maybe
data Maybe' t a where
    Nothing :: Maybe' NothingT a 
    Just    :: a -> Maybe' JustT a　

-- instance class show
instance (Show a) => Maybe' tag a where
    show (Just x) = "Just " ++ show x
    show Nothing  = "Nothing!"

main = do
    --putStrLn $ show Nothing
    putStrLn $ show (Just 42)

#include<iostream>

// tag
struct NothingT{};
struct JustT{};

// data Maybe
template<typename TAG,typename A> struct Maybe
{ A _; Maybe(A a):_(a){} };
template<typename T>
auto Just(T a){ return Maybe<JustT,T>(a); }
template<typename T=int> // 匿名型のままにはできない・・・
auto Nothing(){ return Maybe<NothingT,T>(0); }

// instance class show
template<typename T>
std::string show(Maybe<JustT,T> a)
{return "Just "+std::to_string(a._);}
template<typename T>
std::string show(Maybe<NothingT,T>)
{static_assert(std::is_same<T,void>::value,"can't show Nothing"); return "";}

int main()
{
    //show( Nothing() );
    show( Just(1)   );
}

http://melpon.org/wandbox/permlink/IhrmT6PWKLYN424T

参考：
http://faithandbrave.hateblo.jp/entry/20111201/1322718742

hightoroのブログ

GADT記法＋tagをC++で

GADTとは

こんな事ができると何がうれしいのでしょう？

本題