日々の流転

λ. Text.Regexで日本語が扱えない問題を鬼車で解決

久しぶりのHaskellネタ。GHC-6.2.2現在のText.Regexでは非ASCII文字はまともに扱えないことに段々むかついてきたので、鬼車(Oniguruma)を使って解決してみた。

Current(GHC-6.2.2) implementaton of Text.Regex doesn't handle full range of Unicode. It can handle only ASCII (or maybe LATIN-1) characters which is a very small subset of Unicode. This limits the usefulness of Text.Regex since there are many natural languages (such as Japanese) that need non-ASCII characters.

Therefore I modified the implementation of Text.Regex to use Oniguruma(鬼車) which is a very powerful regular expression library. To a wonderful thing, it supports UTF-32. So that the new implementation can handle full range of Unicode.

for Hugs98-Mar2005 (updated 2005-05-07)

1. Install Oniguruma version 3 (or later).
2. Apply hugs98-Mar2005-oniguruma3-2.patch to the Hugs source tree.
3. Run autoconf in the top directory and `libraries/base' directory.
4. Build hugs as usual.

for GHC-6.4 (updated 2005-05-04)

1. Install Oniguruma version 3 (or later).
2. Apply ghc-6.4-oniguruma3-1.patch to the GHC source tree.
3. Run autoconf in `libraries/base' directory.
4. Build GHC as usual.

for GHC-6.2.2

ghc-6.2.2-onigd20050204-1.patch.gz
このパッチをあてて、autoconfを実行し、./configure に --enable-oniguruma を指定してビルドすると鬼車が使われるようになります。

λ. サブタイプと代入

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal22.html#categorymisc5

私はOCamlの型システムについては全然知らないので勘違いしているかも知れませんが、この問題は単にその型システムが安全でないというだけのように思えます。

安全な型システムであれば、型Aが型Bのサブタイプであることの必要条件として、少なくとも、Bのインターフェース中の正(負)の位置に現れる全ての型について、Aでの対応する型がそのサブタイプ(スーパータイプ)になっていることを要求するはずです。

この例では、型 <n : <y : b>; m : a> のフィールドnが代入可能ということは、この型が setN: <y : b> -> () というメソッドを持っているのと同じとみなせるので、型 <y : b> は負の位置にも現れていると考えるべきでしょう。したがって、<n : <x : a, y : b>; m : a> が <n : <y : b>; m : a> のサブタイプであるためには、<x : a, y : b> が <y : b> のスーパータイプである必要があります。しかし、これはいくらなんでも成り立ってませんよね?　それにも関わらず <n : <x : a, y : b>; m : a> を <n : <y : b>; m : a> のサブタイプと認めてしまうような型システムであれば、実行時にエラーが起こって当然だと思います。

ちなみに、サブタイピングをサポートする関数型言語の他の例としてO'Haskellがありますが、このようなコードはちゃんと型エラーになります。(以下に出てくるCmdはIOモナドみたいなものです)

-- type constructor (kind * -> *) (variance +)
struct Y y =
   getY :: Cmd y
 
-- type constructor (kind * -> * -> *) (variance + +)
struct XY x y < Y y =
   getX :: Cmd x
 
-- type constructor (kind * -> * -> *) (variance 0 +)
struct S n m =
   getN :: Cmd n
   setN :: n -> Cmd ()
   getM :: Cmd m
 
-- OK
cast1 :: S a (XY a b) -> S a (Y b)
cast1 x = x
 
-- NG
cast2 :: S (XY a b) a -> S (Y b) a
cast2 x = x
{-
ERROR "Test.hs" (line 21): Type error in variable
*** term                : x
*** type                : S (XY a b) a
*** does not match      : S (Y b) a
-}
 
-- NG
test :: S (XY a b) a -> Y b -> Cmd ()
test x y = x.setN y
{-
ERROR "Test.hs" (line 31): Type error in function application
*** term                : (.setN)
*** type                : S a b -> a -> Cmd ()
*** constraints         : Y c < a, a = XY b c
*** because             : variable has conflicting bounds
-}

λ. オブジェクトはレコード型か？

