method dependent types と implicit parameters の相性について

scala

簡単に解説してみます。間違いがあったら教えてください。

Agda は依存型を扱える言語です。本題じゃない部分なのでかなり in-formal な説明をしてしまいますが、所謂静的型付き言語でいうところの「型」が first-class value として扱える言語だと思ってください。型も値のように扱えるということです。

例えば Scala で恒等関数を書くと以下のようになります。

def id[A](a: A): A = a

一方 Agda で素朴に書くと以下のようになります。

id : (A : Set) -> A -> A
id = \A a -> a

Scala では型は「型引数」として通常の引数とは別に与えられますが、Agda の場合は型も値と同じように普通の引数として扱われています。

とはいえ、一々型を渡してやるのは正直めんどくさいわけです。

id Bool true

値を渡してるんだから型くらい勝手に推論して適当に埋めといてよ、というときには以下のように書くことができます。

id _ true

しかし、これでもまだ少し面倒くさい。そもそも型渡してるけど、別にシグネチャ上必要になるだけで型触ってないし。そこで Agda の "Implicit Arguments" という言語機能を利用することができます。

id : {A : Set} -> A -> A
id = \a -> a

これで以下のように書けるようになります。型に相当する引数部が、Scala の implicit parameters と同じように、勝手に解決されて埋められるからです。

id true

なんだ Scala の implicit parameters と大して違わないじゃない、と思われるかもしれませんが、一点非常に大きな違いがあります。（実際には Agda のは unification ベースで解決してるはずなので、機能としては全然違うと思うのですが）それは Scala の implicit parameters は必ず引数リストの最後に書く必要があるのに対し、Agda の implicit arguments は任意の場所に書くことができる、という点です。

はい、既に長いですがここからようやく本題です。method dependent types には制限があります。それは「依存する引数が必ず引数として先に現れないといけない」というものです。つまり以下のようなことです。

def f(c: Context)(t: c.Tree): c.Tree = c // ok
def f(t: c.Tree)(c: Context): c.Tree = c // error: illegal dependent method type: parameter appears in the type of another parameter in the same section or an earlier one

この制限は implicit parameters と大変相性が悪いです。というのも、implicit parameters は前述の通り、引数リストの最後の書かなければならないためです。

def f(implicit c: Context)(t: c.Tree): c.Tree = c // ill-formed

困りました。というわけで、ざっくりとした説明ですが「Agda のように任意の位置に implicit parameters を書けるようにしよう」というのが、ツイートで参照されているブログでの提案なわけです。

Problem #2 は apply メソッド明示して呼び出すようにしなよとしか思わないのですが、Problem #3 は中々難しい問題で、まあ各自で適当に読んでください。おしまい。

お仕事を探しています

misc

追記：四月からしばらくのお仕事が決まりました。ありがとうございました。

あけましておめでとうございます。今年もよろしくお願いします。新年一発目で求人エントリ書くことになるとは…
まず最初に注意書きです。かなり面倒な人間の、かなり面倒な求職なので、そういう人間を抱えたくない、抱える余裕がない、という方には読んで頂かなくてもいいと思います。技術的に面白いエントリでもありません。ではちゃきちゃきと始めます。

Read more

COMFRK VOL.4 始まります（CV:田村ゆかり）

scala javascript misc

COMFRK は今年の冬も出るのです。出るのです！去年に同じく三日目「東Y16a」です。既刊もあります。

今回は、Scala のマクロを利用して、Scala コードから Javascript コードを生成するお話を書きました。
ちょっと尺とか何も考えずに書いたのでごにょごにょ…

買ってね〜。

IntelliJ Idea で scala 2.10-RC の macro/reflection について調べるためにしておくと良い設定

scala

情報量ほとんどないんですが、一応書いておきます。生存報告のようなものです。

普通に新規に Scala のプロジェクト作っても、デフォルトの設定だと Project Structure -> Modules -> Dependencies -> scala-library には scala-reflect.jar も scala-reflect-src.jar も scala-compiler.jar も scala-compiler-src.jar も入ってないと思うのですが、入れると色々捗ります。どうでもいいなこれ…

あと、結局 Scala 勉強会 in 本郷の第 91 回でもどうでもよさげな発表をしたんですが、個人的に資料がイマイチ（土壇場で加えた変更と追加何故か入ってなかったし…）なので、まあどうでもいいと思います。

おしまい。なんだこれは。

Scala 勉強会 in 本郷で色々発表してきました

scala

88 回、89 回、90 回と発表してきました。

基本的に勉強会というのは、時間の割にはそんなに勉強にならないので、どうせなら発表すべきだと思ってるのですが、結構疲れちゃうし、難しいですね。発表内容も半分は仕事内容に関係してるので、発表のための特別勉強したとかもないし、うーん…？まあいいか。


