tensorflowの型付け

http://shinh.skr.jp/m/?date=20160912#p01

はいその通りです。というか前者の意味なんだとすると、それはなんというかその、一般的に動的言語は全部ダメという結論になってしまうように思うのですけどどうでしょうか。あと変数名typoはJSなら “use strict” で防げたりする、といったこともあるので、型というよりは処理系や言語仕様の話じゃないかなぁという気も。

で、tensorのサイズの型付けなんですが、理論的には依存型（dependent types）で解決済の話題という気もする。確かリストのサイズを型レベルで覚えておいて、空リストへのheadをコンパイルエラーにする話とかあったよなー……と思って検索したら https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell みたいな話はあります。

ただまあ理論的な結果があるといっても、現実の問題に実際に適用してみたらいろいろな細かい問題はおこりうるだろうとは思うんですよね。convolutionみたいな引数はけっこうややこしいだろうし、embedded lookupみたいなので値域とサイズが入れ替わる場合とかもあるし。

あと自然言語処理みたいな応用例だと数万次元とかあるわけですが、サイズをナイーブにチャーチ数でエンコードしたらパフォーマンス的に大丈夫なんだろうか、とか。

まあそれなりにやってみたら面白いのでは、というのが素人考えですが、理論的には大して面白くないかもしれない。

“tensorflowの型付け” への4件のフィードバック

  1. – 前者の意味だとすると: つまらないというのは同感です。しかし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とかみたいな型計算しかしないやつ以外でよく聞く言語の機能としては見たことが無いと思うな、と
    – ちょっと勉強しなおしたり、あらためてほんの少し勉強してみたりしたけど、相変わらず斜め読みではどうにもむつかしくて身につかない話題です。全然頓珍漢なこと言ってる気がする。。
    – やはり型の話題には一切触れないのが正解という思いを新たにしました

    いいね

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

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

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

    いいね

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

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

    いいね

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

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

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

    いいね

コメントは受け付けていません。