生存記録(2005-02-12) では「レコード型との違いは、自己参照できる点だと思う」と書かれているけど、任意のレコード型Aの上に不動点結合子fix_A:(A->A)->Aが定義されている世界ならば、自己参照してるレコードなんていくらでも定義できるし、あまり本質的な違いではないような気がする。

……考えていて、ふと、オブジェクトがレコード型と同一視されるのは、メッセージが(引数の違いを無視すれば)高々有限個しか存在しないからではないかと思った。高々有限個しかないから、関数をフィールドとするレコードで表現できてしまう。では、もしメッセージが有限個ではなく、しかも何らかの代数構造(プロセス代数的な何か?)を持っていたとしたらどうだろうか?

λ. OOの型理論の本

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal22.html#categorymisc7

読んだことはないですが、最も参照されているのは "A Theory of Objects", Martin Abadi and Luca Cardelli だと思います。

λ. ワカメチョコ

わろた。

λ. 禁苑の黎明−Twilight in the forbidden city

メモ。酔夢ing voice (2005-02-12) と 愛・蔵太の気ままな日記 (2005-02-13) より。

λ. g の逆関数が存在するときに Anamorphic Fusion が成功するか

gに逆関数が存在するなら、ψ' = F(g^-1) ∘ ψ ∘ g とおけば、Fusionできるのは自明。なーんて簡単な話では無いのだとは思うけれど……

λ. レコード型＋不動点演算子で late binding を表現

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal.html

不動点演算子を作用させた時点でthis.methodが決まってしまうのはその通りですが、不動点演算子を使うのはどうせ具体的な値を定義する段階でなので、一般的なOO言語の late binding を表現するにはそれで十分です。

具体的には、AのコンストラクタをA->Aの形で表現しておく約束にしておいて、それにfixを適用することでAのインスタンスを定義することにすればOK。簡単な例をHaskellで書くと以下のような感じ。Aを継承して一部のメソッドをオーバーライドしたBを定義するのを模倣している。

fix :: (a -> a) -> a
fix f = let x = f x in x
 
data A
    = A
    { op    :: Int -> Int
    , twice :: Int -> Int
    }
 
-- Aのコンストラクタ
ctorA :: A -> A
ctorA this
    = A
    { op    = \x -> x+1
    , twice = \x -> this `op` (this `op` x)
    }
 
-- Aのインスタンス
objA :: A
objA = fix ctorA
 
-- Haskellには残念ながらサブタイピングが無いので (T_T)
type B = A
 
-- Bのコンストラクタ。opをオーバーライド。
ctorB :: B -> B
ctorB this = super{ op = \x -> (super `op` x) * 2 }
    where super = ctorA this
 
-- Bのインスタンス
objB :: B
objB = fix ctorB

試してみると、objB `twice` 10 = 46 = (((10+1)*2)+1)*2 となって、AのopではなくBのopが呼ばれていることが分かる。

なお、この方法だと <m_i : B_i>_i∈I は μX.[m_i:X -> B_i]_i∈I ではなく、[m_i: B_i]_i∈I で表現されるので、サブタイピングに関しても何の問題も無い。

λ. るびま 0005号

.

λ. 不動点と有限直和を持つCCC

A Model of Intuitionistic Affine Logic from Stable Domain Theory, Torben Braüner によれば、A Note on Inconsistencies caused by Fixpoints in a Cartesian Closed Category. Huwig, Hagen, Poigné で、「不動点と有限直和を持つCCC(Cartesian Closed Category)は、一つの対象と一つの射しかない圏と圏同値」(a cartesian closed category with fixpoints and finite sums is equivalent to the category with one object and one arrow.)が示されているそうだ。この論文はWeb上には公開されてないみたいだし、メディアセンターで取り寄せるのも面倒なので、その前にちょっと考えてみる。

まず、A Model of Intuitionistic Affine Logic from Stable Domain Theoryから不動点の定義を引っ張ってきておこう。

不動点

有限直積を持つ圏は、 任意の射 f: A×B→B について 射 f^†: A→B が存在して f^† = f o (id_A×f^†) o Δ_A (ここで Δ_A: A → A×A は対角化写像 Δ_A = <id_A,id_A>) を満たすときに、「不動点を持つ」と言う。 また、この f^†: A→B を f: A×B→B の不動点と呼ぶ。

