自然変換としてのzipをCatyScriptで書いてみた

昨日の「zipが自然変換だという話」において、zipの自然性は次の可換図式で表現できると述べました。

PLL(A, B) - zip_(A,B) → LP(A, B)
｜                       ｜
PLL(f, g)               LP(f, g)
↓                       ↓
PLL(C, D) - zip_(C,D) → LP(C, D)

ここで、PLLとLPは、C×C→C という関手です。A, B, C, D は圏Cのすべての対象に渡って動くことになります。また、f:A→C、g:B→D もあらゆる射に対して変化させます。全称記号を使った論理式で書くなら：

• ∀A, B, C, D∈|C|.∀f∈C(A, C), g∈C(B, D). PLL(f, g);zip_C,D = zip_A,B;LP(f, g)

です。写像の等式 h = k は、∀z∈Z. h(z) = k(z) の形なので、それも展開すると：

• ∀A, B, C, D∈|C|.∀f∈C(A, C), g∈C(B, D).∀z∈PLL(A, B). zip_C,D(PLL(f, g)(z)) = LP(f, g)(zip_A,B(z))

エライこと全称記号が続いた論理式になります。「すべての…のすべての…のすべての…の」といった意味なので、1個や2個の事例について確認しても何の意味もありません。とはいえ、1個か2個の事例でも確認してみたいものです。

CatyScriptは明示的な型付けを書くのが割と得意なので、完全に型付けしたzipを書いて、それが自然変換であることを zip-is-natural という述語で表現します。

/** テストサンプル */
command test-sample :: void -> Logical {

 [ [true, false, false, true], [4, 5, 6, 7] ]
 |
 zip-is-natural "to-string" "num:inc"

};

この事例では、4つの対象A, B, C, Dには次のように型（集合）が代入されます。

• A = boolean, B = integer, C = string, D = number

f:A→C は to-string : boolean→string、g:B→D としては num:inc : integer→number（数に1を足す）を使います。実際に試すデータは、PLL(boolean, string) の要素である [ [true, false, false, true], [4, 5, 6, 7] ] です。

caty:test> test-sample
@True [
    [
        [
            "true",
            5
        ],
        [
            "false",
            6
        ],
        [
            "false",
            7
        ],
        [
            "true",
            8
        ]
    ],
    [
        [
            "true",
            5
        ],
        [
            "false",
            6
        ],
        [
            "false",
            7
        ],
        [
            "true",
            8
        ]
    ]
]

自然変換としてのzipの定義はこの下にあります。

/** 射を引数にするためのナンチャッテ定義
 */
type Code<X, Y> = string(remark="X -> Y のコードを表す文字列");

/** リスト関手
 */
type  List<A default any> = [A*];
class List = {
  command fmap<A default any, B default any>
    [Code<A, B> code]
  :: List<A> -> List<B> 
  {
    each {[pass, %1] | eval}
  };
};

/* ペアリング関手
 */
type  Pair<A default any, B default any> = [A, B];
class Pair = {
  command fmap<A default any, B default any, C default any, D default any> 
    [Code<A, C> code1, Code<B, D> code2]
  :: Pair<A, B> ->Pair<C, D> 
  {
    =[
      [pass, %1] | eval, 
      [pass, %2] | eval,
    ]
  };
};

/* PLL = Pair(List(-), List(-)) 関手
 */
type  PLL<A default any, B default any> = Pair<List<A>, List<B>>;
class PLL = {
  command fmap<A default any, B default any, C default any, D default any>
    [Code<A, C> code1, Code<B, D> code2]
  :: PLL<A, B> ->PLL<C, D> 
  {
    =[
      each {[pass, %1] | eval}, 
      each {[pass, %2] | eval},
    ]
  };
};

/* LP = List(Pair(-, -)) 関手
 */
type  LP<A default any, B default any> = List<Pair<A, B>>;
class LP = {
  command fmap<A default any, B default any, C default any, D default any>
    [Code<A, C> code1, Code<B, D> code2]
  :: LP<A, B> ->LP<C, D> 
  {
    each { 
      =[
         [pass, %1] | eval, 
         [pass, %2] | eval,
      ] 
    }
  };
};

/** 自然変換としてのzip
 */
command zip<A default any, B default any> 
:: PLL<A, B> -> LP<A, B>
{
  list:zip
};

/** zipの自然性  
 */
command zip-is-natural<A default any, B default any, C default any, D default any> 
  [Code<A, C> code1, Code<B, D> code2]
:: PLL<A, B> -> Logical 
{
  [
    PLL.fmap<A, B, C, D> %1 %2 | zip<C, D> ,
    zip<A, B> | LP.fmap<A, B, C, D> %1 %2 ,
  ] | eq
};

/** テストサンプル */
command test-sample :: void -> Logical {

 [ [true, false, false, true], [4, 5, 6, 7] ]
 |
 zip-is-natural<boolean, integer, string, number> "to-string" "num:inc"

};