88 回では Play 2.0 の Action と BodyParser について学ぼう ということで発表しました。フレームワークというのは基本的には便利なものなのですが、自分がフレームワークの作法に従って書いているものが結局なんなのか、それを知らずにいるのって気持ち悪いよね…？という気持ちがあって、それをちょっと形にした、というような感じです。Play 2.0 を知らない人にもある程度わかって貰えるようにしたつもりだったのですが、どうかなあ…そんなわけで内容はとても軽いです。


89 回では「sbt + android-plugin を利用して、アンドロイドのテストプロジェクトをうまくビルドするには」について発表というか話しましたが、ちょっと話が難しすぎでしたねスイマセン…Android 開発したことない人は完全に置いてけぼり、どころか、なんなら開発したことある人も置いてけぼりだったと思います。反省。でも頑張った成果だから、伝えたかったんですよ…！
スライドなどはなくて、github にあがっている成果物を見ながらの発表でした。"Step-by-step how to build android test projects is written by scala" とあるように、リポジトリ内のコミットそれぞれが、資料というか解説みたいになってます。逆にいうと、これ見れば完全な sbt の設定が書けるかというと、まあそうでもないかもしれません。
面倒なので書かなかった、かつ話したくなかったのですが、何故テストケースのクラスのロードだけがうまくいかないのかという id:tototoshi さんからの鋭い突込みがありまして…それは、同じクラスローダーを使ってはいるんだけれど、ロードの方法が違う（最早よく覚えてないけれど Class#forName とか使ってたはず）ことがどうやら原因らしいんですね。いや違っててもクラスローダー同じなんだから、一部のクラスだけロードできないのはおかしいだろうという主張は尤もなのですが、とはいえそれは実装次第だろうということもあって、深追いはしてません。なんせ vm は jvm でなく dalvikvm で、ライブラリの中身も別物ですからね。何よりそこを調べても問題解決には影響しないというのが大きいというか。仕事としてやっていたので。
あとこれは 86 回で資料もなしに少し話した気がするのですが、アンドロイドのライブラリプロジェクトのテストプロジェクトについてもやはり結構面倒で（通常のテストプロジェクトに比べたらましだけど）、いい加減きちんとまとめられるといいなと思いつつ、何もできていなくて人間力の低さの証明みたいに…嗚呼ッ。まあぼちぼち…ぼちぼち…（こういうのは絶対やらない）。
しかしどれも結局 android-plugin が最新の sdk のビルドプロセスに追いつけてないのが原因なので、プラグインのほうで頑張ってちゃんと欲しいですね正直。でもやる気ないっぽいんだよなあ。あーあ。


90 回では第一回社内 Scala 勉強会（一部抜粋）という、使いまわしかと思ったら実は本邦初公開みたいなのを発表しました。
Scala の型制約を主題にしつつ、Scala で何ができるようになるのかみたいなのと、それらが何を意味するのか、という二点を伝えたかったんですが、質問とかあんまりなかったし、伝わったのかなあ、うーん…という感じだったのですが、割りと褒めてくださる人も多くて、それで一念発起して今これを書いているというような感じです。
内容に関しては、資料がそこそこそれだけで完結するようになってるので、まあ気になる人は見てください…
あとどうでもいいことですが、社内勉強会が中止になって、いつやるかもわからない状態なので、評判良かったのは実際かなり救われました。


疲れた。


追記：誤解を招くと良くないので補足。View Bounds についでですが、この制約では Nominal Subtyping で許容されるような型も許容されます。単一継承のオブジェクトシステムでのアップキャストは安全であり、暗黙に行われるため、だと思ってください。仕様的にそんな雰囲気だったはず…
なので、下のような型制約を書く必要はないです。

def f[T <: U <% U](...) = ...

Re:小分けの処理とまとめた処理をまとめたい

javascript

http://d.hatena.ne.jp/RiSK/20121027/1351317259

頑張って javascript 語で書くよん。

function string_to_write_proc(str) {
  return function() {
    document.write(str);
  };
};

function proc_binop(lhs, rhs) {
  return function() {
    lhs(); rhs();
  };
};

function string_binop(lhs, rhs) {
  return lhs + rhs;
};

["mizuiro", "sorairo"].map(string_to_write_proc).reduce(proc_binop).call();
string_to_write_proc(["mizuiro", "sorairo"].reduce(string_binop)).call();

要は文字列という半群を構造を保ちつつ処理君にして畳みこむか、文字列を畳み込んで処理君にするかの違いみたいな。

果てしない自明くささのある話だな…うーん。

ていうか本当は reduce とかしたら stack がーってなるので sequence みたいなのが求められるわけですが、まあそういうのはいいでしょう…

疲れた。タイピングは疲れる。あと体が痛すぎて頭が痛くなってきた。