コミケ92 金曜日 東た11bでの同人誌に記事を書きました

c92-cover

コミックマーケット92 金曜日 東た11b参照透明な海を守る会というサークルで「簡約!? λカ娘 10」という同人誌が頒布されるらしいのです。その中で2つの記事を書きました。

1つ目は「Coq ダンジョン : 底抜けの壺の夢」という証明できない命題も証明できるCoqのタクティックを作ってしまおうというチョイネタです。CoqはタクティックがズルしてもGallinaの型検査ではじかれるから安心ですね!

2つ目は「静的コード解析はいいぞ!」というソースコードの検証手法の概要紹介です。特にVeriFastという解析ツールを使う意義を初心者にもわかりやすく導入したつもりです。短かい記事ですが。最近はVeriFastのような製品品質を静的な解析によって向上させる手法に個人的に興味があり、「静的コード解析の会」などというイベントを開催していて、次回は2017/09/23(土)に開催される予定です。

僕以外の記事についても(理解できる範囲で)解説してみます。

「モナドとひも」は@myuon_myonさんの記事で、主にモナドを圏論の図式ではない紐を使った図を描くことで理解を促進するこころみの紹介です。僕個人は日頃ヒューリスティックなブロック図を描いてしまいがちなので、形式的な図の描き方には興味がわきました。

「矢澤にこ先輩と一緒にモナドモナド!」は@public_ai000yaさんの記事で、「モナド上のモナド」について解説しています。本記事は圏論の知識が前提とされて個人的にはショック死しました。。。特にモナド合成とモナドモナドとの関連で今混乱しています。。。@public_ai000yaさんはコミケ当日ブースで売り子をしていただけるようなので直接質問するといいかもしれないですね!

「IST(Internal Set Theory) 入門 (後編)」は@dif_engineさんの記事で、超準解析のための内的集合論の入門記事の後編です。この記事の前編は「簡約!? λカ娘 9」に掲載されています。いきなり後編から読むのは辛いので、9巻も一緒に買うといいですね!9巻では無限に小さい数について考え、述語論理の導入から初学者を高階な数学の世界に持ち上げてくれます。僕も読み直さねば。。。

「VeriFastチュートリアル」は@eldeshさんの翻訳記事で、原文はこちらです。僕も少しだけ翻訳手伝いました。またこの翻訳はオンラインから全文を読むこともできます。VeriFastは先にも紹介した静的コード解析のツールの1つで、C言語やJavaコード中のコメントに特殊な注釈を設計者が書くことで、関数の事前条件/事後条件やポインタの安全な使用などをコードの実行時ではなく静的な検査によって網羅的に検証してくれます。Coverityなどの静的コード解析ツールと異なり、左記の注釈を人力でコードに追記する必要がありますが、(ある条件下では)エラーの見逃しや誤検出が起きないのが良い点だと思います。この正確な検証はVeriFastが分離論理という理論基盤の上に構築されていることに由来しています。

上記同人誌の一部のページは立ち読みできるので、気になったら是非サークルブースにおこしいただけたら幸福です。

広告

プロプライエタリな会社でオープンソース運動をしすぎて怒られた時の謝罪メールテンプレ

[雑談] 僕のオープンソースに対する思い入れについて共有させていただけないでしょうか

少し長い雑談メールをお送りすることをお許しください。

僕はときおりオープンソースについて強い信念をもって主張することが
あると思います。そんな時
「なぜこの人はこんなにオープンソースに思い入れがあるんだろうか?」
と理解に苦しむ場面があると思います。今日はそんな僕のオープンソース
に対する愛着についてどんな理由があるのかについて説明したいと思います。

僕は20世紀MSXユーザとして育ちました。MSX-FANという雑誌があり、
その中で紹介されているコードは紙面にコードが掲載されていて、その
コードを写経して動かしていました。BASIC+マシンコードのプログラム
が多かったですが、それを意味もわからずに写経するのが小学生時代の
僕のプログラミングのルーツでした。そうしてご承知の通りMSXは終焉を
迎えました。それでもMSX-FANは発行し続けたのですが、ついに雑誌さえ
廃刊になりました。その最終号に
「これからMSXユーザはどこへ向うべきなのか」
というコラムが掲載されました。その中に
「GNUプロジェクトは多くのソフトウェアのソースコードを公開している」
「次のMSXユーザの楽園はGNUプロジェクトの菩提樹の下にある」
そのような主張がなされていました。もちろんこれは単なるコラムで
MSXコミュニティの総意ではありません。しかし中学時代の僕の心には
GNUの旗の下で一生を終えるのだ。というかすかな信念が植え付けられ
ました。

