第4回

課題2

コメントアウトの形式は色々あると思いますが、筆者はC言語のコメントアウト2つとOcamlの入れ子のコメントアウトの計3つを作りました。

各コマンドは、commentというエントリーポイントを新しく作り、再帰的に呼びだす（「token lexbuf」「comment lexbuf」などとすると、それぞれtoken・commentエントリーポイントが再帰的に呼び出されます）ことで実現しています。 

   1 (* lexer.mll *)
   2 
   3 rule token = parse
   4         | space+                                        { token lexbuf } (* スペース *)
   5         | "(*"                                          { comment1 lexbuf; token lexbuf }       (* コメント１：OCamlの入れ子にできるコメント *)
   6         | "/*"                                          { comment2 lexbuf; token lexbuf }       (* コメント２：C言語のコメントその１ *)
   7         | "//"                                          { comment3 lexbuf; token lexbuf }       (* コメント３：C言語のコメントその２ *)
   8         | ("exit" | "quit" | eof)                       { raise End_of_file } (* 終了用のコマンド *)
   9         | ";;"                                          { EOC } (* コマンド終わり *)
  10         | num+ as lxm                                   { INT (int_of_string lxm) } (* 数字 *)
  11         | "true"                                        { BOOL (true) } (* true *)
  12         | "false"                                       { BOOL (false) } (* false *)
  13 (* 中略 *)
  14         | '_'                                           { ALL }
  15         | ((alp | '_') (alp | num | '_')*) as lxm       { STRING (lxm) }        (* 識別子 *)
  16         | [^'\n']                                       { raise (Failure "lexing: empty token") }
  17 and comment1 = parse
  18         | "*)"  { () }                                  (* 現在の深さのネストから脱出 *)
  19         | "(*"  { comment1 lexbuf; comment1 lexbuf }    (* ひとつ深いネストに入って"*)"が現れるまで読み進み、その後もとのネストで"*)"が現れるまで読み進める。 *)
  20         | eof   { raise (Failure "lexing: eof appeared in comment") }   (* コメント中で入力が終わったらエラー *)
  21         | _     { comment1 lexbuf }                     (* "*)"がでるまで読み進みつづける *)
  22 and comment2 = parse
  23         | "*/"  { () }                                  (* 現在の深さのネストから脱出 *)
  24         | eof   { raise (Failure "lexing: eof appeared in comment") }   (* コメント中で入力が終わったらエラー *)
  25         | _             { comment2 lexbuf }             (* "*)"がでるまで読み進みつづける *)
  26 and comment3 = parse
  27         | "\n"  { () }                                  (* 現在の深さのネストから脱出 *)
  28         | eof   { () }                                  (* コメント中で入力が終わったらエラー *)
  29         | _             { comment3 lexbuf }             (* "*)"がでるまで読み進みつづける *)
  30

課題3

・授業では副作用使うなといわれましたが、個人的には環境の定義に参照とか使っていいと思います。

第5回の課題で再帰関数をつくるみたいですが、そのための方法のひとつに環境を副作用ありのものに変更するというものがあります。

多分半分くらいの人はそちらの方法で実装することになると思うので、今副作用バリバリの環境を作っても特に問題ないように思います。

・今回必要なものは、環境モジュールと、let文や変数が参照されたときの処理です。筆者のlet文などの処理は下のようになりました。 

   1 (**識別子**)
   2 | Id (e1) ->
   3         Env.get e1 env
   4 
   5 (**let in**)
   6 | LetIn (e1, e2, e3)->
   7         let ans = eval env e2 in
   8         Env.add e1 ans env;
   9         let ret = eval env e3 in (Env.remove e1 env; ret)
  10 
  11 (**let**)
  12 | Let (e1, e2) -> 
  13         let ans = eval env e2 in 
  14         Env.add e1 ans env;
  15         ans

MinCamlというOCamlで書かれた小さいMLコンパイラがあり、それを参考にするとほぼそのまま50点は取れる、はず。 -- Naoaki Iwakiri

