[Scala] Talk on scala-be's "Step by Step Scala" on 12/22

　東京のScala勉強会であるscale-beの、12/22開催のStep by Step Scala [vol.06]@scala-be (ATNDへのリンク)で講師をすることになりました。
　今回は主として14章の「表明と単体テスト」のScalaCheckの使い方を中心に話をしようと思っています。ScalaCheckは「満たすべき性質を記述する」ことでテストケースを自動生成してくれる面白い単体テストツールですが、従来のxUnit系テストツールとはちょっと使い方が違うというのもあって、使い方を学ぶには良いのではないかと思います。
　参加者希望者は上記のATNDのリンクから申し込みをしていただければと思います。
　今回は日程が12/22と多くの忘年会と重なる日で、割と参加者は少なそうでちょっと残念。

[Scala] Scala Style Guide

Scala Style Guide (PDF)

Scalaのコーディングスタイルガイド。

[scala] Proposed Style Guideで議論されていて、Oderskyもコメントしてる。これが叩き台になって正式版が出たら訳すといいかなぁ。

[Scala][Book] Pro Scala: Monadic Design Patterns for the Web

APressからPro Scala: Monadic Design Patterns for the Webという本が出る様です。
今までの職業的プログラマの視野に入っていなかったが、実は実用的にも重要である概念の、
- Monadic design patterns
- Zippers and data type differentiation
- Delimited continuations
を考察するとのこと。

「モナド＝デザインパターン」というのはあちこちで書かれていることだし、モナドに限らず圏論的視点で計算を考えようという話は檜山さんのブログで繰り返し出て来るテーマ（11/28開催のセミナーのコパスタを食べる余会はまだ空席があるようですよ）。
Delimited continuationということはScala 2.8対応だし、限定継続を一般向けに紹介した本は今までにあるのかなぁ？なんかそれだけでも価値があるよね。

なんか非常に楽しみな本ですね。

[Event] Recent Days

今週は、Step by Step Scala [vol.04]@scala-beで話をしたり、Haskellナイトを見に行ったり、Scala Hack-a-thon #1に参加したり、でした。

Step-by-Step Scalaは、（少なくとも何人かの方には）Swarmについて興味を持ってもらえた様なので満足。この先の仕事の状況がまだ確定しないのだけど、また機会があればScalaの講師を出来ればなぁ、とか。

Haskellナイトは、本の話がちょっと多過ぎたかなぁとは思うのだけど、出版合わせのイベントだから仕方がないのかなぁ。もうちょっとHaskellの話を聞きたかったかも。

Scala Hackathonは存在を知った時には既に満員になっていて参加を諦めてたんですが、当日朝見たらキャンセルが大量に出たみたいで慌てて家を出た次第。yuroyoroさんの作成したテキストが良く出来ていて、みんな黙々とそれを読んでいたのかな？かつ、質問はtwitterで主として行われていたみたい。懇親会も楽しく参加させて頂きました。

[Scala] Talk on scala-be's "Step by Step Scala" in November

東京のScala勉強会にscale-beというのがありまして、隔週の水曜or木曜の夜に新宿の豆蔵で開催しています。
内容はOderskyの「Scalaスケーラブルプログラミング」の章立てに沿って講師がScalaを解説するというもので、読書会の様にテキストに厳格に沿う訳ではありません。
参加者は、

• 出来れば該当の本を持参して下さい。本の内容を逐一全部話す訳ではないですし。
  
• 出来れば最近のScala実行系（Scala 2.7系）がインストールされたノートPCを持参して下さい。簡単な課題とか、実際に自分でインタプリタ上で動作確認したり、などがあるので。同様に、Scala APIドキュメント（JavaDoc）などをインストールしておくと良いです。（なお、会場はコンセントは利用可能ですが、インターネット接続は提供されません。）
  

あと、勉強会の後に懇親会も行っています。

で、11/4(Wed), 11/19(Thr)の２回は私が講師を担当する事になりました。それぞれ6,7章と8,9章の範囲について話す予定です。11/19の回にはテキストの内容からちょっと離れて最近のScalaの話題という事でSwarmの話をちょっとだけ紹介しようと思ってます。

なお、参加申し込みはATND上で行われ、ATNDへのリンクを含む開催案内は定期的にscala-be上で告知されます。
では、11月に勉強会会場でお会いしましょう。

---
追記：11/21

２回の発表で使用した資料はPDF形式でscala-be Google groupのファイル置き場で公開してます。

[Agda] Install Agda on Mac OS

Mac OS 10.5 の上にAgdaをインストールしました。基本的にはAgda Wikiを参考にしたのだけど、そのままではうまく動きませんでした。

• Xcodeをインストール。DVDからなり、ADCのサイトなりから。最新版は10.6用なので古いのをインストール。
  
• Mac Portsのインストール。/opt/local/binにPATHを通す。Mac Portsの準備が済んでいる人もsudo port -v selfupdateする。
  
• GHCはportsからインストールすると古くて駄目なので、GHC download pageよりバイナリパッケージを導入。
  
• sudo port install hs-cabalして、sudo cabal updateして、~/.cabal/binにPATHを通す。
  
• sudo port install darcs
  
• sudo cabal install happyして、sudo cabal install alex
  
• sudo cabal install Agda-executable
  
• cd ~/.cabal/binして、./agda-mode setup
  
• emacsは薦められるままにAquamacsを導入する。
  
• 下記を~/.emacsに追加。
  
(setq load-path (cons "~/.cabal/share/Agda-2.2.4/emacs-mode/" load-path))
(autoload 'agda2-mode "agda2-mode" "Major mode for Agda2 files" t)
(unless (assoc "\\.agda" auto-mode-alist)
(setq auto-mode-alist
(nconc '(("\\.agda" . agda2-mode)
("\\.alfa" . agda2-mode)) auto-mode-alist)))

  
• Aquamacsを起動し、~/test.agdaというファイルを作成して、
  
module test where