大学に入学して、学校から勧められたのはMacintoshでした。品質の悪い
OSでしたが、GUIには関心してCodeWarriorのC言語コンパイラを買って
なぜかPascalで書かれているGUIフレームワークのAPIをC言語からたたく
という謎のプログラミングモデルに悩んでいました。

大学時代後半になるとWindows 2000を使うようになりました。驚異的な
品質のOSでしたQuake3をビデオカードの上で動かしていてもまったく
ブルースクリーンになりません。マイクロソフトが設計するソフトウェアの
品質が如何に高いのか。その高品質に対する記憶は僕の心の奥深くに
注入されました。しかしマイクロソフト製品を使うのはGNUプロジェクトの
信念に反しています。僕は葛藤しながらもWindowsを使っていました。

Windowsユーザであると同時に僕はSlackwareというLinuxディストリ
ビューションを大学の友人に紹介してもらいました。そのLinux OSの上
ではGNUプロジェクトの製品がもれなく使えました。完全に自由な
エコノミーが広大な空間にひろがっていました。その全てのソースコードは
公開されていました。
「僕はこのコード全てを一生のうちに読むことができるのだろうか」
そんなみはてぬ遠い展望に僕は目がくらむと同時に大きな希望を感じ
ました。

ところがご存知の通りSlackwareの品質は劣悪なものでした。まずデバイス
ドライバがまっとうに動くことなどありません。ユーザは自分のPCで
デバイス動かないことをあたり前のように経験し自分の責任で不具合を
修正することが求められました。Windows 2000の高い品質を知っていた
自分としては、悔しいけれどLinux OSを大学の実験のようなクリティカル
な用途に使えず、あくまでもホビー用途にしか使えないなと感じていました。

そんな葛藤をかかえていたところにLinux japanとう日本の雑誌に
Debian GNU/Linuxディストリビューションの特集が組まれました。
Slackwareの他のディストリビューションしか知らなかった僕は軽い
気持ちでその特集を読みはじめました。dpkgというパッケージマネージャが
ディストリビューションの全てのモジュールをパッケージとして管理する
というしくみに関心しました。Linux kernelでさえdpkgで管理する1つの
パッケージに過ぎないのです。しかし技術面よりも強く感銘を受けた
のはそのプロジェクトの哲学でした。

そのDebianプロジェクトの哲学について調べているうちに僕は1つの文書
を発見しました「Debian宣言」です。以下にそのURLと文書の要約を引用
します。

https://www.debian.org/doc/manuals/project-history/ap-manifesto.ja.html

## A.1 Debian Linux とは何か?

"今までに開発された他の Linux ディストリビューションのように限定的な
個人やグループが開発しているものではなく、Linux と GNU の精神に則り、
オープンに開発されています。"
"Debian は、市場で十分な競争力を持ちえる、商用ではないディストリ
ビューションを作り出す試みでもあります。"

## A.2 なぜ Debian を作成するのか?

"大抵の Linux ユーザは、ディストリビューションを通して Linux なるもの
の最初の感触を得るものです。また、多くのユーザが、このオペレーティング
システムに慣れてからも、便利さを求めてディストリビューションを使い
つづけるでしょう。"
"ディストリビューションが明らかに重要であるにもかかわらず、開発者達は
ほとんど注意を払わずにいます。単純な理由によります。ディストリビューション
の構築は易しくもないし、魅力的でもないからです。"
"多くのディストリビューションがかなりよいシステムとして発表されました。
しかし、時が経つにつれて、ディストリビューションの保守から次第に関心を失い、
二の次になってしまいます。"
"これら配布業者は、より多くの雑誌で派手に広告を出してもかまわないだけの
金を努力して実際に稼ぎ出しています。単にあまりよくわかっていないだけの者が、
容認できない行動を助長してしまうという古くから見られる事例が見てとれます。
あきらかに、この状況を改善するために何か手を打つ必要があります。"

## A.3 Debian はこれらの問題に終止符を打つためにどのように努力するつもりなのか?

