GADT
Generalized Algebraic Data type
通常のADTでは、全てのコンストラクタが共通の型引数を共有するが、
GADTを使用すると、各コンストラクタが異なる型を持つことができる
例として、単純な数式を表す型を書いてみる
通常の構文で書くと以下のように書ける
code:hs
data Expr a = Val a
| Add (Expr a) (Expr a)
ただし、これには少し問題がある
今のままだと、任意の型aを足し算することが許されてしまう
そこで、aを具体化してIntとしてみる
code:hs
data Expr a = Val Int
| Add (Expr Int) (Expr Int)
これと全く等価なものGADTを使って書くと以下のようになる
code:Hs
data Expr a where
Val :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
ここに、新たにIfやEqなどの命令を追加する
code:hs
data Expr a where
Val :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
Eq :: Expr Int -> Expr Int -> Expr Bool
If :: Expr Bool -> Expr a -> Expr a -> Expr a
これはGADTでないと、このように定義できない
仮に、通常の書き方をするなら以下のようにしか書けない
code:hs
data Expr = Val Int
| Add Expr Expr
| Eq Expr Expr
| If Expr Expr Expr
しかし、こうすると型安全でないのでIf (Val 1) (Val 2) (Val 3)のような間違った式を作れてしまう
つまり、
通常のADTだと、型引数aを取ったとき、全ての値コンストラクタに対して共通のaを使うことになる。
GADTを使うと、値コンストラクタごとに異なるものを指定することができる
この説明で、Generalized ADTがADTの一般化であることがわかると思うmrsekut.icon
1行ごとに値コンストラクタを定義する
purs
参考
わかりやすい解説
実装例など
rust
rust