GADTs使ってみたを読んだらわかりやすかったので、適当なサンプルを見つけてみた。
プログラミングHaskell10.5の仮想マシンを例に取る
data Expr = Val Int | Add Expr Expr value :: Expr -> Int value (Val n) = n value (Add x y) = value x + value y
GADTで書き直すと
data Expr where Val :: Int -> Expr Add :: Expr -> Expr -> Expr value :: Expr -> Int value (Val n) = n value (Add x y) = value x + value y
データコンストラクタが、型をとって型を返す関数のように表現できる。
実行するにはGADTs拡張をつける
$ ghci -XGADTs vmachine2.hs GHCi, version 7.4.1: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( vmachine2.hs, interpreted ) Ok, modules loaded: Main. *Main> value (Add (Val 3) (Val 2)) 5
Haskellerも順調に増加している