tensorflowの型付けへのコメント

Jun Mukai より

Jun Mukai — Wed, 14 Sep 2016 16:53:20 +0000

ああいやtensorの形も型（というか型変数）として表現するということです。C++的に言えばテンプレート引数ですかね。そうすると、おっしゃっているような次元の関係（こことここの次元は一致する、とか、こことここの次元をかけたものがこの次元になっている、とか）をコンパイラが検証してくれるはずなので。

C++だとテンプレート引数で指定したサイズについてstaticな定数を作っておいて、サイズ同士の一致とかの関係はstatic_assertで検証できるのかな？と思いましたがC++もよくわからないので……。

なおこの種の型はHaskellは標準ではサポートしてなくて、GHCなどの独自拡張になるんじゃなかったかな、と思っていて、URL先のやつだと {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-} みたいな部分がそういう独自拡張の指示になります。言語組み込みでやるならAgdaとかが必要なんじゃないかなぁよく知りませんが……。
Idrisというその辺が簡単に書けそうな感じの言語もあるようですが調査不足。

いいねいいね

はまじより

はまじ — Wed, 14 Sep 2016 10:36:20 +0000

template と書いたつもりでした(これでうまくいくだろうか)。まあ型に数値のエンコードももちろんできますが。

tensorの形はランタイムに決めたいと思うんですが。ランタイムに決める変数であるが、こことここの次元は一致してないといけない、とか、ここに1足すとここの次元になってるべき…とかやりたいかなというのが元の話でした。まあC++ TMP脳的にはこれも型にエンコードすればなんとでもできるんですが。

いいねいいね

Jun Mukai より

Jun Mukai — Wed, 14 Sep 2016 04:58:36 +0000

> これは値を型にエンコードすることで、型演算で依存型を部分的に実現したってだけ

だと思います。でもtensorの形状をエンコードするぐらいならそれでいいかなという気も。チャーチ数とかはまったく必要ないです（が、この種の例はたいていチャーチ数でエンコードしているので）。C++ templateでちゃんとできるかはあまり深く考えていないのでわかりません。どういうふうにやる感じでしょうか。

なお私もHaskell界隈はもう何年もまったく追ってないのでとてもトンチンカンなことを書いている危険性があります。

いいねいいね

はまじより

はまじ — Tue, 13 Sep 2016 18:00:57 +0000

– 前者の意味だとすると: つまらないというのは同感です。しかしRubyの顧客が実際に求めてるのはだいたいuse strictだという気もするし、そうだとしても言語理論とかをちゃんと考えた、求められてる以上に良い物を提供したいという気概があるからuse strictとかやりたくないんだろうな気もするし
– Dependent type: 理論的には…というのはたぶんそうだというのが僕の今の理解です、が
– 空リストへのhead: このリンク、「おおkonnさんだ」くらいしか読んでないですけど、これは値を型にエンコードすることで、型演算で依存型を部分的に実現したってだけ (https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E3%83%BB%E3%82%AD%E3%83%A5%E3%83%BC%E3%83%96 の用語法) じゃないんですかね
– そのレベルの依存型ならチャーチ数とか必要なくて、 C++ の template で十分じゃないんでしょうか。が具体的なコンパイル時定数を与えないようなやつは、Agdaとかみたいな型計算しかしないやつ以外でよく聞く言語の機能としては見たことが無いと思うな、と
– ちょっと勉強しなおしたり、あらためてほんの少し勉強してみたりしたけど、相変わらず斜め読みではどうにもむつかしくて身につかない話題です。全然頓珍漢なこと言ってる気がする。。
– やはり型の話題には一切触れないのが正解という思いを新たにしました

いいねいいね

tensorflowの型付け へのコメント

Jun Mukai より

はまじ より

Jun Mukai より

はまじ より

tensorflowの型付けへのコメント

はまじより

はまじより