!kiyoka.blog.2013_10 RSSPLAIN

Related pages: !kiyoka.blog.list
55555552222222222222222222222222222222122112122222222220222333333333333330333444444444444445555555555555555555555555555555555550555555555555555555555555555555555555555555555555505
5

kiyoka日記。NendoSekkaの開発や、最近思うことなど

5

最新10件!kiyoka.blog   過去記事一覧!kiyoka.blog.list

5

kiyoka.blog_header 

5

このブログを書いている人: 西山 清香(kiyoka) - twitter: @kiyokaEXT

5

5

 

5

 

2

kiyoka.2013_10_24[MacOS] MavericksにバージョンアップしてもX11を使う

2

 

2

無料と聞いて、MacBook ProのOSをLionからMavericksにバージョンを上げた。

2

「タダより高いものはない」というわけで、それなりの手間賃を払うことになった。

2

X11 serverがMountain Lionから非標準になって当然Mavericksでも動かなくなっているので、復活するところからスタートした。

2

 

2

普段は、X11プロトコルをsshで転送して北海道のDebianマシンと手元のMacOSXとを繋いでいる。

2
 
2
 X11 server                           X11 client
2
 
2
  [MacOSX]  ----- Internet -------  Debian/GNU Linux
2
 
2

 

2

用意するソフトウェア

2

XQuartzEXT 2.7.4 のdmgファイル。Lion付属のX11の代わりとして使える。

2
 ※ MacOSXのマシンからリモートのLinuxマシンには ssh でログインできる状態であること。
2

 

2

環境設定

2
XQuartzEXT 2.7.4をインストールする。
2

 

2
XQuartzを起動し、設定を行う。
2

 

2
 認証の設定
2

XQuartz_input

2

 

2
 キーボードの設定
2

XQuartz_security

2

 

2

 

2
XQuartzを再起動する(これで設定値が反映される)
2

 

1
MacOS X側の ~/.ssh/config に1行追加する
2
ForwardX11 yes
2

 

1
MacOS X側の ~/.bashrc に1行追加する
1
export DISPLAY=localhost:0.0
2

 

1

 

2

起動

2
XQuartzが起動していることを確認する
2

 

2
ssh -Y オプションを付けてログインする
2
$ ssh -Y remote_host_name
2
$ xterm &
2
 → xterm が起動する
2

 

2

キーボードの調整も完璧だし、やはりX11 serverはMacOS Xの上が一番良い。

2

 

0

comment (disabled)

2

2

 

2

 

3

kiyoka.2013_10_18[TaPL] 演習問題をやってみた

3

4274069117 型システム入門(TaPL)

3

TaPL読書会に向けて11章の演習問題をやってみた。

3
 TaPL_exercise 
3

TaPLの演習問題をまじめにやるのは結構大変だ。

3

 

3

どの演習問題も証明せよと書いてあるのだが、証明しようとするとけっこう時間がかかる。

3

付録の模範解答ページには証明の流れは書いておらず、例えば「構造的帰納法」を使うとしか書いてなかったりする。

3

ああでもない、こうでもないと寄り道してなんとか証明した気になっているが、これで合っているのかどうか。

3

 

3

読書会での答え合わせの場があるのが幸いです。

3

 

3

自分としては11章を読み終わったら、この本を卒業して、Nendoに型検査を実装する作業に時間を使いたいなぁと考えているんだけど…

3

 

0

comment (disabled)

3

3

 

3

 

4

kiyoka.2013_10_12[Lisp][言語] Lisperの楽園: 脳内モデルに一番近い島

4

2779598066_b9c6540175_m

4

タイトルが、リゾートのパンフレットみたいになっているのは御愛嬌。

4

 

4

どの言語よりもLispが自分に合っているようだ。

4

脳内モデルを現実世界にdumpする手段としてLispがストレスが少ない気がする。

4

 

4

Rubyはどうなのかと聞かれてもないのに答えると(笑)、Rubyはそんなに自分の脳にぴったりフィットする感じではないのだよねー。

4

熱狂的なRubyistの方々には悪いけれども、RubyコミュニティのパワーとRuby関連へのお金の流れ込むスピードは圧倒的なのでそこは利用させてもらうのだ。(腹黒いねぇ)

4

時にはまとまったコードをgemとして提供することもあるけれど、メインのプログラム言語としてRubyを選択することは無いかなぁ。

4

であるからしてNendoの「gemが使えるLisp」という路線は今後も健在なのだ。

4

4

 

4

 

5

kiyoka.2013_10_09[Lisp][言語] 処理系開発の効用

5
 このエントリは二年前くらいに書いたものなのでちょっと古いのだが、もったいないので公開。
5

 

5

新しい視点

5

オレ処理系 Nendoの開発は単に楽しいからやっているのだが、開発してみるとアプリケーション開発では得られない視点が得られる。

5

言語の中でもLisp処理系を作るのは貴重な体験だ。

5

Lisp処理系を作るためには、Lispの内部構造やプリミティブの制御構文などについて詳細に落とし込んで考える必要がある。

5

