日々の流転

λ. キャッシュ

tDiaryはrhtmlをキャッシュしているけど、rhtmlから変換されたrubyのソースをキャッシュした方が効率的ではないかと思った。

λ. バーチャル.NETアイドル　ゲイツ46歳

闇黒日記(平成14年4月20日)より

λ. 読書

『ラバーズ02』

犬上 すくね [著]

λ. hsPTQ 0.0.2

hsPTQは一年以上前に作ったまま、ずっとソースコードを公開するのを忘れていたのだけど、ようやく公開した。公開にあたっては一応Cabal化してみた。

PTQというのは R.Montague の論文「The Proper Treatment of Quantification in Ordinary English」からきていて、英語の平叙文のサブセットに対して形式言語と同様の形式的な意味論を与えるものです。 hsPTQはそのPTQをHaskellで実装したもの。 ちょっとしたオモチャだけど、なかなか面白いものだと思うので、向井先生の言語の意味論(2006)の講義資料などを参照しながら、遊んでみてください。

なお、PTQの意義とかは郡司先生の「モンタギュー (Richard Montague 1930–1971) — 自然言語に対する形式意味論の実現者」が分かりやすいです。

λ. ステルス

テレビでやっていたので観た。 映像は良かったけど、なんとも能天気かつご都合主義のストーリー。 あと、死にそうだと思っていたキャラが速攻で死んでうけた。

λ. 長さ付きリストに対する型安全な filter 関数

型レベルプログラミングの会(ヒビルテ(2009-04-18))の会場で出てた話だけど、(a → Bool) → Vec a n → (∃m≦n. Vec a m) みたいなやつなら定義可能。

{-# LANGUAGE EmptyDataDecls, GADTs,
  FlexibleInstances, MultiParamTypeClasses, IncoherentInstances #-}

data Z
data S n

data Vec a n where
    VNil  :: Vec a Z
    VCons :: a -> Vec a n -> Vec a (S n)

class LE a b

-- one definition of ordering
instance LE Z n
instance LE n m => LE (S n) (S m)

-- another definition of ordering
instance LE n n
instance LE n m => LE n (S m)

data BoundedVec a n where
    Bounded :: LE m n => !(Vec a m) -> BoundedVec a n

vfilter :: (a -> Bool) -> Vec a n -> BoundedVec a n
vfilter f xs =
    case xs of
      VNil -> Bounded VNil
      VCons x xs ->
          case vfilter f xs of
            Bounded ys ->
              if f x
              then Bounded (VCons x ys)
              else Bounded ys

ただ、Haskellの型クラスだと推論を制御するのが難しくて、オーバーラップしたインスタンス定義(IncoherentInstances)が必要になってしまった*1。 オーバーラップしたインスタンス定義を使わない定義は型ハッカーの諸氏への課題ということで。