トップ «前の日(04-19) 最新 次の日(04-21)» 追記

日々の流転


2002-04-20

λ. キャッシュ

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

Tags: tDiary
本日のツッコミ(全2件) [ツッコミを入れる]

ψ ただただし [可能性はある。ベンチマーク希望(笑)]

ψ さかい [僕に定量的な評価を求めてはいけません。(^^;; でもまあ、とりあえずTDiary::Plugin#eval_rht..]


2004-04-20

λ. 読書

『ラバーズ02』
犬上 すくね [著]
Tags:

2008-04-20

λ. 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) — 自然言語に対する形式意味論の実現者」が分かりやすいです。

λ. ステルス

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

ステルス デラックス・コレクターズ・エディション [DVD]

Tags: 映画

2009-04-20

λ. 長さ付きリストに対する型安全な 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。 オーバーラップしたインスタンス定義を使わない定義は型ハッカーの諸氏への課題ということで。

Tags: haskell

*1 Agdaだと明示的に書くのでどうとでもなるのだけど、Haskellだと型クラスの機構を使って間接的に書かなくてはいけないのが、隔靴掻痒な感じだなぁ。