なお、CCCが不動点を持つのは、 任意の対象Bに対して不動点演算子 Y_B: B^B → B が存在して、 任意のf: A×B→B について Y_B o curry(f) が f の不動点に なっている時かつその時だけだそうだ。

有限個の対象の直和が存在すると言っているので、ゼロ個の対象の直和、すなわち始対象0も存在する*1。そして、p2: 1×0→0 の不動点 p2^†: 1→0 は !₀: 0→1 の逆射になっているので 0 ≅ 1。 一方、uncurry(!!_0^A): 0×A→0 は !!_0×A: 0→0×A の逆射になっているので、 0×A ≅ 0。 したがって、任意のAについて A ≅ 1×A ≅ 0×A ≅ 0 なので、全ての対象は同型。

次に、任意の対象X,Yを考える。Xから0への同型射をα: X→0、1からYへの同型射をβ: 1→Y とすると、任意の射 f: X→Y について β^-1 o f o α^-1 = !₀ が成り立ち f = β o !₀ o α であるので、射 X→Y はただ一つだけしか存在しない。

ここまでで、この圏は全ての対象が同型で、どの対象X,Yの間にも射は一つだけしか存在しないような、つまらない圏でしかないことが分かった。ちなみに、ここまでは “Conceptual Mathematics: A First Introduction to Categories”, F. William Lawvere, Stephen H. Schanuel の知識だけから言えるはず。最後に、この圏が一つの対象と一つの射しかない圏と圏同値であることは……省略。

……と、ここまで書いてきてなんなんだが、なんか変な気がするなぁ……

λ. 不動点と有限直和を持つCCC (2)

具体例として、全ての pointed CPO と全ての正格な連続関数からなる圏を考えてみる。この圏では 0 = 1 = {⊥} となっていて直積も存在する。もし、冪(exponential)が存在してCCCになっているなら、さっきの議論からこの圏の全ての対象は同型だということになるけど、これは矛盾。したがって、この圏には冪は存在しないはず。

正格な連続関数からなるpointed CPO [A→B] は冪にはならないのかなぁ、と一瞬考えてしまったけれど、さっきの議論から簡単な反例を抽出できる。Aを2要素以上からなるpointed CPOとすると hom(0×A,0×A) ≅ hom(1×A,1×A) ≅ hom(A,A) は2個以上の要素を持つ一方で、hom(0,[A→0×A]) は1要素しか持たないので、同型にならない。

[2005-03-30 追記] ちなみに、A⊗B = {(a,b) | a∈A, b∈B, a≠⊥, b≠⊥} ∪ {⊥} と定義すると、-⊗A は [A→-] の左随伴になっている。つまり、この圏は⊗をモノイド演算とする symmetric monoidal closed category になっている。

λ. 不動点と有限直和を持つ distributive category ?

[2005-03-27 追記] ところで、最初の議論で使った 0×A ≅ 0 は distributive category の定義に含まれるので、この議論での CCC という条件は distributive category に弱めることが出来ると思う。

λ. 『竹島は日韓どちらのものか』, 下條 正男

を読んだ。

λ. 竹島CM

メモ。

λ. OCaml入門 (0)

OCamlの型システムについて良く知らずにあれこれ言うのもアレなので、この機会にOCamlについて少し勉強してみようと思った。とりあえず、現時点での印象は

• 整数の加算を「+」、浮動小数点数の加算を「+.」などと書き分けるのは面倒そー
• 多相バリアント(Polymorphic variants)と多相レコード(Polymorphic records)は便利そー

ってくらい。

λ. 地震

そういえば今朝の地震は揺れたなぁ。目が覚めた。

λ. OCaml入門 (1): 複数のパラメータを持つ型

複数のパラメータを持つ型の例があまり見当たらず、どう書くのかしばらく悩んだ。type 'a 'b hoge = Hoge of 'a -> 'b ではなく、type ('a, 'b) hoge = Hoge of 'a -> 'b と書く。