"Debian の設計過程は、オープンです。システムが最高の品質を持つことと、
ユーザの共同体の要求を反映させることを保証するためです。能力と背景に広がり
がある他人を巻きこむことで、モジュール化して Debian を開発することが可能に
なりました。ある分野の専門的知識を持つ者が、その分野を含んでいる Debian
の個々の構成要素を開発したり保守したりする機会が与えられるので、
その構成要素の品質は高くなります。"
"Linux が商用の製品ではなく、今後も決してそうはならないこと、しかし Linux
が商業的な競争に決して勝てはしないとは意味しないことを世に知らしめることに
なります。同意しない人は、GNU Emacs と GCC が成功していることを理由付けして
いただきたい。これらは商用の製品ではありませんが、商用であるかどうかにかかわ
らず市場に甚大な影響を与えてきました。
"Linux 共同体全体とその未来に迷惑をかけて自分が裕福になるという破壊的な目標
を目指すかわりに、Linux の未来に集中するときがきました。Debian を開発し配布
しても、この宣言で概略を述べた問題への回答とはならないかもしれません。ですが、
少なくとも、これらの問題が解決すべき問題として認められるくらいには Debian
を通して注意を引きたいと望んでいます。"

衝撃です。僕の目から入ったこの文章は確実に僕の心臓と脳を打ち抜きました。
もっと要約してしまえば彼は
「品質なき世界に我々は死するとも正義をなす!」
「品質に対する正義とは何か?それは我々がなにもかも定義するのだ!」
と宣言しているのです。プロプライエタリな製品を作っている人間にとっては
破壊者に見えるでしょう。しかし十字軍もイスラム教にとっては破壊者だったのです。

その後の歴史については解説する必要はないと思います。今皆さんがLinuxデスクトップ
を使っている際に選択するディストリビューションはUbuntuでしょう。そしてその
Ubuntuの品質の根っこは今もDebianプロジェクトが粛々と作りこんでいるのです。
僕の私見ですが、今もDebianプロジェクトを推進できたのはDebian宣言にある
品質に対する強い哲学と信念のおかげだと感じています。

ときおり僕が
「会社での生産物をオープンソース化した方が良い」
と主張するのには上記のような背景があります。今後もご迷惑をおかけすることも
多いと思います。その際には都度適切な方法でしかりつけていただけたら幸福です。

以上よろしくお願いいたします。

前職でオススメのタイル型ウィンドウマネージャを聞かれたので僕なりの解説をしてみました

「今twmかi3かxmonadで悩んでます」
「ぉ。宗教戦争ですね!それぞれの利点がありますよ!」
「これは話すと長いので家に帰ったら詳細を書きますー」

などという会話が某L社のチャットで流れたのをキッカケにして僕の中でなにかがはじけました。そのチャットでの発言をブログにも残しておこうと思います。

1st: 「twmについて」

“X11R4以降、標準のウィンドウマネージャとしてXサーバに同梱されている。” https://ja.wikipedia.org/wiki/Twm

これが唯一無二の強みです。例えばNetBSDのようにOSがパッケージに分割されておらず、ベースシステムとパッケージ(pkgsrc)にわかれている場合、i3wmやxmonadを使いたければpkgsrcでインストールせねばなりません。ときおり競合によって使用不能になるケースもあるかもしれません。twmならベースシステムに含まれているので、NetBSD OSのアップグレードさえ成功すれば問題なく使えます。Linuxでは「全てがパッケージ」という考え方が主流ですが、BSDではベースシステムと{ports,pkgsrc}がわかれているのが主流です。その場合自分の作業基盤が{ports,pkgsrc}に依存していると非常事態のときに身動きが取れなくなります。

R社時代にSさんという伝説のハッカー社員がいました。彼は20世紀にNetBSDを使ってプリンタを設計しようという狂ったアイデアを影で推進した張本人です。彼は「最後の砦」でした。だれにもわからないNetBSD kernelのバグを彼はコードをタグジャンプしたりカーネルデバッガを時折使ったりするだけで解決していました。彼はtwmのユーザでした。彼のデスクトップは「左上: xterm」「左下: xterm」「右側上下: Emacs」というワークスペースのまま、まったくワークスペースを切り換えことなくハックしていました。

そんなBSDカーネルハッカーになりたいあなたにおすすめなのはtwmです!

2nd: 「xmonadについて」

”このウィンドウマネージャは、関数型プログラミング言語Haskellで書かれている。” / “実行中に、設定ファイルを変更しリロードすることで、カスタマイズ可能である。” / xmonad – Wikipedia https://ja.wikipedia.org/wiki/Xmonad