自分で考えた処理系がある程度動くようになるころには、特定の言語に依存しない抽象的な脳内モデルが生まれる。

5

自分は処理系を作って初めて明確な形を取るようになったが、Lispでプログラミングしただけでも脳内モデルが形成される人もいるかもしれない。

5

 

5

コードの中にlambdaの存在が見えるようになる

5

私の場合は脳内モデルとして、抽象的な lambda式の連鎖(lambda計算)として見えるようになった。

5

以前は、PHPでプログラムをする時はPHP、Rubyでプログラムする時はRubyの見た目に近い脳内モデルだったような気がするが、最近は全部lambdaになっている気がする。

5

そういえば、shiroさんのブログ記事にも似たような話があった。

5
 Island Life - グラフ指向理解EXT
5
  で、おもしろいなあと思ったのは、私はプログラムを考える時も頭の中には
5
  グラフがあって、プログラムはそのグラフをテキストとしてダンプしたもの
5
  になっている。WiLiKi:Lisp:S式の理由で書いたけれど、だからプログラムを
5
  書くときにいちいち頭の中のグラフを翻訳しなければならないプログラミン
5
  グ言語よりも、グラフを生に近い形でダンプできるLispの方がずっと書きや
5
  すい。
5
 
5
  でも非Lisperなプログラマに脳内グラフのことを話してみてもあまり賛同さ
5
  れないので、Lispを好むか好まないかの境目は案外そのへんにあるんじゃな
5
  いかという仮説を持っているのだけれどどうだろう。
5

 

5

lambdaの連鎖で見えていることを言葉で説明するのが非常にわかりにくいのも同じかなぁ。

5

図で描いたほうが良いのだろうな。

5

描いて説明したところで、フウンで終わってしまってセツナイので描かないが。

5

 

5

設計に役に立つこともある

5

例えば、RESTベースのWebAPIを考える時や、1ページを超える長い関数を追う時、それぞれのパーツがlambda単位(クロージャ単位)に分割して見えるようになった。

5

長いソース中だろうと、ブロックさえあればなんでもlambda化して切断面が見える能力。意識しなくてもコード中に切断面が飛び出して見えているような。

5

うまく言えないけど便利で強力な特殊能力だと思う。

5

これは設計時、リファクタリング時に威力を発揮する。もしかしてこれが悟り体験?

5

 

0

comment (disabled)

5

5

 

5

 

5

kiyoka.2013_10_03[Nendo] 副作用の無いコードの静的解析について(2)

5

前回の続き。( 前回の記事は、右上の窓から同じタイトルで検索してね )

5

 

5

Nendoにおける型付けについて

5
 4274069117  型システム入門 -プログラミング言語と型の理論-: Benjamin C. Pierce
5

によれば、静的解析をするということは、定義した評価規則と型付規則に従って評価をすることで全ての項を型付けできる。

5

Nendoに応用し、最低限その関数が「副作用」の無い関数かを検査できるようにしたい。

5

 

5

(1)ある関数が副作用の無い関数で構築されている場合は、もちろん副作用が無いといえる。

5

(2)さらには、関数内の束縛関数は破壊したとしても自由変数を破壊しないのであれば、それは副作用の無い関数といってよい。

5

 

5

(1)は自動的に判定することができそうであるが、(2)は人間が判断すればできるのではないか。

5

そうすれば、現実的なレベルの仕様になるのではないかと考えた。

5

 

5

型注釈について

5

Nendoでは上記のような基準から、「副作用無し」と「副作用有り」というどちらかの型で型付けする案を考えた。

5

プリミティブな関数に型を付与し、そこからブートストラップで全てのユーザー定義関数に型を付けていこうと考えている。

5

プリミティブな関数には副作用がある/なしを注釈する。 (型注釈用には :[コロン] が有力。 Typed Scheme: Scheme with Static TypesEXT を参考にした)

5
+ の場合
5
(: +   Pure)
5

 

5
car と cdr
5
(: car Pure)
5
(: cdr Pure)
5

 

5
set! と reverse!
5
(: set! Unpure)
5
(: reverse! Unpure)  ;; srfi-1
5

 

5

自動型付け

5

上記の型注釈が付いた関数を使って、関数を構築すると自動的に型が付与される。

5

少なくとも、Pureな関数だけが使用された関数はPureであり、それ以外は全てUnpureと判定すればよい。

5

 

5
(define (inc1 x)
5
  (+ x 1))
5
 => pureな関数
5

 

5
(define (fast-reverse! lst)
5
  (reverse! lst))
5
 => unpureな関数
5

 

5

感想

5

TaPLを読んでいるわりには、上記の理論を証明も何もしておらず直感でしか語っていないが、多分いけると思う。

5

 

5

COMMENTshiro

「定数でないグローバル変数を参照していない」という条件は必要じゃありませんか?

5

COMMENTkiyoka

おっと、グローバル変数がありますね。あとグローバル変数の一部だと思いますが環境変数もですね。

STDINとかSTDOUTとかは副作用の代表格ですね。

0

comment (disabled)

5