調子に乗って、generalized rose tree のデータ型を定義しようと type ('f,'a) grose = GBranch of ((('f,'a) grose) 'f) と書いたら、これはエラーになってしまった。型構築子をパラメータにすることは出来ないのかな。それとも文法的な問題なのかなぁ……

λ. texdiary

を試してみる。池上さんの真似をしてpstoimgの代わりにconvertを使用。もちろん、Xy-picも使えるようにしとく。

テスト:

λ. Announce: 圏論勉強会(第四回)

今度の土曜は圏論勉強会の四回目ですよん。今回は Session 5 から。

日時

2005年2月19日(土曜) 13:00〜

場所

タイムインターメディア様 2階会議室 (地図)

テキスト

Conceptual Mathematics: A First Introduction to Categories

λ. 『数学の限界』, G.J.チャイティン(Gregory J. Chaitin) 著, 黒川利明 訳

を読んだ。セクシーな数学よりも具体的で分かりやすかった。まだちょっとしっくりこないところもあるけど。

λ. 継承とサブタイプ

暗黙のselfを受け取るメンバ関数のサブタイピングは、操作的意味論を考えるだけならば、確かにそんなに問題では無い気がします。ただ、この議論はこの体系が「二階ラムダ計算＋サブタイプ」へ素直には埋め込めないということを言っているわけで、既存の理論を直接応用できないという点で痛いんじゃないかと。例えば、モデルの存在は自明ではないと思うし、特にパラメトリシティ等の良い性質を持ったモデルを構築できるかどうかも気になります。

Extensible Objects: a Tutorial, Viviana Bono を読まねば……

λ. 「〜」ってなんて読むの？

やっぱ「にょろ」でしょう。それしか考えられん。変換するときも「にょろ」。

λ. Theorems for free!. Philip Wadler

を読んだ。不動点コンビネータを導入する場合には、パラメトリシティを適用できる関係は、単に連続な関係であるだけでなく正格な関係でなくてはならないというのに少し驚いた。

λ. Recursive types for free!, Philip Wadler

正負両方の位置にパラメータの現れるオペレータが不動点を持つような時のパラメトリシティの話かと思ってたのだけど、そうではなくて正の位置にパラメータの現れるオペレータの最小不動点と最大不動点を二階ラムダ計算で表現する話だった。

Fの最小不動点 μX.F(X) は ∀X.(F(X)→X)→X 、Fの最大不動点 νX.F(X) は ∃X.(X→F(X))×X で表される。それぞれ、weak initial F-algebra と weak final F-coalgebra になっていて、パラメトリシティが成り立つときに initial F-algebra と final F-coalgebra になる。

λ. パラメトリシティと不動点

パラメトリシティを仮定すると μX.X = ∀X.(X→X)→X によって initial object 0 を定義できる。ここでさらに不動点コンビネータを導入すると、不動点と有限直和を持つCCCの議論から困ったことになってしまう。不動点コンビネータとパラメトリシティは相性が悪い。

Theorems for free! では、不動点コンビネータを導入する場合には、パラメトリシティの適用できる関係を連続かつ正格なものに制限する必要があるとあった。μX.F(X) = ∀X.(F(X)→X)→X が initial F-algebra になることを示すには任意の射を関係として使えることが必要だったので、このような制限があれば、このμX.F(X)は initial F-algebra にはならない。これはまさにHaskellの場合で、Haskellで定義されるデータ型は weak initial algebra ではあるけど、initial algebra にはなっていない。

また、パラメトリシティと不動点を両立(?)させるには、そもそもCCC(= ラムダ計算)を諦めてしまって、線形論理を代わりに使うといったアプローチもあるみたい。

The Theory of Twiners and Linear Parametricity (Note), Ryu Hasegawa

λ. OCaml入門 (2): variance

OCamlは型定義の際にパラメータのvarianceを明示することが出来るそうだ。試してみる。

# type +'a foo = Foo of ('a -> unit) ;;
Characters 5-34:
  type +'a foo = Foo of ('a -> unit) ;;
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
In this definition, expected parameter variances are not satisfied
# type -'a bar = Bar of 'a ;;
Characters 5-24:
  type -'a bar = Bar of 'a ;;
       ^^^^^^^^^^^^^^^^^^^
In this definition, expected parameter variances are not satisfied

