higher-kinded typesという用語について

1
Windymelt(めるくん)🚀❤️‍🔥 @windymelt

はてなブログに投稿しました #はてなブログ 関数型言語で登場する高カインド型(Higher-Kinded Types; HKT) と(* -> *) -> *みたいなやつの早わかりメモ - Lambdaカクテル blog.3qe.us/entry/2023/10/…

2023-10-09 21:19:21
Kenji Yoshida @xuwei_k

Scalaでhigher-kinded typesと言い出した本人?少なくとも当時にそう呼ばれる機能の実装と理論(Generics of a Higher Kindという2008年論文)に深く関わってた中の人による(有名な?)後悔?のお言葉です stackoverflow.com/a/6427289 adriaanm.github.io/files/higher.p… pic.twitter.com/KHZFRCxS7R

2023-10-09 21:42:30
拡大
Kenji Yoshida @xuwei_k

@windymelt まず用語がアレ、という話 twitter.com/xuwei_k/status… 自信ないけど、もし上記tweetで言及してるようにScalaが初?だとしたらblog内の「Scalaでしか分からない概念は極力排している」と言いつつ、blogタイトル実は当初Scala独自用語!(だけど他でも使われるようになった?)みたいな超面倒事情があり〜

2023-10-09 21:45:38
Windymelt(めるくん)🚀❤️‍🔥 @windymelt

@xuwei_k アハーン、なるほど。もともとはscala的?用語なんですね。ありがとうございます、あとで補足しておきます。(割と使われてるので標準なのかと思ってました〜)

2023-10-09 21:47:16
Kenji Yoshida @xuwei_k

kmizuさんか誰かの発言で自分も大昔に知った気がしたけど、関連発言見つかるけど、そのものの発言見つからないな(そもそもtwitter上だったか不明) twitter.com/kmizu/status/7…

2023-10-09 21:54:36
kmizu @kmizu

higher kinded generics やら higher order polymorphismやら呼ばれてるアレですが、どうもhigher kinded genericsという用語は元をたどるとAdriaan MoorsさんのScalaにアレ実装した論文が元になってるぽい

2016-05-14 16:13:33
kmizu @kmizu

@xuwei_k なんか懐かしいですねー。確かにこの言葉が混乱を生んだのは間違いないというか、単純に型コンストラクタ多相(をもうちょっと小難しくない言い換えをした)が広まってればよかった感じはありますね。

2023-10-09 22:07:04
Kenji Yoshida @xuwei_k

ついでにScalaでのkindにおいて発展的(?)な話題や豆知識を色々書いておくと、 Scala 2にはREPLに :kind コマンドがあったり(Scala 3は・・・) xuwei-k.hatenablog.com/entry/20131017… AnyとNothingはkindが特殊だったり、 Scala 3にはAnyKindというものが増えたり、 など色々ある pic.twitter.com/JKsv8Rj8ay

2023-10-09 22:24:16
拡大
Kenji Yoshida @xuwei_k

このREPLの :kind コマンドの出力をよく見るとわかるように、Scalaにはvarianceもあるので、途中にvariance含めた表記になるが、これは完全Scala独自なのか?他の例あるのか? などといった話題も

2023-10-09 22:27:37
Kenji Yoshida @xuwei_k

例えばこのあたりの twitter.com/xuwei_k/status… "(Scalaの用語での)higher kind type的なもの" という微妙な言い方は、さきほどのtweetの事情が頭の片隅に入っている結果による表現となっています

2023-10-09 22:31:19
Kenji Yoshida @xuwei_k

@kis @windymelt 型クラスそのものは使えれば便利なのだけど、真面目に型クラス便利に使わせようとすると、Scalaのimplicitや(Scalaの用語での)higher kind type的なもの導入する必要があって、 その点において後付けで既存の言語に入れるのはpattern matchその他よりもだいぶハードルが高いはず、みたいなのが

2023-09-18 17:36:15
でこれき @dico_leque

「カインドという用語はもともと〜」という追記がされているけど、よしださんが指摘しているのはカインドではなくhigher-kinded typesのことのような twitter.com/windymelt/stat…

2023-10-10 00:42:05
でこれき @dico_leque

高カインド多相とか高階多相と呼ばれるものの呼び名については「高階多相か高カインド多相、どちらが適切な用語かを考える - kmizuの日記」も参照 kmizu.hatenablog.com/entry/2017/05/…

2023-10-10 00:44:49
でこれき @dico_leque

