GADT
簡単のため、型変数がひとつしかない GADT について考える。
すごいふわっと言うと、「sealed かつ多相的な G[T] (1)であって、T に入り得る型の形というのが G の各 case (2)が宣言する G への extends 関係によって(3)制約されているようなデータ型」のことを GADT (Generalized Algebraic DataTypes) と言う。
「T に入り得る型の形が制約されている」とはどういうことか、というのを明らかにするため、例として、次のようなデータ型 PairOrTriple[A] を考える。この PairOrTriple は GADT である。
code:scala
sealed trait PairOrTripleA // (1)
// (2)
case class PairK(first: K, second: K) extends PairOrTriple(K, K) /* (3) */
// (2)
case class TripleK(first: K, second: K, third: K) extends PairOrTriple(K, K, K) /* (3) */
例えば、 PairOrTriple[Int] というのは、型としては書き下せるのだが、p: PairOrTriple[Int] となるような値はひとつたりとも存在しない。なぜなら、PairOrTriple というのは、 Pair か Triple によってしか値が生成できないデータ型であるから、例えば今手元に x: PairOrTriple[A] があったとすると、
何らかの型 k について、x = Pair[k](k1, k2) として構築されているか、
何らかの型 k について、x = Triple[k](k1, k2, k3) として構築されているか
のどちらかでしかないから、いずれの場合にも A = Int であるのはあり得ないからである。
うまみ
windymelt.icon DSL みたいなデータを作るときに、Pair とか Triple の代わりに case class として Add とか Not を作ると思うんですけど、Not だったら Bool → Bool にしたいはずで、これは Add を使うか Not を使うかで型が変わるけど、どちらも「構文」だよと sealed trait としてまとめたい。どんな型 A でも良いわけじゃないんだよねというケースがある
lemoncmd.icon 誰が A を作るのか理解していない
Kory.icon DSL の話でいうと、インタプリタが使います
lemoncmd.icon あ～解釈する側の人がうれしい。
code:scala
enum ExprR:
case LitNum(n: Int) extends ExprInt
case LitBool(b: Boolean) extends ExprBoolean
case Add(n: ExprInt, m: ExprInt) extends ExprInt
case Not(b: ExprBoolean) extends ExprBoolean
こういう感じで使いたい
code:scala
Add(LitBool(true), LitBool(false)) // こういうコードは拒否したいが、caseごとにextendsを制約できないと型が通っちゃう