課題6

・授業では教えられてないのですが次のようなレコードの定義の仕方があります。 

   1 type tp = { f: 'a. 'a -> 'a };;

中括弧の中の「f : 'a. 'a -> 'a」というのは、「fというフィールドは'a->'aという型を持っていて、'aは多相型として扱われます。」という意味です。

イメージとしては 

   1 type 'a tp = { f: 'a -> 'a };;

という書き方と同じようなものだと思えばいいでしょう。

ただしこの二つの書き方は本質的に異なっています。

tp(あるいは'a tp)型の変数を参照するとき、前者の書き方では'aという型変数は多相型として扱われますが、後者では単相型として扱われてしまいます。

例えば、次のようなコードを書くと、 

   1 let test x = x.f x.f;;

tp型を「type tp = {f: 'a. 'a -> 'a}」と定義したときはエラーは吐かれずに「val test : tp -> 'a -> 'a = <fun>」という結果が返ってきますが、 「type 'a tp = {f: 'a -> 'a}」と定義すると「Error: This expression has type 'a -> 'a but an expression was expected of type 'a」という型エラーが吐かれます。

上のようにx.fなどとしてレコードのフィールドが参照されるとき、ocamlのインタープリタはフィールドfの定義の部分にかかれている文言だけを見て、それぞれの型変数が多相型かそうでないかを判断します。

前者の書き方の場合、fの横には「'a. 'a -> 'a」とかかれており、'aという型変数が多相型であるとインタープリタは判断します。一方、後者の場合、フィールドfの横には「'a -> 'a」としか書かれていないので、型変数'aは単相型だと判断されます（'aが多相型であるという情報はfの定義の外の「type 'a tp = …」の部分にあるため、インタープリタはそれを認識しません）。

なので、x.fという式を評価するときに前者では毎回型'aを実体化（instantiate）するため型エラーが発生せず、後者ではそうしないために型エラーが発生します。（instantiateや型推論の話は一応第6回でされると思います）

このように2つのレコードの書き方には違いがあるので注意しましょう。

・で本題ですが、EXISTというmoduleを定義しなさいという問題でした。

・このEXISTは「exist（とある/記号：∃）」に対応するもので、EXIST(struct … end).tは「∃A, T(A)」(あるAが存在して、T(A)が真)という命題に対応する型です。今回の場合、T(A)に対応する型は'a T.tになるはずなので、気持ち的には「∃'a, 'a T.t」のような型を作ればいいことになります。（existential typeという名前があるようです）

・結論から言うと、「∃'A, T(A)」という命題は「∀A, (∀B, T(B)ならばA)ならばA」という命題と同値（未確認）らしく、existential typeは気持ち的には「∀'a. (∀'b. 'b T.t -> 'a) -> 'a」とも書けるはずです。よって、

に注意すると、EXISTモジュールの中のtは、'b uを利用して、 

   1 type t = {t: 'a. 'a u -> 'a}

と書けます。

課題7

   1 (* 扱いたい型(int, string, boolなど)と、その型の値を別の型（この例ではstring型）に変換する関数のペアを'a T.tにする *)
   2 module E = EXIST(struct type 'a t = 'a * ('a -> string) end);;
   3 let pk1 = E.pack ("x", fun x -> x);; (* "x"という文字列をパック *)
   4 let pk2 = E.pack (1, string_of_int);;(* 1という整数をパック *)
   5 [pk1; pk2];; (* pk1, pk2は同じ型(E.t)なのでリストにできる *)
   6 E.unpack pk1 {f = fun (x, f) -> f x};; (* "x"という文字列が返される *)
   7 E.unpack pk2 {f = fun (x, f) -> f x};; (* "1"という文字列が返される *)

Categoryノート

関数・論理型プログラミング実験/課題メモ/第4回 (最終更新日時 2011-05-30 04:02:17 更新者 carbon_twelve)