full-sessions-0.6.1

Haskell 研究 full-sessions

full-sessionsの新バージョン 0.6.1 を HackageDBにアップロード しました。
full-sessions は、Haskellにおけるマルチスレッド/ネットワークプログラミングのライブラリです。 Sessionモナドという新しいモナドを使ってプログラムを書きます。 チャネルの型表現にπ計算の型理論の一つであるセッション型を採用しています。セッション型のおかげで、チャネルの「使われ方（プロトコル）」がスレッド間で整合していることを実行前の型検査によりチェックできます。これにより、ある種のデッドロックや型の不整合は型検査で排除できるようになります。 さらにHaskellの型推論でセッション型を推論させれば、プログラムがチャネルを意図通りに使っていることを型表現からチェックできます。
full-sessions は、HList等で見られるような型レベルプログラミングのテクニックを駆使したかなり実験的なライブラリで、インタフェースすら安定していませんが、Haskellで作れる「型付きの」DSLの例としても、大きな意味があると勝手に考えています。
今回のバージョンは、

  • ネットワークプログラミングに対応しました。example参照
  • 記法が少し変わりました。(主に再帰の書き方)
  • 多くの場合により具体的な型が推論されるようになりました。
  • ソースからundefinedが無くなり、安全性が向上しました。

配布バイナリの examples/ 以下に、簡単なチャットプログラムと、SMTPクライアントのexampleがあります。

今のところ、まともなドキュメントを書く気力がありませんが、セッション型によるプログラミングの雰囲気だけでもわかっていただければ。

単純な型推論の例

文字列をチャネルで送出する
Main> :t typecheck1 $ \c -> send c "abc"
typecheck1 $ \c -> send c "abc"
  :: (Length ss l) => Session t (ss :> Send [Char] a) (ss :> a) ()

型 Session t ss tt a は indexed monad とうモナドの一種です。 チャネル(の集合)ssをttに変換する、とか、事前条件ssで実行すると事後にttとなる、と読みます。(ss :> s) は型レベルのリストで、ssの末尾にsを加えたリストを表現しますす。
例えば Session t (ss :> Send [Char] a) (ss :> a) () という型をもつ上のスレッドは、あるチャネルのセッション型を Send [Char] a から a に変換します。つまり、スレッドはそのチャネルを 1度 文字列を送るために使う、ということが型からわかります。 また、他のチャネルは使われないということもわかります。

整数を受け取った後にインクリメントして送り返し、その後()を送る
Main> :t typecheck1 $ \c -> recv c >>>= \x -> send c (x+1) >>> send c ()
typecheck1 $ \c -> recv c >>>= \x -> send c (x+1) >>> send c ()
  :: (Length ss l, Num a) =>
     Session t (ss :> Recv a (Send a (Send () a1))) (ss :> a1) ()
チャネルcとdから受け取った和をチャネルcに返す
Main> :t typecheck2 $ \c d -> recv c >>>= \x -> recv d >>>= \y -> send c (x+y)
typecheck2 $ \c d -> recv c >>>= \x -> recv d >>>= \y -> send c (x+y)
  :: (Num a, Length ss l) =>
     Session
       t ((ss :> Recv a u) :> Recv a (Send a a1)) ((ss :> u) :> a1) ()

見た目、型変数がたくさんあってややわかりづいらいですが、dのセッション型がRecv a uからuに、cのセッション型がRecv a (Send a a1)からa1に変換されます。
つまり

  • dは型aの値を1度受信する。 cは型aの値を1度受信し、1度送信する

ということが型からわかります。チャネル間のデータの流れはセッション型からはわかりません。

チャネル生成とスレッド生成

new というプリミティブでチャネルを生成し、 forkIOs というプリミティブで新しいスレッドを走らせることができます。
new はこんな型。 セッション型Botをもつチャネルをひとつ環境に追加します。

Main> :t new
new :: (Length ss l) => Session t ss (ss :> Bot) (Channel t l)

ixdo記法と組み合わせて、普通のdo記法っぽい記法が使えるようになります。(rebindable syntax でもいいかも) ixdo記法は cabal install ixdoppして、{-# OPTIONS_GHC -F -pgmF ixdopp #-} をソースの最初に書けば使えます。

test = ixdo
  c <- new
  forkIOs (send c "abc")
  x <- recv c
  io (putStrLn x)

io は IOモナドのアクションを実行するためのコマンド。

Main> :t test
test:
  :: (Length ss' l, Ended l ss) => Session t ss' (ss' :> End) ()
Main> test
abc
*Main>

エラーの例

セッション型は、チャネルはちょうど2つのスレッドのみ所有できます。2つのスレッドにおいてチャネルの使われ方が整合しないと型エラーになります。
例えば、次のように、 2つのプロセスが同じチャネルに同時に送信/受信するような場合は型エラーとして発見できます。

Main> new >>>= \c -> forkIOs (send c "123") >>> send c "123"

Top level:
    Couldn't match expected type `Send [Char] a'
           against inferred type `Recv t' u''
    When using functional dependencies to combine
      Comp (Send t u) (Recv t' u') Bot,
        arising from the dependency `s u -> t'
        in the instance declaration at src/FullSession/TypeAlgebra.hs:44:9
      Comp (Send [Char] a) (Send [Char] a) Bot,
        arising from a use of `forkIOs' at <interactive>:1:15-36

本来 チャネルで受信すべきところを送信しているため、 Couldn't match expected type `Send [Char] a' against inferred type `Recv t' u'' というエラーがでています。

複雑な型推論の例

例えば examples/ にある SMTPクライアントの関数を型推論でチェックすると、果てしなく長大ですがこんな型が出てきます：

Main> :t \x y z w -> typecheck1 $ sendMail' x y z w
\x y z w -> typecheck1 $ sendMail' x y z w
  :: (Length ss l) =>
     t1
     -> t11
     -> String
     -> String
     -> Session
          t
          (ss
           :> Recv
                R2yz
                (Send
                   EHLO
                   (Recv
                      R2yz
                      (Rec
                         Z
                         (SelectN
                            (Send
                               MAIL
                               (Recv
                                  R2yz
                                  (Rec
                                     (S Z)
                                     (SelectN
                                        (Send
                                           RCPT
                                           (OfferN
                                              (Recv R2yz (Var (S Z)))
                                              (Recv R5yz (Send QUIT Close))))
                                        (Send
                                           DATA (Recv R354 (Send MailBody (Recv R2yz (Var Z)))))))))
                            (Send QUIT Close))))))
          (ss :> End)
          ()
Main>

# ちなみに型チェックに2秒くらいかかります