東京は赤坂に行って来ました

型レベルプログラミングについて聞きに行きました。

つくばと東京はやっぱりそれなりに遠いなーと最近思う様に成って来たあたり。大学に入った頃はそうでも無かった様な気がするけど、あの時から事実としてそうだったのであればやっぱりその通りなのかもしれない。でもまぁTXが出来る前に比べれば大分良く成っているらしいので、これぐらいならまだまだ大丈夫だ。

一次会の自分用メモ　かなり偏りアリ

水島さんのScala

Scalaはぱっと見何を書いてるのかが分からないのが依然として問題であるなという気がしてならない。

落ち着いて考えてみると、割とズレたやり方をしていると言うよりも、既に確立している部分に合わせてる分ぱっと見が意味不明になっちゃってるんじゃないかなーと。

例えば

class Ref[T](private var value :T)
{
  def unary_! :T = value // 単項演算子 ! の定義
  def :=(newValue :T) :Unit = value = newValue
}

水島さんのGenerics(1)を手写し

とかは、Genericsらしいのですが、Scalaの中での型(クラスってそういえば型だっけみたいな...)をparametarizeして持ちましょう！という。だからこれ或る意味でパタンマッチになってるんですな。というのは

val ref = new Ref("Foo")
println(!ref)
ref := "BAR"
println(!ref)
ref := 1 // Error

いややっぱり今書きながら考えてた事とちょっと違ってたw　本当はRef[String]("Foo")とかかなーと思ってたんですけど。まぁでもFooからStringが推論出来るからTはStringに束縛されちゃうのかしら。

//実際にやってみた

class Ref[T](private var value :T)
{
  def unary_! :T = value
  def :=(newValue :T) :Unit = value = newValue
}

object Test
{
  def main( arg :Array[String] ) = 
  {
    val ref = new Ref[String]("Foo") // explicitにも書ける
    println(!ref)
    ref := "BAR"
    println(!ref)
    //ref := 1
  }
}

で、Genericsの2が見辛いなーと思っていたのだけど

class Ref2[G[_], T](private var value :G[T])
{
...
}

これ最初は、コンテナっぽい型をGに束縛する(例えばArray[Int],List[Int])のかなーと思っていたけど、このGはGenericsなGで、それこそGにRefが束縛されるかも分からんわけですにゃとか。(そもそもArrayもListもGenerics(なのかは知らないけど)なので、そりゃそうだ)

計算をtyped λ-calculusという「値と型」という、まぁ種々のプログラミング言語で洗練された手段でやるのでは無く、「型と型の型(kind)」を使って行う(まぁここでやっと型レベルプログラミング(そもそもλ-calculusだと型無いですし))という事にスライドしていく。

でまぁ、C++とかは異常な感じにtemplateが成ってるので、そうでないScala(水島さんはScalaで型レベルプログラミングとかやるのは　外道　と口をすべらせてしまっていましたがw)で如何にしてやるんじゃ！という話にスライドしていくのでした。

純粋にScalaではこう出来るという事が知れて面白かった。

C++

C++って弱二階述語論理(?)ですかみたいな...
久々過ぎてああそういえばこんなんでしたっけという。

ところで、C++でExistential Typeってどうやるんだろうなーと思っていました。勿論値レベル計算でvoid*とかでType Erasureとかは無しで。

keigoiさんのfundeps

HaskellでPeano Numberを普通に表現しようと思えば、次の様に出来ますね。

data Peano = Zero | Succ Peano

add Zero a = a
add (Succ a) b = Succ (add a b)

peano2val a = peano2val' a 0

peano2val' Zero acc = acc
peano2val' (Succ a) acc = peano2val' a (acc + 1)

ところでまぁ、PeanoはTypeなんですが、ZeroはPeano型の要素です、SuccはPeano型の値(ZeroとSuccですが)を取ってPeano型の値を返す、値を取って値を返す関数(このType Signatureは Type -> Typeになりますが)で、これじゃダメなんですよ。

例えば、この状況で0をZero、1をSucc Zero、2をSucc (Succ Zero)とした所で、全てPeano型になってしまう。
そうじゃなくて、0はZeroという型で、1はSucc Zeroという型で、2はSucc (Succ Zero)という型で、別々の型になっていて欲しい。

じゃあType Levelでどうやりたいか、ってなると

{-# OPTION -fglasgow-exts #-}

data Zero :: * where
  Zero' :: Zero
data Succ a :: * -> * where
  Succ' :: a -> Succ a
...

この時、Zero'はZeroと同じく型、Succ'は型を取って型を返す関数(Type Signature は Kind -> KindとかSort -> Sortとか)なのでSucc' Zero'はSucc Zeroとなります。

じゃあ足し算をどう実装するかという事になるのですが...

add :: * -> * -> *
add Zero' a = a
add (Succ' a) b = Succ' (add a b)

add (Succ' (Succ' Zero')) (Succ' Zero') ->
Succ' (add (Succ' Zero) (Succ' Zero'))

add (Succ' Zero') (Succ' Zero') ->
Succ' (add Zero' (Succ' Zero'))

add Zero' (Succ' Zero') -> (Succ' Zero')

↓
Succ' (Succ' Zero')
↓
Succ' (Succ' (Succ' Zero'))

とかは出来んので、じゃあFunctional Dependencyを使って