この「設定ファイル」とは何者で、どんな文法なのでしょうか?なんとそれはHaskell言語そのものなのです!具体的な設定ファイルの例はこちらから閲覧できます / https://wiki.haskell.org/Xmonad/Config_archive

実は実際にはxmonadはアプリケーションではなくライブラリでしかないのです。実際最小のxmonadの設定ファイルは以下で記述できます。

https://wiki.haskell.org/Xmonad/Config_archive#Minimal_xmonad_config_files

import XMonad
 
main = xmonad defaultConfig {
      modMask = mod4Mask -- Use Super instead of Alt
    , terminal = "urxvt"
}

なるほど。だからXモナドなんですね。名は体を表わすという訳です。

というとはこの設定ファイルの中ではありとあらゆるHaskellのライブラリを使って自由に拡張可能なことになります。Haskell言語は近年ではおそらく最も豊かな型システムを持つ言語でしょう。それは国際学会ICFPにおけるHaskell言語の扱いを見れば一目瞭然です。 / ICFP 2017 http://conf.researchr.org/home/icfp-2017

icfp2017

Haskell言語だけ特別扱いで2日間ぶちぬきの #シンポジウム が開かれます。一方OCamlなどの言語には1日間しか与えれていません。そしてOCamlのそれは #ワークショップ です。日本でいうところの #学会 と #お勉強会 の違いのようなものでしょうか。とにかくHaskellは今ぶっちぎりで最先端をはしる高階な言語なのです。(高階なことが良いか悪いかは別にしてですが)

そんな世界一イケているソフトウェア設計言語Haskellで自分のデスクトップを自由自在に拡張したい。カスタマイズしはじめると止まらない貴方におすすめなのがxmonadです!

3rd: 「i3wmについて」

“i3 is a tiling window manager designed for X11, inspired by wmii, and written in C.” / i3 (window manager) – Wikipedia https://en.wikipedia.org/wiki/I3_(window_manager)

え、C言語で書かれているのはいいんだけど、他になんか特徴はないの?って思うんじゃないでしょうか。じゃじゃーん。実はとりたてて特徴がないタイル型ウィンドウマジェージャがi3wmなのでーす。

i3wmはデフォルトの設定を特に弄らなくても容易にステータスバーがいいかんじに表示されるようになっています。キットインしたらすぐ使える。そしてだれもが「まぁ、、、無しってことはないデフォルト設定だなぁ」と納得してしまう。そんなぼんやりしたタイル型ウィンドウマネージャの凡人です。

でもね。人間を想像してみてください。特別な人ってどこかいびつだから特別なのではないでしょうか?20世紀のしっかりした日本製品は特別な人が設計したのではありませんでした。凡人の集団が凡人なりに努力をして、凡人なりの落しどころを作り、丁寧な再発防止をした結果産まれたMade in Japan。それを支えたのは凡人達だったのです。

“俺は普通だから変わったとこもないから、好きなものだって特別にはないんだ” / http://www.uta-net.com/song/221954/

そう #普通であること に悩み、そしてそれでも生きるあなたにこそおすすめしたいのが、i3wmです!

あなたは…?

さぁ3人のペルソナ、あなたは誰を選びますか?誰になりたいですか?その思いが答です。

エホバの証人の友人との手紙1: 生命の起源に関する見方について

メールをやりとりしているので、なんとなく自分の信仰を表明するためにはりつけます。。。

> 表題の件について,イタリアのロボット工学者のコメントをどうぞご覧ください。
> 下記のリンクから動画をご覧いただけます。
> https://www.jw.org/ja/%E5%87%BA%E7%89%88%E7%89%A9/%E3%83%93%E3%83%87%E3%82%AA/#mediaitems/OriginsLife/pub-pcr_J_2_VIDEO

ありがとうございます。拝見しました。同意できる点も多かったです。

しかし、一人のソフトウェアエンジニアとして強調したいのは、この世界全体が誰か一人もしくは集団の手によって意図的に設計されたのだとしたら
「あまりにも完璧に構成されすぎている」
ということです。仮に全知全能な人間が存在したとしてもこのような設計は不可能だったに違いないという直感があります。この直感はなんらかの製品が完璧であることを理論的に検証することができても、「実際の動作」が安定しているかどうかを検証するのは(おそらく)不可能だという認識から産まれています。
また、経済がだんだんと「生命」をおびてきていることも私のガイア信仰をうらづけています。株式の乱高下は地球全体の生命の鼓動のように私には感じられるのです。そして(今のところ)経済は指数関数的な成長を裏付けています。私個人の考えでは、この指数関数的な成長は数学の指数関数的成長にささえられていると考えています。

