檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2011-09-20 (火)

try-catchの双対となる構造

| 18:57 | try-catchの双対となる構造を含むブックマーク

envコマンドの話

Unix/Linuxにenvというコマンドがあります。何も引数を付けないで実行すると環境変数を表示しますが、表示には専用のコマンドprintenvがあります。env特有の機能は、環境変数を一時的に変更してからコマンドを実行できることです。この変更は一時的で、envによるコマンド実行が終わるともとの環境に戻ります。

例えば、UTF-8の日本語環境でmanコマンドを実行するには、env LANG=ja_JP.utf-8 man ls とします。逆に、日本語環境でdateの英語表示を得たいなら、env LANG=en date とします。

$ echo $LANG
ja_JP.utf-8
$ date
2011年  9月 20日 火曜日 17:31:13 JST
$ env LANG=en date
Tue Sep 20 17:31:23 JST 2011
$ echo $LANG
ja_JP.utf-8
$

env - とすると、すべての環境変数がクリアされます。env - に続けて環境変数設定を付けると、設定された環境変数だけの環境によりコマンドを実行できます。

$ printenv
HOSTNAME=microapplications.net
TERM=xterm
SHELL=/bin/bash
HISTSIZE=1000
SSH_CLIENT=::ffff:119.242.17.217 54054 22
SSH_TTY=/dev/pts/0
USER=hiyama
LS_COLORS=no=00:fi=00:di=00;34:ln=00;36:pi=40;33:so=00;35:bd=40;33;01:cd=40;33;01:or=01;05;37;41:mi=01;05;37;41:ex=00;32:*.cmd=00;32:*.exe=00;32:*.com=00;32:*.btm=00;32:*.bat=00;32:*.sh=00;32:*.csh=00;32:*.tar=00;31:*.tgz=00;31:*.arj=00;31:*.taz=00;31:*.lzh=00;31:*.zip=00;31:*.z=00;31:*.Z=00;31:*.gz=00;31:*.bz2=00;31:*.bz=00;31:*.tz=00;31:*.rpm=00;31:*.cpio=00;31:*.jpg=00;35:*.gif=00;35:*.bmp=00;35:*.xbm=00;35:*.xpm=00;35:*.png=00;35:*.tif=00;35:
KDEDIR=/usr
MAIL=/var/spool/mail/hiyama
PATH=/usr/local/python/bin:/usr/kerberos/bin:/usr/local/bin:/bin:/usr/bin:/usr/X11R6/bin:/home/hiyama/bin:/sbin:/usr/sbin
INPUTRC=/etc/inputrc
PWD=/home/hiyama
LANG=ja_JP.utf-8
SHLVL=1
HOME=/home/hiyama
LOGNAME=hiyama
SSH_CONNECTION=::ffff:119.242.17.217 54054 ::ffff:219.94.153.157 22
LESSOPEN=|/usr/bin/lesspipe.sh %s
G_BROKEN_FILENAMES=1
_=/usr/bin/printenv
$ env - printenv
$ env - MYNEME=HIYAMA printenv
MYNEME=HIYAMA
$

環境変数の値を空にすると特定の環境変数だけをクリアできます。

$ printenv LS_COLORS
no=00:fi=00:di=00;34:ln=00;36:pi=40;33:so=00;35:bd=40;33;01:cd=40;33;01:or=01;05;37;41:mi=01;05;37;41:ex=00;32:*.cmd=00;32:*.exe=00;32:*.com=00;32:*.btm=00;32:*.bat=00;32:*.sh=00;32:*.csh=00;32:*.tar=00;31:*.tgz=00;31:*.arj=00;31:*.taz=00;31:*.lzh=00;31:*.zip=00;31:*.z=00;31:*.Z=00;31:*.gz=00;31:*.bz2=00;31:*.bz=00;31:*.tz=00;31:*.rpm=00;31:*.cpio=00;31:*.jpg=00;35:*.gif=00;35:*.bmp=00;35:*.xbm=00;35:*.xpm=00;35:*.png=00;35:*.tif=00;35:
$ env LS_COLORS= printenv
HOSTNAME=microapplications.net
TERM=xterm
SHELL=/bin/bash
HISTSIZE=1000
SSH_CLIENT=::ffff:119.242.17.217 54054 22
SSH_TTY=/dev/pts/0
USER=hiyama
LS_COLORS=
KDEDIR=/usr
MAIL=/var/spool/mail/hiyama
PATH=/usr/local/python/bin:/usr/kerberos/bin:/usr/local/bin:/bin:/usr/bin:/usr/X11R6/bin:/home/hiyama/bin:/sbin:/usr/sbin
INPUTRC=/etc/inputrc
PWD=/home/hiyama
LANG=ja_JP.utf-8
SHLVL=1
HOME=/home/hiyama
LOGNAME=hiyama
SSH_CONNECTION=::ffff:119.242.17.217 54054 ::ffff:219.94.153.157 22
LESSOPEN=|/usr/bin/lesspipe.sh %s
G_BROKEN_FILENAMES=1
_=/bin/env
$

