CoqのSortについて

山本和彦 @kazu_yamamoto

sort の訳語を募集します。 「型の型」ぐらいですか？ Haskell の kind と区別がつくことを希望。 #coqt

Yoshihiro Imai @yoshihiro503

@kazu_yamamoto 割と特別な言葉なので sortまたはソートとかでもよいような気がします。 #coqt

Takuo Watanabe @wtakuo

代数仕様記述をやっている人達は昔から「ソート」と言っていますね． @yoshihiro503 @kazu_yamamoto

山本和彦 @kazu_yamamoto

.@yoshihiro503 「ソート」だと、「整列」を連想させて、いまいちなのです。 #coqt

山本和彦 @kazu_yamamoto

.@wtakuo @yoshihiro503 うう、そうですか。あえて、慣習にあがなう必要もないかもしれませんね。 #coqt

Takashi Miyamoto @tmiya_

CoqでSet,Prop,Typeの上にあるsortと、Maude,OBJとかの代数仕様とかで使うソートと、同じものなんでしょうか？それとも同じ単語を違う意味で使っている？

takeo @bonotake

@keigoi MaudeはOBJの流れを汲んでるので、当然出てきます。項書き換えじゃなく代数的仕様記述の用語として。

Sosuke MORIGUCHI @chiguri

CoqのsortにはSet, Prop, Typeがあるが、これらは「型の素である」という程度だと認識。もちろんそれぞれに特徴はあるが、特徴は固定で、また自分でsortを作れるわけでもない。

takeo @bonotake

@tmiya_ 代数仕様のsortは型とほぼ同義です。typeってのが出てこないから当然区別もない

kenichi kobayashi @kencoba

LOTOSでは、抽象データ型で定義するデータキャリアの名前をsortって言ってるなぁ。オブジェクト指向で言う「属性」ってことかな。 *Tw*

takeo @bonotake

@kencoba 代数仕様記述でも同じノリですよ。属性と言うより、クラスを作るときのプリミティブ型みたいな感じかと。

kenichi kobayashi @kencoba

@bonotake @wtakuo ありがとうございます。sortとしてのqueueって考え方もあるんですね。 *Tw*

Takashi Miyamoto @tmiya_

@bonotake ありがとうございます。代数仕様のsortと、依存型とかでの「型の型」みたいなsortと、なんか違うような気がするけど、同じ単語使っててもやもやとしていましたが、少しはっきりしたような。

takeo @bonotake

@tmiya_ 依存型かどうかはあまり関係ない気がします。CLTTでも慣用的にsortという言葉は出てきますが、typeとの明確な区別はないですね。sortとtypeを区別するのはCoq（Gallina）オリジナルかと。

Takashi Miyamoto @tmiya_

@bonotake ありがとうございます。Coq独特の用語の使い方であること、typeの代わりにsortが使われる分野がある、ということですね。