einblickerの日記

make installしたConCaTが動かない

Coq | 19:36 |

ConCaT

こいつをmakeしてmake installした後coqtop上で

Require Import Category.

とかしたらlibraryが見つからない的なエラーが出る…。

でもmakeした後に手動でConCaTフォルダごと/usr/lib/coq/user-contrib/に移したらちゃんと動いた。make installだとvoファイルだけを直に/usr/lib/coq/user-contrib/へコピーしてしまうのがどうもダメっぽい。

「圏論の基礎」ポチッた

Book | 19:34 |

The Haskell Programmer’s Guide to the IO Monad --- Don’t Panic

↑これが結構面白かったのでもっと勉強したいと思いこの本を買った。

圏論による論理学―高階論理とトポス

ざっと目を通してみるとfunctorとかnatural transformationとかの重要っぽい概念は説明されているんだけどmonadは扱われていなかった。圏論的にはmonadって脇役っぽい感じなんでしょうね多分。高階論理との関連部分は興味無くて殆ど飛ばし読みした。

んでmonadをもっと知りたいので遂にはマックレーンさんの本をポチッてしまった…。

圏論の基礎

多分読み通せずに挫折するんでしょうが。

delegateリテラルが非定数式扱いで泣いた

D | 19:33 |

D言語でdelegateリテラルとtemplate使ってanaphoric ifを再現しようとしたら動かなくて泣いた。

import std.stdio;

template AIF(string cond, string then, string els = "")
{
  mixin("auto AIF = { auto it = " ~ cond ~ "; if (it) { " ~ then ~ "} else {" ~ els ~ "} };");
}

void main()
{
  int x = 3;
  AIF!(q{ 1 + x }, q{ writeln(it); })();
}

delegateリテラルが非定数式なので駄目らしい。まぁ仮に動いたとしてもAIF内部で普通のif文のようにreturnが使えないので微妙ではあるんだけれど。

ちなみにdelegateリテラルの代わりにfunctionリテラルでやってみても非定数式扱いになって駄目だった。delegateリテラルはともかくfunctionリテラルはクロージャにならないんだから定数扱いでいいんじゃないかと思うんだけどどうなんでしょうね。

関数を定義するようにしたら今度は外側の変数にアクセス出来ないので困る。

import std.stdio;

template AIF(string cond, string then, string els = "")
{
  mixin("void AIF(){ auto it = " ~ cond ~ "; if (it) { " ~ then ~ "} else {" ~ els ~ "} }");
}

void main()
{
  int x = 3;
  AIF!(q{ 1 + x }, q{ writeln(it); })(); //xにアクセス出来ないのでエラー
}

呼び出し側でmixinを書けばやりたいことはできる。

import std.stdio;

pure string aif(string cond, string then, string els = "")
{
  return "{ auto it = " ~ cond ~ "; if (it) { " ~ then ~ "} else {" ~ els ~ "} }";
}

void main()
{
  int x = 3;
  mixin(aif(q{ 1 + x }, q{ writeln(it); }));
}

でもaifが文字列返すだけってのはなんだか美しくない感じ。

そういえばD言語には「macro」という予約語（まだ使われてないっぽい）があるんだけど、これはそのうちマクロが導入されるってことなんだろうか…？