数学記号の誕生を年表で。美しい

つまり、私のガイア信仰におけるガイア全体の成長は個々人の血のにじむ苦悩の上にささえられ、そして(願わくば)このガイア信仰によって人類はよりよい生活が得られると考えるのです。この成長によって中期的にはベーシックインカムのようなさらなる自由とおそらくはさらに高次元の苦悩を人類は手にするでしょう。

https://ja.wikipedia.org/wiki/%E3%83%99%E3%83%BC%E3%82%B7%E3%83%83%E3%82%AF%E3%82%A4%E3%83%B3%E3%82%AB%E3%83%A0

私はこのような人間全体の成長を深く信じています。まとめると私達一人一人は経済という生命の細胞の1つでしかないのかもしれないのです。

> ※どのアドレスを使ったらよいか分からなかったため,念のため全部にお送りし
> ておきます。

基本的に個人のメールはkiwamu@gmail.com宛ての方が良いかもしれません。
# じゃあ仕事の名刺わたすなよ、という話でもありますが、これも何かの御縁。仕事上でのお付き合いもある可能性もありますので…

また、キリスト経だけではなく他の宗教にも手をのばしてみることを深すおすすめします。

スリー・カップス・オブ・ティー https://www.amazon.co.jp/dp/4861139414/
神道の逆襲 https://www.amazon.co.jp/dp/4061495607/

前者はイスラム教を、後者は神道を現代的に解釈したおした書籍です。
どうか今の時代において他の宗教への尊重も人類には必要なのだということを(百もご承知だとは思いますが)理解していただくことはできないかと考える日々です。
# もちろん仏教徒もエホバの証人を理解すべきでしょう

僕の職歴3

ちょっと人物紹介をはじめてみようと思います。第一回の今夜はEさんです。

Eさんとぼくが某社で出会ったのは新人研修が終わったあと、職場配属OJTにてでした。当時某チームではペアリーダが二人、新人につくことになっていました。1年間の研修テーマの運用面を見る人と、そのテーマの技術的な面をささえる人の二人です。

ぼくの研修テーマは以前書いたとおりbootloaderの開発だったのですが、その前に仕事に慣れるために新人二人でEthernet MACのテストプログラムを書くことになっていました。しかし所詮新人です。libcのないところでC言語を書いたこともなければ、DMAについてもよく知らないわけです。
MACの仕様書はあるのですが、そこそこ分厚い本でしかも英語でした。そもそも何がわからないのかさえわからない状態におちいってしまいました。

そこでEさんに教えてもらおうと思ったのですが、
「この本全部読んだの?」
と聞かれました。
残念ながらそのページの全てを読んでいたわけではありませんでした。ただ少しズルをして手っ取り早く知識を得たかったのです。するとEさんはその仕様書を床に投げて、ディスプレイに目をもどしてしまいました。かなり傷付いて本をひろってあたりを見回したのですが、誰もフォローしてくれません。自分でやるしかないんだな、と思いました。そのMACのテストは新人の同期ががんばってくれてなんとかなりました。

Eさんはいつもは机で寝ているか、歯磨きしているか、単行本を読んでいるかのどれかなのですが、なぜか仕事のoutputだけは順調に出すという魔法使いでした。

数年後、なぜかEさんとは仲良しになりました。Eさんは色々なことを知っていました。当時のWindows Updateがなぜ機器によって失敗することがあるのか。WindowsのAPIのよくわからない話。スレッドについて。文字コードについて。COCOMの輸出規制について。なぜかカーボンナノチューブについての議論が掲示板に。

あの時、どうして彼が厳しい態度であったのかは、10年後になった今やっと実感できるようになりました。

僕の職歴2

bootloaderの開発が一段落したころ、無線LANチップそのものを開発とする話がありました。無線LANチップの中には実は小さなCPUが入っていて、そのCPU上で動作するプログラムを書くという案件です。やったことがない仕事をするのが大好きだったので、一にも二にもなくとびつきました。