例に挙げたコマンドラインをまとめておきましょう。

  1. env LANG=ja_JP.utf-8 man ls
  2. env LANG=en date
  3. env - printenv
  4. env - MYNEME=HIYAMA printenv
  5. env LS_COLORS= ls

例外付き計算とその双対

例外付き計算とグロタンディーク構成」に次のような図を載せました。

正常終了時には型Bの値を出力して、異常終了時には型Xの例外を投げる計算単位fです。例外をキャッチした場合は次のようになります。

双対性と環境付き計算」では、双対的な対応を示す次の表を挙げました。

例外 環境
出力 入力
直和 + 直積 ×
モノイド 余モノイド
余対角 ∇ 対角 Δ
始対象 0 終対象 1
例外型 環境型

この表の双対性に従い、例外処理とその双対を絵に描いてみます。

行きがかり上、例外型がEになって横っちょから飛び出していますが、左の絵が発生した例外をキャッチして次の処理gに渡す状況を表しています。左の図を180度回転したのが右の図です。右の図のEは環境型を意味し、fが使う環境をgが生成していることを示しています。「直和←→直積」の双対性を表すために色も変えています。青が直和、赤が直積です(「色付き絵算と分合律」も参照)。

念のために、左右の絵に出てくる計算単位(圏の射)のプロファイルを書いておきます。+:、:× は直和と直積の記号ですが、コロンの付いている側にそれぞれ例外型と環境型を書く約束です。

  • 左 f:A → B +: E
  • 左 g:B + E → C
  • 右 g:C → E×B
  • 右 f:E:×B → A

cotryとunclose

例外を起こすかもしれない計算 f:A → B +: E の例外をキャッチして正常出力 B + E にするには、f全体をtry-catchで囲めばいいですね。キーワードをtryだけにして、例外捕捉をしたfを try{f} と書くことにします。先の図の左側は、try{f};g と書けます。

双対的に、環境を参照するかもしれない計算 f:E:×B → A の環境を入力タプルの第一成分に含めて E×B としたものを cotry{f} と書くことにします。先の図の右側は、g;cotry{f} となります。

  • 左 try{f};g : A → C
  • 右 g;cotry{f} : C → A

cotry{f} では、fが使う環境をすべてgが供給しなくてはなりません。実用上これは不便なので、cotryを少し修正したuncloseという構成子を考えます。uncloseは次のように図示できます。

左側*1を縦に走るEは不変(イミュータブル)な環境です。各計算単位は、Eのコピーを受け取り必要ならそれを使います。fの場合は、型Eの値をそのまま使うのではなくて、gからの出力の一部であるXの値とEの値をφで計算した結果を環境とします。

演算 φ:E×X → E としては次を考えています(いずれも、X = E を仮定します)。

  1. Eの値とXの値を“マージ”する。このとき、Xの値を優先する。
  2. Eの値を捨てて、Xの値をそのまま使う。

この2つの演算をφとして選んだときそれぞれ、unclose{f}, unclose-clear{f} と表記することにしましょう。環境データをJSONリテラルで書いて、デカルトペアリングを <-, ->、始対象(集合圏では単元集合)の恒等射をunitと書くことにすると、先のUnixコマンドラインは次のように書けることになります。

envを使ったコマンドライン:

  1. env LANG=ja_JP.utf-8 man ls
  2. env LANG=en date
  3. env - printenv
  4. env - MYNEME=HIYAMA printenv
  5. env LS_COLORS= ls

uncloseとunclose-clearを使った圏論的な記法:

  1. <{"LANG":"ja_JP.utf-8"}, unit> ; unclose{date}
  2. <{"LANG":"en"}, unit> ; unclose{date}
  3. <{}, unit> ; unclose-clear{printenv}
  4. <{"MYNAME":"HIYAMA"}, unit> ; unclose-clear{printenv}
  5. <{"LS_COLORS": undefined}, unit> ; unclose{ls}

undefinedは、その環境変数が未定義であることを示します。

CatyScriptの構文では次のようになります*2

  1. [{"LANG":"ja_JP.utf-8"}, void] | unclose {date}
  2. [{"LANG":"en"}, void] | unclose {date}
  3. [{}, void] | unclose --clear {printenv}
  4. [{"MYNAME":"HIYAMA"}, void] | unclose --clear {printenv}
  5. [{"LS_COLORS": undefined}, void] | unclose {ls}

[追記]環境の注入は例外処理の双対なので、「シーケント計算と例外処理コード」と同じような方法で、uncloseを含んだ処理方式をシーケント計算の推論規則にすることができます。通常のシーケント計算では、正常処理と異常処理、入力と環境の区別をしないので、その点を補う必要がありますが、例外と環境付きの計算はシーケント計算と相性がいい体系です。[/追記]

*1:あー、また右と左を間違った。

*2:まだ実装はされていません。