{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE UndecidableInstances #-}

data Zero = Zero
data Succ a = Succ a

class Add a b ab | a b -> ab where
    add :: a -> b -> ab

instance Add Zero b b where
    add = undefined

instance (Add a b ab) => Add (Succ a) b (Succ ab) where
    add = undefined

とか書くんですが、keigoiさんの説明が上手でした。スライドを是非見るべきであるとか。私もくだんの論文読もうっと。

それと、undefinedとか上の定義では使ってるけどそれってどうなのよみたいなのは、だってこれ"型の型"と"型"における計算をAdd自身で定義している(fundepsで計算)んだからaddとかいうダミーの定義は実際要らんので(型レベル計算に値レベルの計算持ち込んでも、ドラゴンボールで言うところのヤムチャ視点というか)undefinedでさよなら。

別に定義しても良いですけど、使いません。型さえ合わしておけば良いです。

shelarcyさんのtype families

分からん

これは分からん！！スライド後で読み直そう。

kinabaさんのD

D言語は標準ライブラリにあの類の関数があるのか・・・。

凄いすんなり分かってしまったので、それは逆に恐ろしかった。
後はCTFEとShadow Type

処理系入れて色々試してみる
(そういえばdmdがIntel Mac向けの新しいの出してたっけ

ikegamiさんと418

水島さんが428買うらしいのですが、筑波大学WORDにはWiiは無いので、これはしまったなーとかずっと思っている。現在進行形。

難しい事考えないで(つまり証明がががとかでなく)依存型したいならCayenneじゃないですかねやっぱり。

関係無いですが、オプーナもやってみたいです。

ytさんとG'Caml

ytさんは雑談会の時にもお会いしたんじゃないかと思ったらやはりそうでした。

G'Camlは初耳だったのですが、camlspotterさんによる実装らしいです。

インタプリットタイムで型だけを持ち回したいので、Obj.*を使いまくると。
Phantom Typeでどうこうしていけば良いんじゃないかと思ったものの、以下略

(以下略部分は、それOlegさんで http://okmij.org/ftp/Haskell/number-parameterized-types.html)

二次会

ざっと

会場への移動途中で、ikegamiさんにAgdaとAISTの関係性について教えて貰う

書きながら教えて貰った事を思い出したのですが、AgdaにはかつてGUIのエディタ(というかIDE?)も付いていたようです。
それの元になったのがHaskellによるGUIプログラミング/パラダイムについて書いた論文であるとか。

二次会でkeigoiさんとkinabaさんとsoutaroさんと一緒の卓に
kinabaさんの最近の研究についてちょろりと説明してもらう大いに分からない
keigoiさんがλ計算のπ計算への変換を教えてくれた。評価戦略に応じて異なる変換。これは面白そうなので読む
soutaroさんがHigher Order Origamiの存在(実はこれはデマ(というか...))を教えてくれる。

筑波大学の人だとOrigamiがちょっと分かると思うのですが・・・SCOREとOrigamiの組み合わせでググると雰囲気が掴めます。
この後大学につくまで私は頭の中で度々first-order origamiについて考えていました。

Epigramの"Why Dependent Types Matter?"を読んでいると思ったらCurry-Howard対応を調べていて、FelleisenのCオペレータ(これはtyped λ-calculusでのCPS translation + Continuationをcaptureして取りあえず関数に渡してあげる)というのが二重否定除去に対応してるんですが、事実は分かったけどなんかへんなのーと思っていたら、何故かPrologの周りに居ますとか言ってみた。

今思えば、そもそもPrologに関わったのは大阪さん会の時が初めてだったので、この馴れ初めはウソと言えばウソだ・・・。でも今何もやっていない事は事実

卓でPPIM(Mって何?)の存在を告知してみた。soutaroさんが釣れたかもしれない。
fundepsって勝手に型クラスの後ろで探してくれるのと、単一化してくれてるっぽいのでPrologぽいですねと言ったら違うから論文読もうぜみたいな。読みます。
soutaroさんに、私みたいな馬鹿野郎の為に輪読会をしてくださいよーと言ったら、やってあげましょうと言ってもらえた。やった。
NyaRuRuさんのD論が、私にはさっぱり分かりませんでした・・・。
bonotakeさんと双方向でお互いの顔と名前(ハンドル)を一致させた以前は仕事(研究)でHaskellを使っていたそうです。何の研究をしていたのか聞きそびれたので今度お会いした時に
ITproの記事ベースでshelarcyさんに質問する会をbonotakeさんが現実のモノに!! -> http://atnd.org/events/580
bonotakeさんをPPIMにお誘いした。
shelarcyさんから最近のGHC処理系の最適化に関する話を聞きだす。Cmmとかバックエンドの話も。GHC-As LibraryとかGHC APIの話。

Cmmはそこまで詳しく知らないので(むしろ言語表層だけ知ってる程度)これはお勉強だ。

λ-cubeとL-cubeと二階述語論理とCurry-Howardとかをごっちゃに混ぜた様な質問をsakaiさんにしようと思っていたのを完全に忘れていたのでこれまた今度お会いした時に。
人が多くても結局少しの人としか話せなかったのが残念かなーとか。

取りあえず帰りはsoutaroさんに藤田の公理(折紙公理、Huzita's Axiom)を教えて貰ったので、高階折紙とはなんであろうかをまた考えていたのだけど「研究としては」(少なくとも未だ)無いらしい。うえー。

Origamiについて興味がある人は、次のpaperが面白いかもしれません。
http://www.ipl.t.u-tokyo.ac.jp/jssst2006/papers/Ghourabi.pdf

Pointという紙上の点集合と、Lineという辺集合と、同値関係、および幾つかの関数と述語で説明していて、その意味でfirst order predicate logicだ、と書かれています。

後は
http://ja.wikipedia.org/wiki/%E6%8A%98%E3%82%8A%E7%B4%99%E5%85%AC%E7%90%86

私としては、紙を折り曲げるという行為は紙に折跡を残すという意味においてside-effectがあるとか考えていたのですが・・・。
無理矢理typed λ-calculusと対応付けようと思ったもののうまくいかねーなーとか思ってるうちに、いつの間にか寝てました。

とかが4/18のまとめ。