RPCのreturn

RPCのcallには、2つの部分デカルト閉構造（評価構造とか適用構造と言ってもいい）が絡むのでけっこう複雑。しかしreturnは簡単。CとDが圏で（C = D でもよい）、F:C→D が関手（あるいは部分関手）とする。別に、埋め込み関手 I:C→D があるとして、return::F⇒I という自然同型となる。

Cがクライアント圏で、Dはサーバー圏を含む十分に大きな圏だとする。Iは大きな圏Dへの埋め込みなので、C⊆D と考えてよい。I(S) = S のようにIを恒等関手のようにみなす。return_S:F(S)→S という同型。F(S)は、クライアントサイドの型Sに対応するサーバーサイドの型。よって、return_S:F(S)→S によりサーバーサイドの戻り値と対応するクライアントサイドの戻り値が１：１に対応するのが保証される。