data Bool : Set where
  true : Bool
  false : Bool

  と書く（true, falseの前のインデント必須。単語や:の前後に空白があるのも確認。）
  C-c C-lで入力内容が処理され、文字が色分けされたら、agda2-modeが動いている。
  

---
追記: ~/.emacsについて念のため全部掲載。haskell-modeの設定も重要らしいので。

(setq load-path (cons "‾/.cabal/share/Agda-2.2.4/emacs-mode/" load-path))
(autoload 'agda2-mode "agda2-mode" "Major mode for Agda2 files" t)
(unless (assoc "¥¥.agda" auto-mode-alist)
(setq auto-mode-alist
(nconc '(("¥¥.agda" . agda2-mode)
("¥¥.alfa" . agda2-mode)) auto-mode-alist)))
(setq load-path (cons "‾/lib/elisp/haskell" load-path))
(setq auto-mode-alist
(append auto-mode-alist
'(("促促.[hg]s$" . haskell-mode)
("促促.hi$" . haskell-mode)
("促促.l[hg]s$" . literate-haskell-mode))))
(autoload 'haskell-mode "haskell-mode"
"Major mode for editing Haskell scripts." t)
(autoload 'literate-haskell-mode "haskell-mode"
"Major mode for editing literate Haskell scripts." t)
(add-hook 'haskell-mode-hook 'turn-on-haskell-decl-scan)
(add-hook 'haskell-mode-hook 'turn-on-haskell-doc-mode)
(add-hook 'haskell-mode-hook 'turn-on-haskell-indent)
(add-hook 'haskell-mode-hook 'turn-on-haskell-ghci)

(setq haskell-literate-default 'latex)
(setq haskell-doc-idle-delay 0)


(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))


[Agda] Agda Lectures at CVS

産業技術総合研究所の研修コース「 Agda による仕様記述」に参加しました。

以下は私の参加した10月の回の話。もしかしたら11月は10月の参加者の反応を見て内容が変更されるかもしれません。

一言で言うと
Coq, Agda のような定理証明系とか依存型の関数型言語とかに興味のある人が、概要を知るには良い二日半のコース。参加費無料なのもポイントが高い。お薦め。（開催が大阪なんで関西周辺以外の人にはちょっと厳しいが）

もう少し詳しく説明すると
「Agdaの持つ依存型の機能を使って、仕様の制約を型として表現すれば、機械的に検証出来るよね」というところに主眼を置いているみたいです。なので、定理証明の部分は従であり、主眼は仕様を書ける様になろう、ということのようです。
とはいえ、仕様の制約をAgdaで書く以上、書いた関数が仕様を満たしていることを示す必要がある訳ですが...。

が、まぁ当たり前と言えば当たり前なんですが、二日半ではAgdaを使いこなせるようにはならなかった...。まぁJavaだってHaskellだって二日半では使える様にはならない訳で、当然というか仕方が無い。なので、「Agdaがどんなものなのかの概説を聞く」ぐらいに考えていたほうが良いです。
とはいえ、Agdaに関する日本語の資料はほとんど無い現状で、テキストの説明を聞き、判らないところを教わりつつのハンズオン実習がある訳で、価値は大きい。

参加者は結局８名。堅苦しさの無い普通のIT系勉強会のようなフレンドリーな雰囲気で、質問しまくりみたいな。逆に言うと講義内容がまだきっちりと固まっている訳では無い感じです。
にわとり小屋でのプログラミング日記のCoqな今井さんとお近づきになれたのも良かったです。数人で２日目の夜に懇親会したのですが、最初からちゃんと計画して全員（講師の方にも声をかけて）でやれば良かったと反省。
＃話に出た紫色の本は、"Handbook of Practical Logic and Automated Reasoning" (John Harrison, Cambridge Univ. Press, 2009) です＞今井さん。

とにかく私は楽しかったです。代休消化で関西旅行した価値がありました。参加させて頂き、ありがとうございました＞CVSの方々。

参加の前提について
募集要項には「プログラムを書いた経験(言語不問)、またはシステムやソフトウェアの設計に従事したことがあること。」「Emacs で文書を作成編集した経験があること。」と書いてあるんですが...。
うーむ、HaskellとかOCamlとかの類の型付き関数型言語の初歩的な知識があったほうがいいかも。モナドとか別に知らなくてもいいけど、簡単な再帰とかパターンマッチとか使って List の map とか length とかぐらい書けたほうが良いかもしれないです。そうでないと初日の演習問題でいきなり困るかも。あとはまぁ、ペアノの自然数( 3 = succ(succ(succ(zero))) みたいな話 ) も知ってた方が良いかなぁ。
ただ、参加者の関数型言語への習熟度を見て調整していたかも知れないので、11月はどうなるかは判らないです。

[Scala] sbt : simple-build-tool (1)

sbt (simple-build-tool) は Scala で書かれたビルドツールです。
これもscalaで書かれたDSL的なツールであり、プロジェクトのビルドの設定などをscalaで記述する事が出来たりします。

試しに使ってみて、使い方が判ったら追記していこうと思います。

★インストール

Setupのページに従い作業します。
私は MacOS ユーザなので Unix の指示に従い作業。

まずsbt-launcher-0.5.1.jar をダウンロードして指示通り~/binに置き、~/bin/sbt ファイルを作り chmod したりします。

% ls ~/bin
sbt   sbt-launcher-0.5.1.jar
% cat ~/bin/sbt
java -Xmx256M -jar `dirname $0`/sbt-launcher-0.5.1.jar "$@"
%

★動作確認
空の (*.scala の無い) 作業ディレクトリに hw.scala を作ります。(main メソッドを探して自動で判断する都合上、無関係なソースがあると巧く動作しません。最初それで失敗しました。)

% ls
hw.scala
% cat hw.scala
object Hi { def main(args: Array[String]) { println("Hi!") } }
% 

とりあえず下記の様に動きました。

