PDF形式のファイルを開くには、Adobe Reader(旧Adobe Acrobat Reader)が必要です。お持ちでない方は、Adobe社から無償でダウンロードできます。
Adobe Reader の入手

 

市民講座

 
 

平成28年度 市民講座「情報学最前線」

第3回
2016年10月20日(木)

正しいプログラムを簡単に書くには?
プログラムの型とそのデバッグ手法

対馬 かなえ (国立情報学研究所 アーキテクチャ科学研究系 助教)


 

講演当日に頂いたご質問への回答(全11件)  

※回答が可能な質問のみ掲載しています。 (この他いくつかの質問への回答を後日掲載予定)

Q1.
型の強い言語と弱い言語があると聞いたことがあります。先生の研究は、どのような言語を対象にしているのですか?
A1.
型の強い言語です。型の強い言語では、実行する前に型に関するエラーを検出してくれるのですが、それを直すのは多くの場合簡単ではありません。どうやったら簡単に直せるのか、というのが私の研究の目的です。
Q2.
OCalmはどのような分野に使われているのでしょうか。
A2.
"企業では一部の金融関係の会社などで使われています。また OCaml に限りませんが、ML (Meta-Language) 系の言語はプログラミング言語の実装に向いています。MinCaml (http://esumii.github.io/min-caml/) という東北大の住井先生のML 系言語の美しい実装がありますので、コンパイラに興味がある方は参照してください。"
Q3.
対馬先生の好きな言語とその理由は何ですか?
A3.
"基本的には強い型付けの言語が好きです。好きな理由は二つあります。一つは事前に型検査してくれた方が実行するときに安心であること。もう一つはプログラムを頭の中で考えるときに、なんらかの抽象化された形(すなわち型) で考えた方が楽だからです。"
Q4.
講師のいう“プログラミング”の簡単な実例を示してください。
A4.
"電卓を使うのも一種のプログラミングです。やってほしい仕事を人間が書いて、コンピュータが実行します。そのやってほしい仕事を書くのがプログラミングになります。関数電卓になると、人が考えるプログラミングにより近くなりますね。"
Q5.
Rubyのまつもとゆきひろさんが、次のRubyバージョンではグローバル型推論を行って形チェックを強化すると言っていました。すでにある大量のライブラリとそのテストプログラムの実行事情報を蓄積して推論の精度を上げて、型を書くことなく強力な型チェックを行うらしいです。このような方法はうまういくと思いますか?
A5.
面白い試みだと思います。ただ、強い型付けの言語は型の規則に関して progress (正しく型付けされるプログラムはおかしな状態になっていない) と preservation (正しく型付けされたプログラムが実行されるならば、実行後も正しく型付けされている) という性質を証明することで、型がついたプログラムは型による実行時エラーがおきないことが保証されています。質問のような方法ではそれらの保証は得られないとは思いますが、もともと型チェックを行っていない言語ですから、多くの実行前型エラーを見つける可能性があると思います。
Q6.
・静的、動的の使い分け、アプリ?動的が流行っていますか?
・何で似た言語が沢山あるのでしょうか?
・手続き・関数・論理型、宣言型言語と型との関係
・型の形
・どのようなツールを使っていますか?ソース、テスト、ローンチ
・プロトコルの正しさ?
・生産効率はどのくらい変わりますか?
A6.
プログラミング言語はコンピュータを動かすための道具です。似たように見えてもいろんな用途の調理器具があるように、それぞれに特化した部分があったりします。また、新しい道具を作りたいというのがわりと自然な人間の欲求でもあるのかなと思います。プログラムを書いているときにそのプログラミング言語になんらかの不満を感じると、新しい言語を作るモチベーションになります。(実は誰かがもう似たものを作っていたりもするのでしょうが ..)
Q7.
P.27、28あたり 十:数*数→数という表現で、*は一般的なoperatorという意図だと思いますが、それ以前のページで掛け算を意味する記号として*を使っているので、説明としてわかりにくくないでしょうか?全然別の記号を使った方がよいのではないかという提案です。
A7.
A * B で A の型と B の型の組 (ふたつの型をひとつにまとめたもの) の型を意味しています。つまり、"数*数→数"は + が要素を二つ受け取り、一つ返す関数である、という意味になります。これは OCaml での記法で、そのまま使ってしまいましたが、違うものの方が分かりやすかったかもしれません。
Q8.
動的型付ヶ言語(Python、Ruby、Java Script)が続行してますか。どう思われていますか?(なお、静的型付ヶ言語(Haskel、Scala)が好きです。コンパイルでエラーを検出してくれた方がたすかると思うのですが・・・)
A8.
Q6の質問への回答のとおり、それぞれの言語には特化した良さがあると思います。私も普段は Haskell、Scala等に代表される強い静的型付け言語を使っていますが、シェルスクリプトを書いたり、Rubyで授業をしたりもします。なにかを書くときに言語による向き不向きもありますので、自分に一番居心地の良い言語をホームにしつつ、他の言語も必要に応じて使ってみるのが一番良いのではないかなと思います。
Q9.
型は最低何種類くらいあれば良いのですか?、多い方が良いのですか?型変換が面倒なのはIDEの入力補助で解決するしかないのでしょうか?
A9.
基本的な型は整数・実数・真偽値・文字列のような限られたもので定義されています。それらを使って自分で新しく必要な型を定義ができる仕組み (C 言語では構造体とか、OCaml では組・レコードなど) があります。ですので、もともとの型が多く定義されている必要はありません。
強い静的型付け (暗黙の型変換が行われない言語) を好む立場から言わせていただくと、明示的に書く必要があるキャストはなんらかの問題が起きる可能性があるのでプログラマに書くことが求められています。プログラムの安全のために、面倒がらずに一度立ち止まってキャストをしても良いのか考えてほしいなと思います。
Q10.
複数の言語を使い分けながら仕事をしています。そもそも、なぜ微妙に文法が異なる言語が次々と生まれるのでしょうか。
A10.
Q6の質問への回答をご参照ください。
Q11.
型推論の方法論について知りたい。OCamlやHaskellのような強い型推論はどのように行われているのでしょうか。
A11.
簡単な例で説明してみましょう。1 + x (ただし x は変数) の型を考えるとします。
+ の型は数字をふたつ受け取って、数字を返す型です。なので、1 と x はそれぞれが数字でなくてはいけません。部分プログラムの 1 について考えてみると、数字が要求されていて、実際に数字なので良さそうです。もうひとつの部分プログラムの x について考えてみると、数字が要求されていますが、それ自身はなんの型でも良いので、x の型も数字だということにします。全体として、1 + x の型は数字になります。これらの推論から、{x:数字} |- 1 + x: 数字 という結論を得ることができます。この (judgement の) 意味は x が数字という前提のもとで、1 + x は数字であると読めます。
このように決められた型の制約 (+ が数字をふたつ受け取って数字を返す型とか、 1 が数字とか) を使って、それらを満たす解を得られるかというのが型推論になります。実際にどのような型の制約を使っているか、どのように型安全性の証明をしているか、多相型等の面白いトピックなどに興味があれば、「型システム入門 プログラミング言語と型の理論 Benjamin C.Pierce 著」を参照してください。

開催プログラム一覧に戻る

お問合せ先

国立情報学研究所 総務部 企画課 広報チーム
〒101-8430 東京都千代田区一ツ橋2-1-2
E-mail: kouhou(a)nii.ac.jp 
※(a)の部分を@に置き換えて送信してください。