まずAtherosのホスト側ドライバのソースコードが公開されていたので、それを読んで気になるところをメモしました。その後できあがってきたプロトタイプのでっかいボードの起動確認をしたりしていたのですが、他業務と並行で工数調整をしながら進める能力がかけていて、途中で戦力外通告されてしまいました。プロジェクトに大変迷惑をかけましたが、安易に仕事を引き受けてはいけないという良い経験になりました。

そうこうしている内に新製品のBIOSのメーカを既存製品と違う会社にしようという案件がもちあがりました。英語が苦手でしょうがなかったのですが、米国東海岸に行って身振り手振りでOSサイドからBIOSへの要求項目を説明したら1週間程度である程度動作するBIOSを作ってくれました。あの時ぼくのつたない英語力を使う機会をくれたKさんには感謝しています。

その後にアサインされたのは巨大な組込みシステムの起動時間を10秒にする、というプロジェクトでした。この10秒というのはkernelの起動だけではなく、BIOS=>OS=>アプリ=>画面表示の全てを10秒におさえなければなりません。まず最初に左記の起動シーケンスを横断で測定できる簡単なツールを開発しました。これで、測定にかかる手間を一気に削減できました。その後、各ステージでかかっている時間が長いものから順番に削減検討しました。本来は各アプリの開発担当を呼んで、削減依頼をかけるべきです。しかし、IPCでからみあった起動シーケンスは定常状態とは異なり、1アプリの中だけで完結しません。アプリAの処理に時間がかかっているのは、アプリBの処理待ちで、さらにアプリBはディスクのmountを待っている、ようなことが多発していた訳です。そこで、一旦一人で起動ログを横時間軸の散布図にして、ギャップの大きい部分にしぼり、その処理待ち合わせの依存を解析しました。その解析結果もってアプリの修正をコンサルタントするようにしました。

このような方法を取ったのですが、それでも10秒を達成するのは困難でした。ディスクの読み込みに時間がかかっていたためです。そこで、アプリを画面表示に必須なものと、そうでないものの二種類に分けて、前者のみをディスクから読み込み/起動、後者は画面表示が完了してから読み込むようにしました。この方法で10秒起動を達成できたのですが、アプリのIPC接続関係が変動するとバグを引き起こすという諸刃の剣です。当然、機種が出る度になんらかの障害を引き起こしてしまうことになりました。もっと良い方法がなかったのか、今でも悩むことがあります。

モナドって何だろうか

モナドって何だろうかということを昔考えていたときのメモが見つかったので、以下にはりつけておこうと思います。何かの役に立てば。


@s_h_i_g_e_chan さんと勉強会をしました。前回の勉強会で疑問だったモナドの別の例を学ぶためです。

結局モナドってなんなんだろうと思って図にしてみたが、Haskell文法以上の何かにさえなりませんでした。。。Haskell文法以上に抽象化した表現はできないということでしょうか。

まず↓のようなdo文があったとしましょう。

↑を>>=に変換すると↓のようになるわけです。

ここまではどのようなモナドでも同じ形を取ります。というかHaskell文法そのものです。
例として以下のようなdo文を例にして、もっと詳しく処理内容を見てみましょう。

-- リストモナド定義
instance Monad [] where
  m >>= f  = concatMap f m
  return x = [x]
  fail s   = []
instance MonadPlus [] where
  mzero = []
  mplus = (++)
-- do文の例
do x <- [1,2,3]
   y <- [3+x,6+x]
   [x,y]

どのようなモナドかわかれば、具体的な実行イメージはできます。

前回の勉強会ではdo文が一行実行したら次の行を実行していっているように見えましたが、リストモナドは使い方によってはツリー状に次の行が分裂して実行されていくように見えます。

なぜそのようなことになるかというと、>>=がconcatMapになっているためです。concatMapは「第一引数の関数を第二引数の要素それぞれに適用して、その結果のリストをconcatする」ように動作するため、第一引数で指定された関数(この場合はλxだったりλyだったり)がリストの個数だけ実行されます。

。。。なんか言えば言うほど当たり前のことしか説明できないのですが、>>=によってdo文の次の行がどのように実行されるのか、いかようにも決められるワケです。それでもdo文のλスコープによって計算は前後に分離されます。do文が出現したら順序制御したいんだなって思えばいいのかな?

そーゆーワケでリスト内包表記はリストモナドのdo文です。なるほどです。

-- do文で
do x <- [1,2,3]
   y <- [3+x,6+x]
   return (x,y)
-- リスト内包表記で
[(x,y) | x <- [1,2,3], y <- [3+x,6+x]]

.