Wednesday, 22 November 2017

Applicative Functor and Monoidal Functor

なんか、Haskell のMonadがApplicative を要求するようになっていて、Monad を作るのが面倒になって困っていたんですが、そもそも、

  なんで Applicative が必要なのか良くわからない

て問題が。

  http://learnyouahaskell.com/functors-applicative-functors-and-monoids

とか、まぁ、面白いんだけど、

  で、それって圏論的にはどうなの?

という疑問が。Functor は、

fmap :: ( a → b ) → f a → f b

で、これが関手の射の写像に対応するってのは、まぁ、わかる。だからなんなのってのは置いといて。

  pure :: a -> f a
  <*> :: f (a -> b) -> f a -> f b

こっちはなぁ。fmap の写像が関手、つまりHaskellのデータ構造に包まれてるみたいな感じ。

なのですが、MacLean には Applicative Functor とかなくて。で、

  https://stackoverflow.com/questions/35013293/what-is-applicative-functor-definition-from-the-category-theory-pov

これによると、圏の積の構造を保存するFunctorである、Monoidal Functor と同じなんだとか書いてある。MacLean だと Monoidal Functor は一章使ってある。それかぁ。面倒くさそうなの避けていたんだけど。

で、Monoidal Functor ってのは、

unit :: f ()
φ :: (f a , f b ) → f ( a , b)

のことだそうです。あぁ、まぁ、積を写像しているような感じ。

** :: f a → f b → f ( a , b )
** x y = φ ( x , y )

としても良いらしい。逆に、

   φ ( x , y ) = ** x y

ですね。要するに引数に出てくる積は Curry 化でなくせるというわけ。そういう風に、Monoidal Functor から直積をなくしたのが Applicative Functor ってことね。

実際に、Monoidal functor と Applicative functor の相互変換もできるんですが、ちょっとしたパズルみたいな感じ。Sets だから射とかも集合の要素としてとってこれるので、変換できるらしい。つまり、

  Sets 以外には Applicative Functor は無意味

な感じらしい。

ついでに Monoidal 圏と Monoidal Functor も Agda で1日で書けたんですが、忙しい時期にそんなことやってていいのか?

この後、Applivative law から Monodail law だすとか、その反対とか、Sets が Monodail 圏なこととか、いろいろやらないといけないようですが、ちょっと量が多い感じだな。


で、結局、Applicative Functor なんの役に立つの? ってことですが、まぁ、あんまり良くはわからないです。データ構造に写像も格納できて便利ってことかな。なんか最初の理解から進んでないぞ。

  http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/808b03184fd3/monoidal.agda

Monday, 20 November 2017

沖縄寒い


今頃で20度切るのは珍しいんですけどね。南国行きたいとか言っているバカものも見かけました。

まぁ、Ingress にはちょうど良いです。うちのtop agentの cena 女史が faction change というのが最近の話題かな。Double Top とはやるな。

少しこまめに実家に行こうキャンペーンで12月上旬に、また東京にいこうと考えてます。その代わり、年末年始はパスかな。プロシンが後ろにずれたので、そんな感じにしようかと。

Sunday, 19 November 2017

コンパイラの授業

いつもの授業ですけどね。途中から GCC とか LLVM とか読むわけですが、

  放置していたGCC版のCbCを最新に対応させるか?

というわけで、GCCとLLVMの最新のを、うちのrepositoryに merge! いや、これ自体は授業とは関係ないんですが...

GCCは4.6から7なので、いろいろ変わっているわけですが...

  ファイルの位置が変わっている

くらいかも。まぁ、そんなに簡単には移行できないだろうけどね。

GCCちょっと読んだので、来週はLLVMを読んで、その後は、12/1,2,3 で

  Rakudo ( Perl6 実装)

を読もうかと思っています。YAPC もあるしな。

Saturday, 18 November 2017

Windows 7 から Windows 10

まぁ、Windows とかロクなことには使ってないんですが...

  OS X Marverkics 上のVMware Fusion 8.5 上の Windows 7

だったんですけどね。Windows 7 な Disk full とおっしゃる。VMだが60GBもあればいいでしょ? 100GBまで拡張するか。と、思ったら、

  Snapshotを削除しないと拡張できない

え、てめーなにふざけたことをいってる。Snapshot こまめにとってるわけでないのですが、

  VMWF は Snapshot の削除にとっても時間がかかる

まぁ、取りあえず削除は放り込んで... でも Diskfull って変だよな。っで、なんとかなったんですが、今度は、

  共有フォルダに赤バツが付いてる

ぐ、なおらない。Windows って長く使ってると腐るんだよな。

そういえば、そろそろ Windows 10 にしても良いかな。それが罠だったわけですが...

Windows 10 は学科がライセンス保っているので、それをもらえば良いだけらしい。岡崎さんにDVDもあるとか言われたんですが「ないので、imageで」まぁ、それでも問題ないです。

で、image 落として、VMWare から入れるわけですが、

  立ち上がって「インストールするイメージがない」で止まる

あれ? どういうこと? 8.5 で Windows 10 問題ないはずなんだけど。でも、新しいVMWare Fusion 入れてもいいか! と思ったら、

  VMWare Fusion 10 は High Sierra でしか動かない

そこで諦めるべきだったんですが... いいや、ついでに High Sierra に上げるか。ところが、

  App store が開かない

ぐ。なにそれ。そこでいつもの、

  Shift 押しながら Safe boot

で、App store は治りました。そこから、High Sierra の install に。ちょっと待て。

  Time Machine を止めて、別なHDDをつなげておく

そろそろ切り替えるべきだからな。よしよし。で、

  問題なく High Sierra に