ふむふむ。確かにvarianceと矛盾する位置に変数が現れるとエラーになってくれますな。もう少し試す。

# type -'a foo = Foo of int ;;
type 'a foo = Foo of int
# type +'a bar = Bar of 'a foo ;;
type 'a bar = Bar of 'a foo

ありゃ。これはエラーにならないのか。ということは、型の定義中にはユーザに与えられたvarianceを使ったチェックを行うけど、一旦定義された型が他で使われたときには、ユーザによって与えられたvarianceではなく推論されたvarianceを使うということなのかな。

λ. 第四回圏論勉強会

今日は例の圏論勉強会の第四回目だった。

• CategoryTheory:圏論勉強会 (sampou.org, Programming in Haskell)

ところで、Conceptual Mathematics: A First Introduction to Categories, F. William Lawvere, Stephen H. Schanuel という本をテキストとして使っているのだけど、実は僕がこの本を注文したのは丁度3年前の今日だった。あれから、3年間で自分は少しは成長できただろうか?

λ. Haskell で始めたプログラマに C を教えるには…

• Haskell で始めたプログラマに C を教えるには…
  • FFI からアセンブラが分かるはずだから、Monad -> FFI 経由で教えるのがいい？

FFI からアセンブラが分かる……

　　 ／￣￣￣￣￣ ミ
　 /　　 ,————-ミ
　/　　／　 ／　　 ＼ |
　|　 /　　　,（・）　（・） |
　 (6　　　　　　 つ　　|
　 |　　　　　　＿＿_　 |　　 ／￣￣￣￣￣￣￣￣￣￣
　 | 　　　　 /＿＿/ ／　 ＜　なわけねぇだろ！
／|　　　　　　　　 ／＼　　 ＼＿＿＿＿＿＿＿＿＿＿

λ. monadic catamorphisms

僕の知っている monadic catamorphism は、以下のfoldWithM*1を使って書かれるようなもの*2なのだけど、これは 横山さんの日記 に出てきているものと同じものなのだろうか。

import Control.Recursion
import Control.Monad
 
foldWithM :: (Fixpoint f t, Monad m) => (forall a. f (m a) -> m (f a)) ->
             (f x -> m x) -> (t -> m x)
foldWithM k phi = fold (\x -> k x >>= phi)

λ. OCaml入門 (3): 多相バリアント(polymorphic variant)

Haskellの代数的データ型やMLのバリアントはデータ構築子がその型に結び付けられてしまうけど、似たようなデータ型が複数あるときには、データ構築子を共有したいこともある。そんなときにOCamlでは多相バリアントというのを使うことが出来るそうだ。

多相バリアントのデータ構築子は、バッククォート「`」で始まる名前で、データ型を定義せずに使うことが出来る。`Aまたは`Bで構築された値の型は [> `A | `B] となる一方、`Aまたは`Bで構築された値だけを受け取る関数の引数の型は [< `A | `B] となるようだ。

試しにλ式をSKIコンビネータに翻訳するコードを書いてみる。

# let (@) a b = `App (a,b) ;;
val ( @ ) : 'a -> 'b -> [> `App of 'a * 'b ] = <fun>
# let rec ski x t =
    match t with
      `Var y when (x==y) -> `I
    | `App (y,z) -> (`S @ ski x y) @ ski x z
    | `Lam (y,z) -> ski x (ski y z)
    | _          -> `K @ t
;;
val ski :
  'a ->
  ([> `App of 'b * 'b | `I | `K | `Lam of 'a * 'b | `S | `Var of 'a ] as 'b) ->
  'b = <fun>
# let test1 = `Lam (0, `Var 0) @ `Hoge ;;
val test1 : [> `App of [> `Lam of int * [> `Var of int ] ] * [> `Hoge ] ] =
  `App (`Lam (0, `Var 0), `Hoge)
# let test2 = ski 0 test1 ;;
val test2 :
  [> `App of 'a * 'a | `Hoge | `I | `K | `Lam of int * 'a | `S | `Var of int ]
  as 'a = `App (`App (`S, `App (`K, `I)), `App (`K, `Hoge))
# 

skiは `Var, `App, `Lam 以外のデータ構築子で構築された値も受け取れるので、skiの引数の型は [< `App of ... | ...] という形ではなく、[> `App of ... ] という形になっている。

使ってみた感じでは、ちと強力すぎる気がする。もう少し制限された形でも十分ではないか?

あと、asを使って循環的な型を書けるというのに少し驚いた。infinite unification?　単にoccurs-checkをしなければ良い?　infinite unification で検索したら、An Overview of the Theory of Relaxed Unification, Tony Abou-Assaleh, Nick Cercone, and Vlado Kešelj というのを発見。

λ. 『常識としての軍事学』, 潮 匡人

を読んだ。

λ. When is a function a fold or an unfold?, Jeremy Gibbons, Graham Hutton, and Thorsten Altenkirch

を読んだ。集合の圏の場合の、関数がfold/unfoldの形で書けるための必要十分条件を与えている。証明は集合論的かつ選択公理を使っているので、構成的な関数の圏に一般化することは出来ない。条件とその証明は非常にシンプルなんだけど、具体例はちょっと不思議な感じもする。

• (∃g:FA->A. h = fold g) ⇔ ker(Fh)⊆ker(h ∘ in)　*1
• (∃g:A->FA. h = unfold g) ⇔ img(Fh)⊇img(out ∘ h)

λ. Constructively Characterizing Fold and Unfold, Tjark Weber and James Caldwell

.

λ. 型が a -> b となる関数はなんでしょう？

すぐに思いつくのは、\_ -> undefined とか undefined :: a -> b とかだけど……、さすがに違うよなぁ……

λ. Almost homomorphisms

横山さんの日記を読んでいて、Almost homomorphism が分からなかったので、ググってみた。Optimizing Compositions of Scans and Reductions in Parallel Program Derivation とかを見ると、どうやら h をhomomorphism、πを射影として、π∘h と書けるもののようだ。

[追記] 横山さんの日記に出てきたのは、モノイドに関する homomorphisms と almost-homomorphisms 。

[追記] 横山さんによると「やはり、homomorphism と合成するのは射影関数とは限らなそうです」とのこと。

λ. Mutumorphisms

almost homomorphisms と関係がありそうなので、ついでに mutumorphisms についてもググってみた。これは以下のような形で書ける関数族 { f_i : μF → A_i }_i∈I のことのようだ*1。

f_i: μF → A_i
f_i = φ_i ∘ Fh ∘ in_F^-1

φ_i: F(∏_j∈I A_j) → A_i
φ_i = ...

h: μF → ∏_i∈I A_i
h = <f_i>_i∈I

この定義から h = (| <φ_i>_i∈I |)_F かつ f_i = π_i ∘ h であることが直ちに言えるので、f_i はF代数に関する almost homomorphism であり、catamorphism の almost- なので、almost-cata とも呼ばれる。

almost-cata の典型的な例は paramorphisms とその一般化である zygomorphisms。

λ. almost-catamorphism

f を cata とするとき，

accept . f      -- accept は fst, snd, (\ (x,y) -> x + y) など

なるほど。解説ありがとうございます。しかし、そうなると今度は accept として許される関数のクラスが気になります。comcatamorphisms *1 は全て almost-catamorphism と呼べるのだろうか?

λ. 代数的データ型と始代数の話

2004-07-31の代数的データ型と始代数の話にちょっと追記。最初は自信たっぷりに書いたけれど、例は正しくなかったし、どうもこの辺の話はイマイチよく分かっていない。この辺りは論文などでは適当に誤魔化されてしまう事が多いけれど、結構微妙なところもあるので、最低限のjustificationは必要なのではないか思った。

λ. Haskellたん

気に入ったのでこっそり転載。言っとくけど、関数型プログラミング言語Haskell Part3 の 432 に書いたのは俺じゃないからね。

λ. C と Haskell のハイブリッドな hello world

Syntax Error (2005-02-25)でコメントしたものを一応こっちにも転載しておく。リンク先の別の解の方が面白いと思う。

long a = 0;
int main (void) {--a;//-} = 0
a // b = 0; main = putStrLn "Hello World"
-- ; printf("Hello World"); return 0; }

λ. Ruby.NET コンパイラの開発

メモ。