カインドという用語がいつから使われているかは知らないけど、BarendregtのAn Introduction to Generalized Type Systems (1991)に"□ , the sort of all kinds"という表現があるのでそれよりは前? homepages.inf.ed.ac.uk/wadler/papers/…

2023-10-10 01:00:58
Kenji Yoshida @xuwei_k

@windymelt "カインドという用語はもともとScalaあたりで作られた用語" ではなくhigher-kinded のはずです(追記されてる件)

2023-10-10 09:22:17
Kenji Yoshida @xuwei_k

ついでだから、Scala 2 compiler内部にhigher kindが実装されたcommitを探してみたけど、当時はSVNでGitHubではなかったので探しづらいし、commitが判明しても議論が・・・これかな?2007年4月 github.com/scala/scala/co…

2023-10-10 13:58:31
Kenji Yoshida @xuwei_k

@windymelt 念のためかるく調べたけど、 kindという用語自体は少なくともHaskell 98というものに既に出ていて(Scalaが作られるずっと前から使われていて)、 あくまでおそらくkindはそれなりに昔から一般的用語で、higher-kinded (types)、という用語の導入が微妙だったかもね、という

2023-10-10 14:01:27
Kenji Yoshida @xuwei_k

@windymelt twitter.com/esumii/status/… でも、ここにきてScala初出ではないかもしれない情報発掘したので、余計にややこしくなってきた(?)

2023-10-10 15:07:20
S (ツイートはスレッド全体をご確認ください) @esumii

(int→int)→intをあまりhigher typeとか言わないと思うんですがhigher kindって誰が言い出したんだろう(すみません調べていません。すでにScalaやGenerics of a Higher Kind(2008)より前のTAPL(2002)にありますが twitter.com/esumii/status/…

2017-08-09 21:09:00
S (ツイートはスレッド全体をご確認ください) @esumii

@xuwei_k @windymelt Kindはもちろんですが、higher kindも、Scalaよりはるか昔からある型システム用語なのは確実です。ご参考まで。

2023-10-10 16:59:33
Kenji Yoshida @xuwei_k

@esumii @windymelt お、なるほど??? 用語としては(少なくともScalaより)昔からあるけれど、似たようなというか同じようなものを示す用語がそれより前に既に存在した(?)から、そういう用語発明しなくてよかったのでは?という認識自体はあってますか・・・?

2023-10-10 17:02:30
S (ツイートはスレッド全体をご確認ください) @esumii

@xuwei_k @windymelt それは"kind"や"higher kind"ではなく"higher-kinded type"のことでしょうか。そもそもtypeならkindは*なのでhigherではなく、"higher-kinded type"という用語自体が論理的に意味が不明で、ちゃんと調べてませんが正確な用語ではない気がします。

2023-10-10 17:08:09
Kenji Yoshida @xuwei_k

@esumii @windymelt なるほど、ありがとうございます

2023-10-10 17:17:02
Kenji Yoshida @xuwei_k

"higher kinded type"という用語が微妙な場合 twitter.com/esumii/status/… ざっくり調べたけど - "Generics of a Higher Kind"の論文に出てくる - Scala 2や3の実装にも出てくる - Scala 2の仕様では使ってない?(偉い?) - Scala 3の仕様(あまり書かれてないが)、には出てきてしまってる? という感じ

2023-10-10 17:43:35
S (ツイートはスレッド全体をご確認ください) @esumii

@xuwei_k Scalaの実装や言語仕様は論文ではないので用語が正確とは限らないのと、Generics of a Higher Kindも実用寄りの論文&学会なので、査読で理論の専門家がいなかったか、いてもコメントが反映されなかったのかもしれませんね。

2023-10-10 19:33:00
でこれき @dico_leque

higher kindについては、TaPL (2002)の31 Higher-Order Subtypingの章に用例がある(索引になかったため目でざっと探したけれど、もっと前の章にもあるかもしれない

2023-10-10 21:42:02
S (ツイートはスレッド全体をご確認ください) @esumii

twitter.com/esumii/status/… 「Higherなkindをつけられたtype」という文字通りの意味ではなく、大雑把に「higher kindを含むtype system全体」ぐらいのつもりのネーミングだったのかも?(憶測

2023-10-11 09:18:39
S (ツイートはスレッド全体をご確認ください) @esumii

そもそも"higher kind"も、kindが"high"とか"low"とか言うのか、ちょっと変な気がしますが、これはScalaよりはるかに前から定着している用語らしい。Cf. twitter.com/esumii/status/…

2023-10-11 09:22:59