pthread_createに渡してるのってクロージャだったんだ

κeenです。いわれてみれば当たり前なんですが最近気づいたこと pthread_create に渡してるのって要するにクロージャなんですね。

pthread_create は以下のようなシグネチャです。

int pthread_create(pthread_t *thread, const pthread_attr_t *attr,
                          void *(*start_routine) (void *), void *arg);

ここの void *argvoid *(*start_routine) (void *) に引数として渡されます。 void * だと情報量がないですが、要はジェネリクスですよね。ML風に型を付けるとこうなるでしょうか。

val pthread_create: pthread_t * pthread_attr_t * ('a -> ()) * 'a -> int

しかしどちらかというと start_routine が引数に受け取る型を知っていて、それに合わせてデータを渡すので存在型をつけたくなります。 引数内の存在型なのでML多相と同値ですし問題ないでしょう。

exists 'a, ('a -> ()) * 'a

この形、どこかで見覚えがあります。 Closure Conversion as CoYoneda に出てくるクロージャの型とそっくりですね。

\[ A \to B \cong \exists \Gamma.\Gamma \times (\Gamma \times A \to B) \]

よく考えたら高級な言語(クロージャのある言語)だとspawnの引数に渡すクロージャは () -> () なことが多いですね。

実装上の解釈をすると、クロージャは関数とそれが捕捉した環境の組で実装されることが多いです。その関数と環境を2つに分けて引数に渡していると考えれば納得できます。 なるほどー。

Written by κeen