2002-05-29
λ. 夕方まで寝てた。これでここんとろこの不足分を取り戻したぞー
λ. TinyC
こないだkjanaさんに紹介してもらった TinyC のコードにざっと目を通した。さて、どこから弄るかな……
λ. 誤変換
「総資産」を「荘子さん」と誤変換。あうあう……
λ. 続^2 Y Combinator
[ruby-list:35060]のFは、自分自身が定義域になっているようなnon-well-foundedなタイプなので考えにくくてしょうがない。
こういうのって、超集合論(hypersets)とかを知ってると、わりと楽に考えられたりするのだろうか?
λ. ところで、Y Combinator のようなトリッキーな事をしなくても同じことが出来るような仕組みを大抵の言語は持ってるのね。
- Schemeではletrecを使う
-
(define fact (letrec ((f (lambda (n) (if (zero? n) 1 (* n (f (- n 1))))))) f)) - Haskellのletは他の言語でのletrecに相当する
-
fact = let f n = if n == 0 then 1 else f (n - 1) * n in f - Common Lisp だとlabelsを使う
-
(defun fact (n) (labels ((f (n) (if (zerop n) 1 (* n (f (- n 1)))))) (f n))) - Smalltalk
- 使ったこと無いけど、thisContextという特殊変数でブロック自身を参照できるそうだ。
2004-05-29
λ. Rena (5)
色々とダメダメだけど、こっそり公開。rena-0.0.1.tar.gz
λ. [ruby-dev:23634] Re: NEWOBJ() in dfree
そういえばRuby-GNOME2もdfree()内でRubyのコードが実行される可能性があるなぁ。というのも、destroyシグナルのようなシグナルにシグナルハンドラを結び付けていると、dfree内でオブジェクトが開放された際にそれが実行されてしまうため。
λ. 某コンサート
気まぐれで、某コンサートのお手伝い。小学校の頃の同級生に会う。
λ. "A New Notation for Arrows", Ross Paterson
を読んだ。「κpat -> cmd」なんてどっかで見たような文法が出てきて、おやっと思ったら、やっぱり"Decomposing Typed Lambda Calculus Into a Couple of Categorical Programming Languages"のκ-calculus 繋がりだった。Arrow とは全然関係ないと思っていたので、こういう繋がりがあるのは意外で面白いな。
[2005-04-30 追記] ArrowZero は zeroArrow >>> f = zeroArrow と f >>> zeroArrow = zeroArrow という強い性質を要求しないため、単に ArrowPlus の <+> の単位元という位置づけでしかない。でも、それならば ArrowZero を ArrowPlus から独立したクラスにすることに何の意味があるのか?
2005-05-29
λ. 永夜抄スペカ取得率: 214/222/222
久し振りに東方永夜抄をプレイ。Lunaticを頑張ってノーコンテニュークリア。7機で始めてクリア時に残機0・ボム0という惨状だけどね。で、Lunatic 6Bのスペルカードを中心に何枚か回収したので、取得済み/挑戦可能/総数 が 214/222/222 になった。残るは以下の8個。取れそうな気がするのは「ライフスプリングインフィニティ」と「永夜返し -丑の四つ-」くらいか……
- 禁薬「蓬莱の薬」 (Lunatic)
- 神宝「ライフスプリングインフィニティ」 (Lunatic)
- 神宝「蓬莱の玉の枝 -夢色の郷-」 (Lunatic)
- 「永夜返し -丑の四つ-」
- 「インペリシャブルシューティング」
- 「エンシェントデューパー」
- 「夢想天生」
- 「深弾幕結界 -夢幻泡影-」
ところで、「永夜返し -子の四つ-」は「子の刻」「子の二つ」「子の三つ」よりも簡単な気がする。
λ. Extensional Equality in Intensional Type Theory. Thorsten Altenkirch
を読んだ。問題意識は良くわかるのだけど、モデルの構成がイマイチよく分からなかった。
(2005-09-17 追記) 読み返したらあらかた理解できた。けど、まだ幾つか理解できていない概念がある。large elimination とか。
(2005-09-30 追記) Agdaでも実装してみた。An Implementation of a setoid model in Agda.
(2006-05-30 追記) large elimination は多分 elimination した結果が要素ではなく集合などになるような elimination 。
2006-05-29
![[今日の写真]](./images/20060529_0.jpg)
慶早戦で授業は無し、と思ったら大学院の授業は普通にあるのだな。すっかり忘れていて、さぼってしまった。
λ. 古川研:Abduction勉強会
3.2 Protected Links, Threats, Promotions and Demotions。保護リンクがclippedの否定が保たれることで実現されるのはわかったが、PromotionとDemotionに対応する順序がどこで導入されるかが良くわからなかった。
λ. 博士号を取得するとは
帰り道の途中で博士号を取得するとはどういうことかという話が耳に入った。政治学の人のようだ。むちゃくちゃ要約すると「研究は質よりも量。教授をうんざりさせられれば勝ち。量は誠意」という話。結構嫌な気分になる。
2008-05-29
λ. OCamlでランクn多相
レコードでもliftしたい - みずぴー日記 のコメントに関する補足。
関数を受け取って、レコードの型の異なる複数のフィールドに対して適用する高階関数を書きたいという話。
型の異なるフィールドに対して適用するには、受け取る関数は [Int]→[Int]→[Int] のような型の単相的な関数ではなく、∀a. [a]→[a]→[a] のような型の多相的な関数である必要がある。で、多相的な関数を受け取る高階関数の (∀a. [a]→[a]→[a])→Record→Record→Record のような型は、二階ラムダ計算の言葉でいうと、ランク2の型になっている。
ランクの正確な定義は Type reconstruction in finite-rank fragments of the polymorphic λ-calculus (c.f. The “Curry view” and the “Church view” of polymorphic λ-calculus - ヒビルテ (2006-04-25)) あたりを参照してもらうとして、ランク2の型はHindley-Milnerの型システムの表現力を超えるので、言語によって扱いが異なっていて面白い。
Haskellの場合
GHCはランク2多相(rank-2 polymorphism)をサポートしていて、型宣言を書きさえすれば自由に使うことが出来る*1。
{-# LANGUAGE Rank2Types #-}
data Record
= R
{ x :: [Int]
, y :: [Double]
}
lift :: (forall a. [a] -> [a] -> [a]) ->
Record -> Record -> Record
lift f R{ x=x1, y=y1 } R{ x=x2, y=y2 }
= R{ x = f x1 x2, y = f y1 y2 }
append' :: Record -> Record -> Record
append' = lift (++)
ちなみに、Haskellでのランク2多相の使用例でもっとも有名なのは、STモナド(Control.Monad.STモジュール)の runST :: (forall s. ST s a) -> a で、これについては Lazy Functional State Threads で詳しく説明されている。
OCamlの場合
一方、OCamlの場合にはランクN多相に直接対応してはいない*2けど、レコードのフィールドが多相型を持つことが出来るので、多相関数をレコードに包んで受け渡すことでエンコードできる。
type some_record = {x:int list;y:float list}
type op = { app : 'a. 'a list -> 'a list -> 'a list }
let lift f {x=x1;y=y1} {x=x2;y=y2} =
{x=f.app x1 x2;
y=f.app y1 y2}
let append' = lift { app = (@) }
あと、同様の例として、昔のOCaml.jpにあったチャーチ数の例がある。
- Church 数 ― OCaml.JP
- <URL:http://web.archive.org/web/20060430024445/ocaml.jp/archive/sample/firstclass.ml>
Scalaの場合
Scalaでランクn多相をエミュレート - Onion開発停滞日記(2008-05-30) で水島さんがScalaへの翻訳を書いてくれました。ありがとうございます。 あとで自分でやろうと思ってたら先を越されてしまった(^^;
SML#の場合
現在のSML#にはこういった機能はないのかな。LLDN のときの上野さんの発表「Language Update: Standard MLer から見たML 概要」の「Next generation of ML」によると Rank-n polymorphism についても「理論的には完成。実装待ち」とのことなので、そのうち実装されるのだとは思うけど。
【2009-03-14追記】 ……と書いたけど、PPL2009で上野さんに聞いたら、どうもこういったファンシーな機能は当面実装されることはなさそうな感じだった。
F#の場合 (2009-02-19追記)
いげ太さんという方が、いげ太のブログ: F# で ランク N 多相っぽく でF#の場合について書かれていた。 F#ではOCaml流の多相的なフィールドを持つレコードではなく、ジェネリックなメソッドを持つインターフェースが推奨されているらしい。