素晴らしい。そこで、VMware Fusion 10 を入れて。Windows 10が...

  このハードはリアルモードをサポートしてません CPUID Early

は? 何言ってんので、しばらくぐぐったところ...

  VMFware Fusion 10 は、2010 iMac では動かない

くそ〜 無駄足だったか。まぁ、それはMBPで使えば良いが... で、8.5 で Windows 10 が上がらないのはなんで?

  簡易インストールを諦めてみると…

Windows のライセンスを入れるところで

  ライセンスに対応するイメージがない

最初から言ってよ。なので、ライセンス無ならインストールできました。VMにinstallだとタイミングによって無効になったりするらしいが... こんなこともあろうかと、

  ライセンスは二つもらっていた

ので、二つ目のラインセスを入れて解決。長い道のりだった...

Windows 10 ですか? キーボードの配置がJISでUSにならないのを除けば快適です。Windows 7 より遅いだけ。右クリックが多用されるので、Mac のマウスだと使い辛いかな。

Wednesday, 15 November 2017

コインランドリー


なんか、最近、派手で綺麗なコインランドリーが流行りらしく。うちの近所にもできてました。

で、少し冷かしに行ってみたところ、

  河野先生ですよね

え? なんと、うちの卒業生が経営者らしく...

大学の勉強役に立った? と聞きましたが、普通にWebとかを使えただけで、直接には役に立ってないみたいです。

研究室にも、初期の頃のOBとか来てたな。ちょっと沖縄に戻ってくるのは早いんじゃない? とか思うけど、まぁ、それも良いか。

Monday, 13 November 2017

かばん壊れた


Twitter と同じこと書いてると言われるでしょうが、こっちにも書きます。年一回は壊れてる気がするよ。

バスから降りたら「バスっ」とかいう音とともにかばんが落下。もはや、いつものことなので驚きはしないんですが。

既に、付属の肩紐は使い物にならず実家の別なかばんの肩紐に交換済。なので、少し金具が元の違う。で、壊れたのは、肩紐側の金具かぁ。油さしておくべきだったかも。削れちゃうんだよね。

だいたい、革の方もリングになっているので、そこにOリングを通すのが良い。それが一番もつ。

  最初から、Oリングにしておけよ!

と思います。デザイン的にもそっちの方が良いと思うし。

なんだけど、Oリングあったかな。4Fの実験室にいけばあるんじゃないか? メイクマンいけばあるのは知ってるのだが... なのだが、山田さんが「ここになはない。前も買った」というつれない返事。予算で買う時には余計に買うんだよ。秋葉原で電子部品買う時には必ず余計に買っていた。すごすごと部屋に戻ったのですが、

  もう一度探したら、ロッカー置いてあったポーチの中にあった

旅行用のポーチでカミソリとか綿棒とか入っている奴。旅行には、Oリング必須だったのか。そうだろうなぁ。イギリスに行った時に既に、3.4kgのダイナブックをかばんで持ち歩いていたからな。

だた、キーホルダー用みたいな小さいやつなので、あまり保ちそうにないな。メイクマンにいくしかないか。少し余計に買うことにしよう。いや、既に買ってある可能性も高いな。

Sunday, 12 November 2017

論理式と方向

いつもの Agda の話題ですが、論理式には方向がない 例えば、

 a = b

と書いてあっても、a が出力とか b が入力とかない。一方で、関数(λ式)には方向がある

λ x → y

では x が入力で、y が出力になります。

Agda だと、数学的構造は record や data で書きます。record は積で and でつながったもの、data は排他的論理和で case 文の集合みたいな感じ。

で、Agda の library とかを見ると、record Hoge と record IsHoge とかが組で出てる。良くわからなかったんだけど、どうも、

record Hoge ( input : InputType ) where
field
output : OutputType
isHoge : IsHoge input output

record IsHoge ( input : InputType ) (output : OutpoutType ) where
field
property : ppro inupt output

みたいに使うらしい。filed は名前と型、つまり、名前の付いた変数とか論理式が来るわけですが、record の引数は入力、field には出力、つまり、その数学的構造で存在が主張されるものを列挙します。例えば、有界な実数の集合には最大値にになる極限が存在して上界というとか、そんなの。

その入力と出力は数学的構造の性質(公理)が要求されるわけですが、それらは論理式なので方向性はない。それを IsHoge にわけて書くという方式らしい。

こうすると、

lemma1 : (input : InputType) → Hoge input → ...
lemma1 input hoge = ...

とすると、Hoge i での IsHoge の性質が使えるようになる。つまり、

∀ input → ∃ output such that IsHoge input output

というわけ。Hoge の存在を示す時には、

lemma2 : (input : InputType ) → Hoge input
lemma2 input = record { output = ... ; isHoge = record { property = ... } }

という風にするらしい。なるほど。

で、今までにやった圏論(クライスリ圏とかLimitとか)を、これにそって書き直したんですが...

  仮定が余計とか、仮定が足りないとか

が若干でて、少しはまりました。一通り書き直して、だいぶ、見通しが良くなったみたい。普遍問題では入力は圏A,Bと関手Uで、それがUに対するLimitの存在につながるとか、ちょっとあやふやだったところが理解できたみたい。形式大事だな。

IsHoge のみで書くことも可能で、初期の頃のはそういう風に書いていて、必要なものは module input に書くとかしてたみたい。楽なんだけど、

Hoge → Fuga

みたいにならないで、

(x y z : ...) IsHoge x y z ... → IsFuga x w q

とかで、 x y z とかの仮定にいろいろ余計なものが入ったり、うっかり書きそびれたりしていたようです。

Programming 的には Hoge が interface で、IsHoge が実装だと言えないこともないかな。