Guarded Algebraic Data Types = 保護された代数データ型？
検索するとヒットした。
Guarded algebraic data types, which subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and phantom types, and are closely related to inductive types, have the distinguishing feature that, when typechecking a function defined by cases, every branch must be checked under di#erent typing assumptions.
Constraint-based type inference for guarded algebraic data types - CiteSeerX
保護された代数データタイプは、インデックスのついた型として学問においてコンセプトが知られているが、
再帰データ型のコンストラクタやファントム型を保護し、帰納型と密接に関連する。
ケースによって定義された関数を型チェックするとき、すべてのブランチが異なる型にあるという前提をチェックしなければならないという機能と区別される。
んーわからない。パターンマッチングの部分の話みたいだ。
ところでファントム型って何？
A phantom type is a type used only to construct other types; its values are never used. Phantom types are used in Type arithmetic, and for encoding bounds checks in the type system.
Phantom type - HaskellWiki
ファントム型は他の型を構築するためだけに使う型だ。その値は絶対に利用されない。ファントム型は型算術においてと、型システムにおいて符号の協会をチェックするために利用される。
まだはっきりしないけど、HaskellのWikiにあるから、関数型言語の何かのようだ。
とりあえずコードを書いてみよう。
package sample.snippet /** This examples illustrates the use of Guarded Algebraic Data Types in Scala. */ object gadts extends Application { /** The syntax tree of a toy language */ abstract class Term[T] /** An integer literal */ case class Lit(x: Int) extends Term[Int] /** Successro of a member */ case class Succ(t: Term[Int]) extends Term[Int] /** Is 't' equal to zero? */ case class IsZero(t: Term[Int]) extends Term[Boolean] /** An 'if' expression */ case class If[T](c: Term[Boolean], t1: Term[T], t2: Term[T]) extends Term[T] def eval[T](t: Term[T]): T = t match { case Lit(n) => n // the rigth hand side makes use of the fact // that T = Int and so it can use '+' case Succ(u) => eval(u) + 1 case IsZero(u) => eval(u) == 0 case If(c, u1, u2) => eval(if (eval(c)) u1 else u2) } println(eval(If(IsZero(Lit(1)), Lit(41), Succ(Lit(41))))) }
ジェネリックな戻り値とパターンマッチングの組み合わせかな。
特に問題なし。
Tは抽象クラスだから、そのサブクラスでパターンマッチしてる。
Termはジェネリックな型を持っていて、eval()の戻り値はTermが持つ型になる。
IsZeroだけがextends Term[Boolean]だからBooleanが戻り値になる。あとはInt。
要は最終的にeval(false, 41, 42)を呼び出す。
実行結果。
42
ところで。
case Succ(u) => eval(u) + 1
の引数 u はどんな名前でもいいんだ。
case Succ(z) => eval(z) + 1
としても実行結果は同じだった。
(追記)
Wikipediaに載ってた。代数的データ型と訳すみたい。
代数的データ型（英: Algebraic data type）とはプログラミングにおけるデータ型の一種で、他のデータ型を当該代数的データ型のコンストラクタで包んだデータを値とする。この包まれたデータはコンストラクタの引数である。他のデータ型と異なり、コンストラクタが実行されることはなく、データを操作するにはパターンマッチを使ってコンストラクタからデータを抜き出さねばならない。
代数的データ型 - Wikipedia