[apple-3:~/work/scala/hw] miyamoto% ~/bin/sbt 
Project does not exist, create new project? (y/N/s) : s
:: loading settings :: url = jar:file:/Users/miyamoto/bin/sbt-launcher-0.5.1.jar!/org/apache/ivy/core/settings/ivysettings.xml
:: retrieving :: sbt#boot
 confs: [default]
 2 artifacts copied, 0 already retrieved (9831kB/149ms)
:: retrieving :: sbt#boot
 confs: [default]
 3 artifacts copied, 0 already retrieved (3171kB/26ms)
[info] Building project scratch 1.0 using sbt.DefaultProject
[info]    with sbt 0.5.1 and Scala 2.7.5
[info] No actions specified, interactive session started. Execute 'help' for more information.
> run
[info] 
[info] == compile ==
[info]   Source analysis: 1 new/modified, 0 indirectly invalidated, 0 removed.
[info] Compiling main sources...
[info] Compilation successful.
[info]   Post-analysis: 2 classes.
[info] == compile ==
[info] 
[info] == run ==
[info] Running Hi ...
Hi!
[info] == run ==
[success] Successful.
[info] 
[info] Total time: 2 s
> quit
[info] 
[info] Total session time: 14 s
% 

この結果として下記の様にプロジェクトが生成されます。このあたりは Maven とかと同様な感じ。各プロジェクト毎にscala-compiler.jarを持ったりするのは、なんか富豪的だなぁ。

% ls -RCF
hw.scala project/ target/

./project:
boot/   build.properties

./project/boot:
scala-2.7.5/

./project/boot/scala-2.7.5:
lib/  sbt-0.5.1/ update.log

./project/boot/scala-2.7.5/lib:
scala-compiler.jar scala-library.jar

./project/boot/scala-2.7.5/sbt-0.5.1:
ivy-2.0.0.jar  jsch-0.1.31.jar  sbt_2.7.5-0.5.1.jar

./target:
analysis/ classes/

./target/analysis:
applications  external  hashes
dependencies  generated_files  tests

./target/classes:
Hi$.class Hi.class
% 

[Scala] S-99: Ninety-Nine Scala Problems (P01-28)

S-99: Ninety-Nine Scala ProblemsのList編(P01-P28)の抄訳です。

• アスタリスクの数は難易度です。


• 効率も大事ですが、エレガントな回答を求めます。可能ならばより簡潔で、計算量が少なく、末尾再帰になっている回答を作りましょう。


• Scalaの組み込み関数を使ってもOKです。が、使わないほうが勉強になります。


• 答えが知りたければ、元の英語文書の各問題のリンクをクリックして下さい。

P01 (*) リストの最後の要素を求めよ。

scala> last(List(1, 1, 2, 3, 5, 8))
res0: Int = 8


P02 (*) リストの最後から二番目の要素を求めよ。

scala> penultimate(List(1, 1, 2, 3, 5, 8))
res0: Int = 5


P03 (*) リストのn番目の要素を求めよ。但しリストの最初の要素は0番目とする。

scala> nth(2, List(1, 1, 2, 3, 5, 8))
res0: Int = 2


P04 (*) リストの要素の数を求めよ。

scala> length(List(1, 1, 2, 3, 5, 8))
res0: Int = 6


P05 (*) リストを逆順にせよ。

scala> reverse(List(1, 1, 2, 3, 5, 8))
res0: List[Int] = List(8, 5, 3, 2, 1, 1)


P06 (*) リストが回文になっているか調べよ。

scala> isPalindrome(List(1, 2, 3, 2, 1))
res0: Boolean = true


P07 (**) ネストされたリスト構造を平坦化せよ。

scala> flatten(List(List(1, 1), 2, List(3, List(5, 8))))
res0: List[Any] = List(1, 1, 2, 3, 5, 8)


P08 (**) リスト要素の連続した重複物を除去せよ。もしリストの要素で繰り返し要素が含まれていたならば要素一つに置き換えよ。要素の順序は変えてはならない。

