余冪に対応するプログラムの要素ってどんなの

デカルト閉圏というものがある。これは型付きλ計算や直観主義論理のモデルとなる圏だけども、その特徴は

である。これらをプログラムに対応させると次のようになるだろう。

これらの双対概念は次のようになるけども、

余冪に対応するものがよく分からん。余冪の定義からいうと余冪を X**Y と表現することにすれば

Hom(X**Y, Z)≅Hom(X, Y⊕Z)

が成立すればよい。だから、

IntOrString = IntValue of int | StringValue of string

let f(x:int) : IntOrString = if x &gt;= 2 then IntValue(1) else StringValue("1")

なんて関数があったときに、これを一意的に

let f'(xy:X**Y) : string = "1"

のように書き換えることができればそれは余冪と言えると思えるのだが、そのような書き換えは可能なのか？

とりあえずこの場合に限れば、

exception Y of int

type XToYCopower(x:int) =
    let x' = if x &gt;= 2 then raise(Y(1)) else x

let f'(xy:XToYCopower) = "1"

みたいにして、呼び出すときは、

let mutable z: IntOrString = IntValue(0)
try
    z &lt;- StringValue(f'(XToYCopower(0))) 
with
    | Y(y) -&gt; z &lt;- IntValue(y)

とすると、書き換えができているような気もするし、やはり何か違う気もする。

よく分からんなぁ…。

2015-10-21