日々の流転

λ. CLTT の 1.5 Change-of-base and composition for fibrationsのノート

CLTT読書会で読んでいる Categorical Logic and Type Theory の、1.5 Change-of-base and composition for fibrations を復習して、練習問題も一通り解いた。だんだん追いついてきたよ。練習問題はきっと綺麗に解けるんだろうけど、がりがり計算して解いてしまった。

• ノート

λ. CLTT の 1.6 Fibrations of signatures のノート

CLTT読書会で読んでいる Categorical Logic and Type Theory の、1.6 Fibrations of signatures を復習して、練習問題も一通り解いた。もう少しで勉強会に追いつく。

• ノート

λ. iteratee I/O勉強会

に参加。詳しくはmaoeさんのブログなどを参照。

• Tweetvite :: iteratee I/O勉強会
• Lazy I/O must go! - Iteratee: 列挙ベースのI/O - 純粋関数型雑記帳
• maoeのブログ
  • HIMA' #1: iteratee I/O勉強会 - maoeのブログ
  • iteratee I/O勉強会 - maoeのブログ

iteratee law とかないのなと思う。 IterVがMonadであることを含意するのが最低限の条件。

それと、以下の iteratee-0.4 での定義をCPSスタイルと言っていたけど、感じとしてはIterVMのモナディックなチャーチエンコーディング(?)を考えているような雰囲気だと思った。もう少しちゃんと考えたいところだけど。

iteratee-0.2 での定義:

data IterVM el m a = DoneM a (StreamG el) 
                   | ContM (Iteratee el m a) 

newtype Iteratee el m a = 
  Iteratee { runIter :: StreamG el -> m (IterVM el m a) } 

iteratee-0.4 での定義:

newtype Iteratee el m a = 
  Iteratee { 
    runIter :: forall r. 
      (a -> Stream el -> m r) -> 
      ((Stream el -> Iteratee el m a) -> Maybe ErrMsg -> m r) -> 
      m r 
   }

あと、全然脱線して、pirapirapiraさんに Epigram, OTT(observational type theory), Pola: a language for PTIME programming とかについて盛り上がる。

• Extensional Equality in Intensional Type Theory - ヒビルテ(2005-05-29)
• Towards Observational Type Theory - ヒビルテ(2006-05-16)
• Observational equality, now! - ヒビルテ(2009-07-15)

その後は例によってシャヒ・ダワットで懇親会。 ビリヤニというのが日本ではここでしか食べられないらしい*1。 それから、アダムの呪い、イブの7人の娘達 とかの話面白かった。 あと、「やっぱりgitは使える様にならないとなぁ」と思った。

λ. CLTT読書会 第6回

今回は、1.7 Categories of fibrations の Lemma 1.7.6 後の 2 categorical struture のところから Exercise 1.7.2 くらいまで。

• CLTT読書会 第6回 : ATND
• 前回

λ. 誕生日

λ. CLTT の 1.7 Categories of fibrations のノート

CLTT読書会で読んでいる Categorical Logic and Type Theory の、1.7 Categories of fibrations を復習して、練習問題も一通り解いた。 これで勉強会に追いついた。

• ノート