scala> compress(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[Symbol] = List('a, 'b, 'c, 'a, 'd, 'e)


P09 (**) 連続した重複物を子リストに纏めよ。もしリストの要素が繰り返し要素ならば、別々の子リストに分割せよ。

scala> pack(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[List[Symbol]] = List(List('a, 'a, 'a, 'a), List('b), List('c, 'c), List('a, 'a), List('d), List('e, 'e, 'e, 'e))


P10 (*) リストをランレングス・エンコードせよ。P09の結果を用いていわゆるランレングス・エンコーディングによるデータ圧縮法を実装せよ。連続した重複要素はタプル(N,E)にエンコードされる。但しNは要素Eの重複数。

scala> encode(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[(Int, Symbol)] = List((4,'a), (1,'b), (2,'c), (2,'a), (1,'d), (4,'e))


P11 (*) 修正ランレングス・エンコーディング。P10の結果を修正し、もし要素に重複が無ければ単に要素を結果にコピーせよ。重複している要素だけを(N,E)の形に変換せよ。

scala> encodeModified(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[Any] = List((4,'a), 'b, (2,'c), (2,'a), 'd, (4,'e))


P12 (**) ランレングス・エンコードされたリストをデコードせよ。P10の仕様で生成されたランレングス・エンコードされたリストを元の圧縮されていないものに戻せ。

scala> decode(List((4, 'a), (1, 'b), (2, 'c), (2, 'a), (1, 'd), (4, 'e)))
res0: List[Symbol] = List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e)


P13 (**) リストのランレングス・エンコーディング（直接解法）。いわゆるランレングス・エンコーディングを直接実装せよ。すなわち（P09のpackの様な）自分で書いた他のメソッドを使ってはならない。直接書く事。

scala> encodeDirect(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[(Int, Symbol)] = List((4,'a), (1,'b), (2,'c), (2,'a), (1,'d), (4,'e))


P14 (*) リスト要素を重複させよ。

scala> duplicate(List('a, 'b, 'c, 'c, 'd))
res0: List[Symbol] = List('a, 'a, 'b, 'b, 'c, 'c, 'c, 'c, 'd, 'd)


P15 (**) 指定した個数、リスト要素を重複させよ。

scala> duplicateN(3, List('a, 'b, 'c, 'c, 'd))
res0: List[Symbol] = List('a, 'a, 'a, 'b, 'b, 'b, 'c, 'c, 'c, 'c, 'c, 'c, 'd, 'd, 'd)


P16 (**) 毎N番目の要素を除去せよ。

scala> drop(3, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: List[Symbol] = List('a, 'b, 'd, 'e, 'g, 'h, 'j, 'k)


P17 (*) リストを二つに分割せよ。前半の長さは与えられるものとする。結果はタプルで返す。

scala> split(3, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: (List[Symbol], List[Symbol]) = (List('a, 'b, 'c),List('d, 'e, 'f, 'g, 'h, 'i, 'j, 'k))


P18 (**) リストのスライスを抽出せよ。二つの添字 i と j が与えられたとき、スライスとは元のリストの i 番目の要素を含むが j 番目の要素を含まないリストである。要素は0番目から始まるとする。

scala> slice(3, 7, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: List[Symbol] = List('d, 'e, 'f, 'g)


P19 (**) リストの要素をn個左ローテートせよ。

scala> rotate(3, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: List[Symbol] = List('d, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'a, 'b, 'c)

scala> rotate(-2, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res1: List[Symbol] = List('j, 'k, 'a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i)


P20 (*) リストのk番目の要素を除去せよ。除去されたリストと除去した要素をタプルで返せ。要素は0番目から始まるとする。

scala> removeAt(1, List('a, 'b, 'c, 'd))
res0: (List[Symbol], Symbol) = (List('a, 'c, 'd),'b)


P21 (*) リストの指定された場所に要素を追加せよ。

scala> insertAt('new, 1, List('a, 'b, 'c, 'd))
res0: List[Symbol] = List('a, 'new, 'b, 'c, 'd)


P22 (*) 与えられた範囲の整数のリストを作れ。

scala> range(4, 9)
res0: List[Int] = List(4, 5, 6, 7, 8, 9)


P23 (**) リストから指定された数だけ値をランダムに選択せよ。（ヒント：P20を使え）

scala> randomSelect(3, List('a, 'b, 'c, 'd, 'f, 'g, 'h))
res0: List[Symbol] = List('e, 'd, 'a)


P24 (*) ロト：1〜Mからn個の異なるランダムな値を選べ。

scala> lotto(6, 49)
res0: List[Int] = List(23, 1, 17, 33, 21, 37)


P25 (*) 要素のランダムな順列を作成せよ。（ヒント：P23を使え）

scala> randomPermute(List('a, 'b, 'c, 'd, 'e, 'f))
res0: List[Symbol] = List('b, 'a, 'd, 'c, 'e, 'f)


P26 (**) n要素数のリストからk個の異なるオブジェクトを取り出す組み合わせを生成せよ。12人から3人の委員会を作る方法は何通りだろうか？答えは C(12,3)=220通り（C(n,k）はよく知られた二項係数）である。数学者にとってはこれで十分であるが、我々は本当に全ての解を生成したい。

scala> combinations(3, List('a, 'b, 'c, 'd, 'e, 'f))
res0: List[List[Symbol]] = List(List('a, 'b, 'c), List('a, 'b, 'd), List('a, 'b, 'e), ...


P27 (**) 集合の要素を、互いに素な部分集合に纏めよ。
a) 9人の人をそれぞれ2,3,4人の３グループに纏める方法は何通りか？全ての組み合わせを生成する関数を書け。

scala> group3(List("Aldo", "Beat", "Carla", "David", "Evi", "Flip", "Gary", "Hugo", "Ida"))
res0: List[List[List[String]]] = List(List(List(Aldo, Beat), List(Carla, David, Evi), List(Flip, Gary, Hugo, Ida)), ...

b) 上の問題を一般化してグループの大きさのリストを与えるとグループのリストを与える様にせよ。グループメンバーの順列は求めていない、すなわち((Aldo,Beat),...)は((Beat,Aldo),...)と同じ解である。しかし、((Aldo,Beat),(Carla,David),...)は((Carla,David),(Aldo,Beat),...)と異なる解である。

scala> group(List(2, 2, 5), List("Aldo", "Beat", "Carla", "David", "Evi", "Flip", "Gary", "Hugo", "Ida"))
res0: List[List[List[String]]] = List(List(List(Aldo, Beat), List(Carla, David), List(Evi, Flip, Gary, Hugo, Ida)), ...

この組み合わせ問題に関して知りたければ離散数学の良い本で「多項係数」について調べよ。
P28 (**) リストのリストを長さでソートせよ。
a) 要素がリストであるリストを考える。そのリストの要素を長さでソートする、すなわち短いリストを前に、長いリストを後にする。

scala> lsort(List(List('a, 'b, 'c), List('d, 'e), List('f, 'g, 'h), List('d, 'e), List('i, 'j, 'k, 'l), List('m, 'n), List('o)))
res0: List[List[Symbol]] = List(List('o), List('d, 'e), List('d, 'e), List('m, 'n), List('a, 'b, 'c), List('f, 'g, 'h), List('i, 'j, 'k, 'l))

b) 次に同様にリストを長さでソートするが、今回は長さの頻度でソートする。すなわち稀な長さのものを前に、頻度の高い長さのものを後ろにする。例の場合、長さ４と１のリストはただ１度しか現れない。3番目と4番目は長さ3のリスト２つである。最後に３つの最も頻度の高い長さ２のリストが現れる。

scala> lsortFreq(List(List('a, 'b, 'c), List('d, 'e), List('f, 'g, 'h), List('d, 'e), List('i, 'j, 'k, 'l), List('m, 'n), List('o)))
res1: List[List[Symbol]] = List(List('i, 'j, 'k, 'l), List('o), List('a, 'b, 'c), List('f, 'g, 'h), List('d, 'e), List('d, 'e), List('m, 'n))


[Scala] Sudoku in Scala

Scalaユーザ会5/22(金)19：00-21：00@新宿三井ビル3で話をする予定の「Scalaで数独を解く」話です。

ScalaSudoku.pdf : プレゼン資料
Sudoku.scala : ソースコード

[Joke] Translation of "A Brief, Incomplete, and Mostly Wrong History of Programming Languages"

A Brief, Incomplete, and Mostly Wrong History of Programming Languagesの翻訳です。面白かったので翻訳してみました。

「簡潔で不完全でほとんど間違っているプログラミング言語の歴史」

1801 - Joseph Marie Jacquardが、織機にパンチカードで命令することで、タペストリーに「hello, world」を織り込んだ。（しかし）末尾再帰やコンカレンシーの欠如、あるいは適切に大文字が使用されていないため、当時のRedditerたちは感銘を覚え無かった。

1842 - Ada Lovelaceが最初のプログラムを書いた。その過程に於いて、コードを走らせる実際のコンピュータを持っていないという些細な困難に妨げられた。後のエンタープライズアーキテクトたちは、UMLでプログラムする為に、彼女のテクニックを再習得した。

1936 - Alan Turingが、（将来に亘る）全てのプログラミング言語を発明した。しかし彼がその特許をとる前に、英国情報部は彼を007にするために強制徴募した。

1936 - Alonzo Churchもまた、（将来に亘る）全てのプログラミング言語をさらにうまく発明した。彼のλ算法はC言語に十分似ていない為に無視された。この批判は、当時まだCが発明されていないという事実にも関わらず生じた。

1940年代 - 結線とスイッチによって様々な「コンピュータ」が「プログラム」された。「タブ vs 空白」の論戦を避けるために、技術者たちはこの方式を採用した。

1957 - John BackusとIBMがFORTRANを作った。IBMにもFORTRANにも面白いところは何も無い。青いネクタイを着用せずFORTRANを書くのは文法エラーである。

1958 - John McCarthyとPaul GrahamがLISPを発明する。戦後の戦略的括弧備蓄の枯渇による高コストの為、LISPは決してポピュラーにはならなかった[1]。ポピュラーでは無いにも関わらず、LISP (今では "Lisp" あるいは時には "Arc") は「再帰と他人を見下すことなどの重要なアルゴリズム技法」に於ける影響度の高い言語であり続けている。

1959 - L. Ron Hubbardとの賭けに負けた後に、Grace Hopperを含む何人かのサディスト達が「大文字化された定型文志向言語」 (Capitalization Of Boilerplate Oriented Language = COBOL) を発明する。後に、Hooper提督のCOBOLの業績に対する見当外れで性差別的な報復として、Rubyコンファレンスでは嫌女性的題材が取り上げられる。

1964 - John KemenyとThomas Kurtzが、非計算機科学者の為の非構造化プログラミング言語であるBASICを作った。

1965 - KemenyとKurtzはGO TO 1964.

1970 - Guy SteeleとGerald SussmanがSchemeを作った。彼らの著作は「Lambda the Ultimate」の一連の論文をもたらし、「究極の台所用品ラムダ」にその頂点を迎えた。この論文はロングランの基礎となったが、深夜のインフォマーシャルとしては究極的に失敗であった。Javaがラムダを持たないことによってラムダをポピュラーにするまでラムダは比較的目立たないところへと左遷された。

1970 - Niklaus Wirthが手続き型言語のPascalを作った。Pascalは直ちに批難されたが、"x := x + y"という構文を、より親しみやすいC的な"x = x + y"の代わりに使用したためであった。この批判は、当時まだCが発明されていないという事実にも関わらず生じた。

1972 - Dennis Ritchieは前後を同時に撃つことの出来る強力な銃を発明した。発明のもたらした多くの死者及び障害者に満足することなく、彼はCとUnixを発明した。

1972 - Alain Colmerauerは論理型言語Prologをデザインした。彼の目標は二歳児の知性を持った言語を作ることであった。全てのクエリに「No」と答えるPrologセッションを示すことによって、目標に達したことを証明した。

1973 - Robin MilnerはM&M型理論に基づく言語のMLを作った。MLの子供として形式仕様意味論を持つSMLが生まれた。形式意味論の形式意味論を質問されてMilnerの頭は爆発した。ML一家の他の良く知られた言語にはOCaml, F#, Visual Basicがある。

1980 - Alan kayはSmalltalkを作り、用語「オブジェクト指向」を発明した。その意味を聞かれると彼は「Smalltalkのプログラムは単にオブジェクトである」と答えた。オブジェクトは何から作られるのかを聞かれると彼は「オブジェクトだ」と答えた。再度質問されると彼は云った。「だからさ、下の下まで全部オブジェクトなんだってば。亀にたどり着くまでは。」

1983 - Bjarne Stroustrupは耳にしたもの全てをCにねじ止めすることでC++を作った。その結果、言語は非常に複雑になり、プログラムをSkynet人工知能でコンパイルするために未来へ送らねばならなかった。ビルド時間は犠牲となった。Skynetがサービスを提供し続けた動機は依然としてはっきりしないが、未来からの広報担当はオーストリア訛りで単調に「気にするようなことは何も無い、ベイビー」と云った。Skynetはバッファーオーバーランを飾り立てたものに過ぎないという推測もある。

1986 - Brad CoxとTom LoveがObjective-Cを作り、アナウンスした。「この言語はCのメモリ安全性とSmalltalkの素晴らしい実行速度が結びついたものです。」現代の歴史家たちは二人が失読症であったと疑っている。

1987 - Larry Wallが眠気を催し、キーボードに額をぶつけた。目を覚ましたとき、Larry Wallのモニターの上の文字列はランダムなのではなく、神が預言者Larry Wallにデザインすることを欲しているプログラミング言語のサンプルプログラムだと悟った。Perlが生まれた。

1990 - Simon Peyton-Jones, Paul Hudak, Philip Wadler, Ashton Kutcher そして「動物の倫理的扱いを求める人々の会」からなる委員会は、純粋非正格関数型言語Haskell を作った。副作用を制御するためモナドを使用する複雑さの為、Haskellは抵抗を受けた。Wadler は批判を和らげるために説明した。「モナドは自己準同系ファンクタの圏のモノイドなんだ。何か問題が？」

1991 - オランダ人プログラマのGuido van Rossumが謎の手術の為にアルゼンチンへと旅行した。頭部に大きな傷を負って帰国し、Pythonを発明し、多数の賛同者によって終身独裁者に任じられ、世界に対して「あることをするのにひとつしかやり方がない」と報じた。ポーランドは神経質になっている。

1995 - 「Mad Matz」こと、まつもとゆきひろは、漠然とした特定されない終末を避けるためにRubyを作ったが、その終末においてはオーストラリアはモヒカン戦士とティナ＝ターナーが支配する砂漠となる。その言語は後にRuby on Railsと、真の発明者David Heinemeier Hanssonによって改名された。[まつもとがRubyと呼ばれる言語を発明した云々は実際には起きておらず、この記事の次の改訂時に削除されるべきだ - DHH].

1995 - Brendan Eichはプログラミング言語設計で起きた全ての失敗について読み、自分でも幾つか発明し、LiveScriptを作成した。後にその言語は、Javaの人気に肖る為、JavaScriptと改名された。後になっても、皮膚病の人気に肖る為にECMAScriptと改名された。

1996 - James GoslingはJavaを発明した。Javaは比較的冗長で、ガベージコレクションをし、クラスベースで、静的型付けで、シングルディスパッチで、単一実装継承と複数インタフェース継承のオブジェクト指向な言語である。SunはJavaの新規性を宣伝した。

2001 - Anders HejlsbergがC#を発明した。C#は比較的冗長で、ガベージコレクションをし、クラスベースで、静的型付けで、シングルディスパッチで、単一実装継承と複数インタフェース継承のオブジェクト指向の言語である。MicrosoftはC#の新規性を宣伝した。

2003 - 酔っ払ったMartin Oderskyは誰かのピーナツバターが別の人のチョコレートにくっつくというReeseのピーナツバターカップのCMを見て着想を得た。彼はオブジェクト指向と関数型言語の作り上げたものを統合する言語Scalaを作った。これを見た両派閥とも激怒し、それぞれ直ちに聖戦を宣告した。

Footnotes

1. 計算機科学にとっては幸運なことに、中括弧と山括弧の供給は潤沢であった。
2. Catch as catch can - Verity Stob

[Scala] Jersey with Scala + Jetty

Jersey は JAX-RS (Java API for RESTful Web Service)のreference実装です。
これをScalaで動かしてみます。

1. Libraries : Jetty 6.1.17. Jersey 1.0.3 を使用しました。下記をEclipseプロジェクトのreference librariesに登録

Jetty : jetty-XX.jar, jetty-util-XX.jar, servlet-api-XX.jar
Jersey : jsr311-api-XX.jar, jersey-core-XX.jar, jersey-server-XX.jar, asm-XX.jar

2. test.jersey.JerseyTest.scala : メインルーチンです

package test.jersey

import javax.servlet.ServletException
import javax.servlet.http.HttpServlet
import javax.servlet.http.HttpServletRequest
import javax.servlet.http.HttpServletResponse

import org.mortbay.jetty.Server
import org.mortbay.jetty.nio.SelectChannelConnector
import org.mortbay.jetty.servlet.Context
import org.mortbay.jetty.servlet.ServletHolder

import com.sun.jersey.spi.container.servlet.ServletContainer
  
object JerseyTest {
  def main(args: Array[String]) {
    val server = new Server(8080)
    val connector = new SelectChannelConnector()
    server.addConnector(connector)
    
    val holder:ServletHolder = new ServletHolder(classOf[ServletContainer])
    holder.setInitParameter(
      "com.sun.jersey.config.property.resourceConfigClass",
      "com.sun.jersey.api.core.PackagesResourceConfig")
    holder.setInitParameter(
      "com.sun.jersey.config.property.packages",
      "test.jersey.resource")
// URLをクラスにマッピングする為のpackage名

    val context = new Context(server, "/", Context.SESSIONS)
    context.addServlet(holder, "/*")
    
    server.start()
    server.join()
  }
}

3. test.jersey.resource : /helloworld に対応するリソース

package test.jersey.resource

import javax.ws.rs.GET
import javax.ws.rs.Produces
import javax.ws.rs.Path

@Path("/helloworld")
class HelloWorldResource {
  @GET
  @Produces(Array("text/plain"))
  def getMessage:String = "Hello, World"
}

4. テスト
Eclipseでtest.jersey.JerseyTest をアプリケーションとして実行させます。

2009-05-03 22:56:18.064::INFO:  Logging to STDERR via org.mortbay.log.StdErrLog
2009-05-03 22:56:18.123::INFO:  jetty-6.1.17
2009-05-03 22:56:18.205::INFO:  Started SocketConnector@0.0.0.0:8080
2009-05-03 22:56:18.226::INFO:  Started SelectChannelConnector@0.0.0.0:55736

次いでアクセス

% telnet localhost 8080
Trying 127.0.0.1...
Connected to localhost.
Escape character is '^]'.
GET /helloworld HTTP/1.0

HTTP/1.1 200 OK
Content-Type: text/plain
Server: Jetty(6.1.17)

Hello, WorldConnection closed by foreign host.
% 

2009/05/03 22:57:08 com.sun.jersey.api.core.PackagesResourceConfig init
情報: Scanning for root resource and provider classes in the packages:
  test.jersey.resource
2009/05/03 22:57:08 com.sun.jersey.api.core.PackagesResourceConfig init
情報: Root resource classes found:
  class test.jersey.resource.HelloWorldResource
2009/05/03 22:57:08 com.sun.jersey.api.core.PackagesResourceConfig init
情報: Provider classes found:

[Scala] Scala Servlet with Jetty6

Jetty + ScalaでServletを書いてみました。

1. Projectの作成
Eclipseで普通にScala Projectを作ります。
ScalaServletという名前のScala Projectを作りました。

2. Jetty6 の入手
JettyのサイトからJetty6を入手します。私がダウンロードしたのはJetty 6.1.17でした。
zipを解凍し、jetty-6.1.17.jar, jetty-util-6.1.17.jar, servlet-api-2.5-20081211.jar をプロジェクトにimportします。

3. ソースを書く
パッケージtest.jettyを作って、下記の様なJettyTest.scalaというファイルを作成します

package test.jetty

import javax.servlet.ServletException
import javax.servlet.http.HttpServlet
import javax.servlet.http.HttpServletRequest
import javax.servlet.http.HttpServletResponse

import org.mortbay.jetty.Server
import org.mortbay.jetty.nio.SelectChannelConnector
import org.mortbay.jetty.servlet.ServletHandler

object JettyTest {

  def main(args: Array[String]) {
    val server = new Server(8080)
    val connector = new SelectChannelConnector()
    server.addConnector(connector)
    
    val handler = new ServletHandler()
    handler.addServletWithMapping(HelloServlet.getClass, "/")
    server.addHandler(handler)
  
    server.start()
    server.join()
  }
}

object HelloServlet extends HttpServlet {
  override def doGet(req:HttpServletRequest, resp:HttpServletResponse) {
    val out = resp.getWriter
    resp.setContentType("text/html")
    out.println("<html><body>Hello, World!</body></html>")
  }
}

4.サーバ起動
上記のJettyTest.scalaを普通にScala Applicationとして起動します。
コンソールに下記の様に表示されます。

2009-05-03 02:20:29.316::INFO:  Logging to STDERR via org.mortbay.log.StdErrLog
2009-05-03 02:20:29.358::INFO:  jetty-6.1.17
2009-05-03 02:20:29.392::INFO:  Started SocketConnector@0.0.0.0:8080
2009-05-03 02:20:29.413::INFO:  Started SelectChannelConnector@0.0.0.0:52134

5.アクセス
ブラウザからhttp://localhost:8080/で確認してもOKですがコンソールから確認。

% telnet localhost 8080
Trying ::1...
telnet: connect to address ::1: Connection refused
Trying fe80::1...
telnet: connect to address fe80::1: Connection refused
Trying 127.0.0.1...
Connected to localhost.
Escape character is '^]'.
GET / HTTP/1.0

HTTP/1.1 200 OK
Content-Type: text/html; charset=iso-8859-1
Content-Length: 40
Server: Jetty(6.1.17)

<html><body>Hello, World!</body></html>
Connection closed by foreign host.
% 

[Event] Type-Level Programming Meeting

型レベルプログラミングの会

定員がすぐいっぱいになってしまって会場参加は出来ず、自宅からustreamで拝聴。
発表された皆さん、どれも興味深い話でした。ありがとうございます。

• Scala : Scalaの型プログラミングの話は前にも聞かせて頂いたような気がするけど、更に話題が広がっていたような。


• C++ : 定番ではありながら、私はC++は経験が少ないので興味深く聞けました。


• Haskell : フォロー出来ない話も多かったですが勉強になりました。勉強すべき事、多いなぁ。


• D : 型プログラミングの為のような言語ですね。興味深い。


• 依存型プログラミング : プレゼン資料が大変面白いというか芸達者というか。April Foolの予告のGirardの逆理の話では無かった。


• G'Caml : 存在を始めて知りました。OCaml関係も色々あるなぁ。

この手の勉強会に参加すると、今まで知らなかったことがいっぱいあると判り、もっと勉強しなくちゃ、と思う。
日々の仕事は非技術的な作業ばかりが増えているので、知的好奇心の刺激の為にもこの手の勉強会に積極的に参加しないと。

[Coq] Coq'Art Chap.2

Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions の Chapter 2 です。

この章では概ね次の４つが語られているように見えます。

(1) Coq のコマンド

下記の様なコマンドがあります。

★Require Import library.
ライブラリをロードして environment に追加する。
libraryとしては、Arith, ZArith, Boolなどがある。

★Open Scope scope名.
Scope は notation を interprete する規則。例えばZ_scopeを指定すると各種演算子記号が Z の演算のものと判断される。

★Print Scope scope名.
Scopeで定義された notation の一覧を得る。

★Check term.
termのtypeを表示させる。

★Parameter t:A.
t:Aを environment に追加する。environmentはglobalなもの。

★Section id.

　    ...

　End id.
localなblockを作る。

★Variable t:A.
t:Aを context に追加する。contextはlocal。なので、Section...Endの範囲内で有効。

(2) Inference Rules

様々な推論規則があります。

    (x,A)∈E∪Γ
Var ------------    x:identifier
    E,Γ |- x:A

 E,Γ|- e_1:A->B  E,Γ|- e_2:A
App ------------------------------  関数適用
    E,Γ|- e_1 e_2:B
 
  E,Γ|- e:A_1 -> A_2 -> ... -> A_n -> B   E,Γ|- e_i:A_i (i=1,...,n) 
App* -------------------------------------------------------------------
     E,Γ|- e e_1 ... e_n:B
 
 E,Γ|- t_1:A  E,Γ::(v:=t_1) |- t_2:B
Lam --------------------------------------  λ式
    E,Γ|- fun v:A => e:A->B
 
    E,Γ|- t_1:A  E,Γ::(v:=t_1) |- t_2:B
Let-in --------------------------------------  let
       E,Γ|- let v:=t_1 in t_2:B
    
      E,Γ|- A:Set  E,Γ|- B:Set
Prod-Set --------------------------
         E,Γ|- A->B:Set

  E,Γ|- t:A  E,Γ|- A ≦_{beta delta iota zeta} B
Conv --------------------------
     E,Γ|- t:B

(3) Eval

★cvb : call-by-value (cbvでなくlazyで遅延評価)

★delta-reduction : t ==> t{v/t'}。tのidentifier vをその定義t'で置換。

★beta-reduction : (fun v:T => e_1) e2 ==> e_1{v/e_2}。λ式を簡約。

★zeta-reduction : let v := e_1 in e_2 ==> e_2{v/e_1}。letを簡約。

★iota-reduction : 帰納的な処理で詳しくはChap.6でということで後回し。nat,Zは帰納的な定義なので計算する時はiota-reductionが必須。

★compute = cvb iota beta zeta delta の略

★Eval compute in (....). : ...を実際に計算する。

Reductionに関する性質

• strong normalization : reductionはfinite
  
• confluence : t |> t_1, t |> t_2 ならば、あるt_3があって、t_1 |> t_3 かつ t_2 |> t_3。
  

(4) Universe

typeもtermだとすると、typeのtypeがあるはず。それをsortという。
CoqではSetというデフォルトのsortが定義されている。
更にその上の無限の階層まで考えるようだが、CoqではType(i)は全部ひっくるめてTypeにしてしまう様子。

Level 0 : 具体的な項とか関数。O, S, trinomial,...
Level 1 : データの型。nat, nat->nat, ...
Level 2 : ソート。Set
Level 3 : Type(0)
   :

[Coq] Coq'Art Reading in Tokyo ?

ところで東京近辺でSpringerのCoq本Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructionsに興味のある人っています？
何人かいるようならば読書会でもとか思うのですが。なお、私は素人で型理論の専門家とかではありません。なので他人に教える程の知識は無く、一緒に勉強する感じになってしまいますが。
逆に既に本を読んでいるとかで、私が参加しても構わないグループとかありましたら声をかけて下さい。

[Coq] Coq'Art Chap.1

Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructionsを読み始める事にしました。

Chap.1ではinsertion sortを例にしてCoqの解説が行われています。そこで、Appendixのinsertion sortのコードをCoqIdeに入力してみました。実際に証明が自分で出来る様になるのは将来の課題として、とりあえずCoqでの開発の流れを追ってみます。
なお証明自体はinsertionv8.vにあります。

まず、list Zがソートされた状態を定義するsorted : list Z -> Propを定義します。こんな感じです。

Inductive sorted : list Z -> Prop :=
  | sorted0 : sorted nil
  | sorted1 : forall z:Z, sorted (z :: nil)
  | sorted2 : forall (z1 z2:Z) (l:list Z), 
       z1 <= z2 -> sorted (z2 :: l) -> sorted (z1 :: z2 :: l).

sortedは定義なのでこれ自体は証明の対象ではありません。

これを用いて、

Theorem sorted_inv : 
  forall (z:Z) (l:list Z), sorted (z :: l) -> sorted l.

を証明します。

次いで、並べ替えであることを示すequivを定義します。まず、リストのなかの出現数を示す

Fixpoint nb_occ (z:Z) (l:list Z) {struct l} : nat :=
  match l with
  | nil => 0%nat
  | (z' :: l') =>
      match Z_eq_dec z z' with
      | left _ => S (nb_occ z l')
      | right _ => nb_occ z l'
      end
  end.

を定義します。このnb_occは定義なので証明しません。

これを使って、

Definition equiv (l l':list Z) := forall z:Z, nb_occ z l = nb_occ z l'

を定義します。これ自体も証明しません。

nb_occ, equivの定義から、下記の補題を証明します。

Lemma equiv_refl : 
  forall l:list Z, equiv l l.
Lemma equiv_sym : 
  forall l l':list Z, equiv l l' -> equiv l' l.
Lemma equiv_trans : 
  forall l l' l'':list Z, equiv l l' -> equiv l' l'' -> equiv l l''.
Lemma equiv_cons : 
  forall (z:Z) (l l':list Z), equiv l l' -> equiv (z :: l) (z :: l').
Lemma equiv_perm : 
  forall (a b:Z) (l l':list Z), equiv l l' -> equiv (a :: b :: l) (b :: a :: l').

次いで、実際にinsertion sortを行う関数aux : Z -> list Z -> list Zを定義します。

Fixpoint aux (z:Z) (l:list Z) {struct l} : list Z :=
  match l with
  | nil => z :: nil
  | cons a l' =>
      match Z_le_gt_dec z a with
      | left _ =>  z :: a :: l'
      | right _ => a :: (aux z l')
      end
  end.

auxがinsertion sortの性質を持っている事を示す補題、つまりauxの結果がequivであること、sortedであることを証明します。

Lemma aux_equiv : 
  forall (l:list Z) (x:Z), equiv (x :: l) (aux x l).
Lemma aux_sorted : 
  forall (l:list Z) (x:Z), sorted l -> sorted (aux x l).

最後に、sort:list Z -> list Zを定義というか、sortされた出力の存在を証明します。

Definition sort :　forall l:list Z, {l' : list Z | equiv l l' /\ sorted l'}.

証明を追いきれてないのですが、どうもexists (aux a l')の様に、実例を示して存在を証明するみたいにauxを使っているようです。

----

sorted, nb_occ, equivは定義なので証明の対象ではありません。
aux, sortは成果物として得る、証明済みのプログラムです。sortを満たす具体的なl'の値としてauxを使った式を与えます。その値がl'の条件を満たす事はaux_equiv, aux_sortedから保証されます。

一般的に

• 仕様を表す様な述語(X -> Prop)を書く。仕様に関する補題も証明しておく。
  
• 解を与える様な関数を書く。
  
• その関数の出力が仕様を満たす事を証明する。
  

とかすれば良い様に見えます。

----

ある程度、この本を読み終わった後で、またこのプログラムを振り返ってみたいと思います。