多相種とGenericDerivingの関係について

shelarcy（しぇらーしぃ） @shelarcy

そっか。データ型を型レベルに昇格させる機能があれば、Generic Deriving で使われる多くのデータ型をいくつかの少ないのデータ型に集約させることができますね。 http://t.co/Ql6ZukJm

shelarcy（しぇらーしぃ） @shelarcy

多相種が扱えることだけ見ていて、こちらの改良が行われる可能性を見逃してましたが。

ELD-R-ESH-2 @eldesh

あれより少なくなるとかワケ分からん

shelarcy（しぇらーしぃ） @shelarcy

@eldesh あ、今は :+: を除き型とデータ構成子を一体一対応で定義したり、「data P」のようなデータ型を構成子を持たない空の型として定義したりしていますが、

shelarcy（しぇらーしぃ） @shelarcy

@eldesh データ型を型レベルに昇格させる機能があれば（データ構成子をデータ型として扱うことができるようになるので）、そんなことをしなくても、各データ構成子を Universe や MetaData のような少数のデータ型に属するものとしてまとめることができるということです。

shelarcy（しぇらーしぃ） @shelarcy

@eldesh 例えば、リンク先のアイデアでは「data MetaData = C | D | S」というデータ型の定義が書かれていますが、（PolyKinds 言語拡張を使えば）ここで定義されているCやD、Sというデータ構成子をデータ型として型宣言の部分で書くことができます。

shelarcy（しぇらーしぃ） @shelarcy

@eldesh あと、データ型の種を合わせるために便宜的に利用していたデータ型に関しては、（同じく PolyKinds 言語拡張で）「k -> *」のような多相種が扱えるようになったことにより要らなくなる可能性がありますね。

ELD-R-ESH-2 @eldesh

@shelarcy :+: とかPとかを特別な(deriving用の)型として与えておかなくても、Universe型の構成子として普通の型のように定義出来る…？

shelarcy（しぇらーしぃ） @shelarcy

@eldesh Universe 型のデータ構成子として提供した :+: とか P を、Generic Deriving のユーザーは従来の :+: 型や P 型として利用できるという意味であるなら、そうです。

ELD-R-ESH-2 @eldesh

@shelarcy はい。そういう意図でした。

ELD-R-ESH-2 @eldesh

複雑なパターンが分かりやすい感じに定義できたりするのかな？

shelarcy（しぇらーしぃ） @shelarcy

@eldesh Universe 型に所属させる利点は、P や :+: のような型の利用方法の間違いが種によって（分かりやすく）区別できるようになることです。

shelarcy（しぇらーしぃ） @shelarcy

@eldesh これまで:+:型には「* -> * -> *」という引数の数以外の制約は含まれていませんでしたが、Universeのデータ構成子として定義とすることで「Universe k -> Universe k -> Universe k」という明確な種を持つことになります

shelarcy（しぇらーしぃ） @shelarcy

@eldesh e.g. （AnyK = 種変数です。） > :kind (:+:) (:+:) :: Universe AnyK -> Universe AnyK -> Universe AnyK > :kind P P :: Nat -> Universe AnyK

shelarcy（しぇらーしぃ） @shelarcy

@eldesh .｡oO(:kind は種を調べるコマンドです。型を調べるコマンドではありません。念のため。あと、「data Nat = Zero | Succ Nat」としてます。この定義では、P 型が P と P1 型を一つにまとめた形になってますね。)

ELD-R-ESH-2 @eldesh

@shelarcy 「利用方法の間違いによって～」というのは、Universe型に含まれる構成子(?)から成る型のみについてderiving(が定義)出来るから、ということでしょうか？

ELD-R-ESH-2 @eldesh

.oO(ところでそろそろ頭がばくはつしそうなのです)

shelarcy（しぇらーしぃ） @shelarcy

@eldesh Generic Deriving でインスタンスを導出したいクラス（例えば GShow）の定義が正しいかどうかを検査するのに、現在の引数しか情報のない種では情報が少なすぎますよね？、ぐらいの意味です。

shelarcy（しぇらーしぃ） @shelarcy

@eldesh データ型を型レベルに昇格させる機能を Generic Deriving の例とで考えると、一度に複数のことを考えないといけなくなって難しくなるのだと思います。

shelarcy（しぇらーしぃ） @shelarcy

@eldesh 例えば型レベル自然数の例 [http://t.co/fdxzNtPm http://t.co/UbwUx3bq ] だと、「data Zero; data Succ n」ではなく「data Nat = Zero | Succ Nat」と書けるようになって、

ELD-R-ESH-2 @eldesh

@shelarcy はい。まず個別に理解するべきですねｗ (特に型レベルに昇格させる方を…

shelarcy（しぇらーしぃ） @shelarcy

@eldesh * という種ではなく Nat という種をつかうことで、型レベル自然数が入ってくるべきところにそうでない型が入ってくるようなプログラムを種のエラーとして弾ける、これがすべてです。

ELD-R-ESH-2 @eldesh

あぁ、わかった。universeは名前通り全部入りだからバリエーションが思い付かなかったけど、nat見るといくらでも面白いことになりそうな気がする。