日々の流転

λ. GHC and impredicativity

GHCが impredicative polymorphism (非可述的多相) をサポートか。進化早いね。

「Qualified Types for MLF」のエントリでとりあげたチャーチ数(Church numerals)の引き算のような例も通るし、[forall a. a->a] のような型*1も扱えるようになっている。

import Prelude hiding (pred)

type CN = forall a. (a->a) -> (a->a)

add, mult, sub :: CN -> CN -> CN
add m n  = (\s z -> m s (n s z))
mult m n = (\s -> m (n s))
sub m n  = (n::(CN->CN)->(CN->CN)) pred  m

pred :: CN -> CN
pred n s z = n (\g h->h (g s)) (\_->z) (\u->u)

xs :: [forall a. a->a]
xs = [id, undefined]

実装については Boxy types: type inference for higher-rank types and impredicativity を参照。 MLF は impredicative rank-n polymorphism の元でも principal type が存在するよう 型言語を拡張していたが、必要な場所では型注釈を与えるならそもそも principal type が存在しなくても問題ない気がするし、こっちの方が筋が良いような気がする。

Qualified Types for MLF で evident translation が困難ということの例として挙げられていた以下の式のうち、xs3とxs4はエラーになるな。

xs1 = []          :: forall a. [a]
xs2 = const : xs1 :: [forall a b. a -> b -> a]
xs3 = min : xs2   :: [forall a. (Ord a) => a -> a -> a]
xs4 = (<) : xs3   :: [Bool -> Bool -> Bool]

λ. ウォン高について色々

小熊さんのところで先日の日韓財務相会談について「協調介入でも申し込んでくるかなぁと思ってたんだけど」と書いてありましたが、ウォン高に対して日本が協調介入するというのは可能なのかという素朴な疑問があります。ウォン高に対する協調介入ならウォンを何らかの形で売らないといけないと思うのですが、日本の外貨準備はドル中心でウォンなんかほとんど持ってないはず……

あと、関係ないけど、大空のサウラビで取り上げられていた漫画(1,2,3)、小泉首相役の兵頭会長が「改革断行」とか言ってるのにウケました。内容は無茶苦茶だけどね。大体ウォン高に対して韓国はウォンを刷って幾らでも介入出来るので、これで通貨危機のようなことが再び起こるなんて有り得ない。まあ、韓国経済は今わりと調子がいいらしいので、あまりマネーサプライが増えるとインフレになる可能性はあるけど。

• 「ワロス曲線」おさらいスレ。