ASymmetric Type Unification

/** ASymmetric Type Unification 
 */
module astu; 

型表現（type expression）をXJSONデータにレイフィケーションして、型表現の代理であるXJSONデータの操作により型単一化を行う。ここで扱う型単一 化は非対称（不等式的）であり、単一化の結果は、型（＝集合）の包含関係の真偽または成立条件となる。

別な言い方をすると、非対称単一化により、型（＝集合）の連立不等式系の可解性が判断できる。（包含関係⊆を不等号とみなす。）

実行例：

caty:SysSpecs> [@_var "x", @_boolean true] | astu:do
$x ⊆ true
caty:SysSpecs> [@_string "hello" , @_var "y"] | astu:do
"hello" ⊆ $y
caty:SysSpecs> [@_array [@_string "hello", @_var "x"] , @_array [@_var "y", @_var "z"]] | astu:do
"hello" ⊆ $y
$x ⊆ $z
caty:SysSpecs> [@_array [@_string "hello", @_var "x"] , @_array [@_var "y"]] | astu:do
**CAN NOT**
caty:SysSpecs>

制限と前提

1. インターセクション（&）とマージ（++）は前もって計算されているとする。
2. ユーザー定義型は考えない。前もって展開されているとする。
3. オプション型 A? は (A | undefined) と展開して表現する。ただし、any? は特別にアトミックな型と考える。（any?は順序構造のトップ。anyはトップではなく余アトミックな要素。）
4. タグ付き型のタグは明示的タグだとする。暗黙タグの正規化（消去）は済んでいるとする。
5. スキーマ属性は考えない。
6. integer型は、numberにスキーマ属性が付いたものと解釈するので、考えない。
7. 配列のクリーネスター、オブジェクトのプロパティ名ワイルドカードは考えない。
8. アノテーションと文書コメントは考えない。
9. タグ名ワイルドカードは考えない（リテラルタグのみ）。
10. 再帰的に定義された型は考えない（サイクルの処理が必要）。
11. バッグ型は考えない（等号が異なる）。
12. 型変数は許すが、ユニオン型の選択肢には出現できない。
13. 型変数の意図せぬ捕捉（本来違う変数が偶発的に同じ名前になること）が起きないようにリネームは済んでいるとする。
14. 型変数は、視認性から接頭辞'$'を付けて表示する。
15. オブジェクト型の単一化がイイカゲン。プロパティ名セットを揃える処理をしてないので、事前に手でプロパティ名セットを揃える必要がある。

最後の「手でプロパティ名セットを揃える必要がある」とは、{} と {"a":string?} を単一化するとき、 @_array {} と @_object {"a":@_union ["string", "undefined"]} ではダメで、 @_object {"a":"undefined"} と @_object {"a":@_union ["string", "undefined"]} とする必要があること。 手抜きです。

クリーネスター／ワイルドカード（星印付き型）と再帰は無限構造を導入するが、実用上は無限構造を避けては通れない。無限構造を扱うには、ここで述べるようなやり方（構文駆動方式）が向いているとは限らない。

スキーマ属性を導入すると、「台集合＋論理式」からなる制限型（restricted type）／部分集合型（subset type）が現れる。台の操作と論理計算を組み合わせる必要が出てくる。

/** 型を表現するデータ */
type TypeExpr = (
 BasicType   |
 ProductType |
 UnionType   |
 SpecialType |
 TypeVar     |
);

基本型

undefined型、null型、boolean型、nunmber型、string型、binary型と、すべてのスカラーシングルトン型（リテラル）が基本型。 nullは型名とリテラル表記が同じなので、型名として処理して、シングルトン型からは除く。 undefined型は（後述の）特殊な型に分類するのが適切かもしれない。

基本型は、次のデータで表現される。

1. "undefined"
2. "null"
3. "boolean"
4. "number"
5. "string"
6. "binary"
7. @_boolean true, @_boolean false
8. @_number n （nは任意の数）
9. @_string s （sは任意の文字列）

スカラー基本型を表す名前以外の名前（の文字列）はユーザー定義データ型の名前とみなすが、ここでは扱わない。

type BuiltinType = (
 "undefined"|
 "null"     |
 "boolean"  |
 "number"   |
 "string"   |
 "binary"   |
);

type BooleanSingletonType = @_boolean boolean;
type NumberSingletonType  = @_number  number;
type StringSingletonType  = @_string  string;

type BasicType = (
  BuiltinType | 
  BooleanSingletonType |
  NumberSingletonType  |
  StringSingletonType  |
);

積・複合型

集合の直積（の変種）により構成された型を積・複合型と呼ぶ。配列型、オブジェクト型、タグ付き型がある。

積・複合型は、次のデータで表現される。

/** 配列型 */
type ArrayType = @_array [TypeExpr*];

/** オブジェクト型 */
type ObjectType = @_object {* : TypeExpr?};

/** タグ付き型 */
type TaggedType = @_tagged (@*! TypeExpr);

/** 直積ベースの型 */
type ProductType = (
 ArrayType  |
 ObjectType |
 TaggedType |
);

/** ユニオンを構成する要素的な型 */
type ElementalType = (
  BasicType   |
  ProductType |
);

和・複合型

集合の直和により構成された型を和・複合型と呼ぶ。排他的ユニオン型ともいう。

和・複合型は、次のデータで表現される。

/** ユニオン型 */
type UnionType = @_union [ElementalType, ElementalType, ElementalType*];

特殊な型

any? を独立の型のように扱うことにする。

/** 特殊な型 */
type SpecialType = (
  "never" |
  "any"   |
  "any?"  |
);

型変数

type TypeVar = @_var string;

インスタンスの型への埋め込み

command to-type :: any? -> TypeExpr
{
 when {
 /* 基本型 */
  undefined => "undefined",
  null      => "null",
  boolean   => @_boolean pass,
  number    => @_number pass,
  string    => @_string pass,
 /* 積・複合型 */
  array     => each { call astu:to-type } | @_array pass,
  object    => each --obj { call astu:to-type } | @_object pass,

 /* その他はタグ付き型 */
  *         ==> [tag, (untagged | call astu:to-type)] | tagged | @_tagged pass,
 }
};

文字列化

/** 型表現を文字列化する */
command print :: TypeExpr -> string
{
 case {
  // 基本型と特殊な型
  string            => pass,
  @_boolean boolean => untagged | to-string,
  @_number number   => untagged | to-string,
  @_string string   => untagged | json:pretty, // カンマ忘れてエラーにならない ^^;

  // 積・複合型
  @_array  array    => untagged | each {call astu:print} | text:join ", " | ["[", pass, "]"] | text:concat,
  @_object object   => untagged | call astu:print-object, // 下請けに回す
  @_tagged any      => untagged | ["@", tag, " ", untagged | call astu:print] | text:concat,

  // 和・複合型
  @_union array     => untagged | each {call astu:print} | text:join " | " | ["(", pass, ")"] | text:concat,

  // 型変数
  @_var string      => ["$", untagged] | text:concat,
 }
};

/** オブジェクト型を文字列化する */
command print-object :: {*:TypeExpr?} -> string
{
  each {[%_key, call astu:print]} |
  dump --prefix="print-object" |
  each {[nth 1 | json:pretty, ":", nth 2] | text:concat} |
  text:join ", " | ["{", pass, "}"] | text:concat
};

単一化

• unify
• unify-left-elemental
• unify-both-elemental

type TypePair = [TypeExpr, TypeExpr];

type Result = @True [TypePair*] | @False null | @NG any;


command unify :: [TypeExpr left, TypeExpr right] -> Result
{
 [nth 1 > left, nth 2 > right];

 %left |
 when {
  _var   => 
    @True [ [%left, %right] ],
  _union => 
    each {
      [pass, %right] | dump --prefix="unify (union)" | call astu:unify-left-elemental
    }  | cpl:gather,

  * ==> [pass, %right] | dump --prefix="unify (other)" | call astu:unify-left-elemental,
 }
};

command unify-left-elemental :: [TypeExpr left, TypeExpr right] -> Result
{
 [nth 1 > left, nth 2 > right];

 %right |
 when {
  _var   => 
    @True [ [%left, %right] ],
  _union =>
    each {
     [%left, pass] | call astu:unify-both-elemental
    } | dump --prefix="unify-left-elemental (union)" | cpl:choose,

  * ==> [%left, pass] | call astu:unify-both-elemental,
 }

};

command unify-both-elemental :: [TypeExpr left, TypeExpr right] -> Result
{
 [nth 1 > left, nth 2 > right];

 %left |
 when {
  _array  => pass > left-items;
     %right |
     when {
      _array => [%left-items, pass] | call astu:unify-array-items,
      * => @False null,
     },
  _object  => pass > left-properties;
     %right |
     when {
      _object => [%left-properties, pass] | call astu:unify-object-properties,
      * => @False null,
     },
   _tagged => pass > left-tagged;
     %right |
     when {
      _tagged => [%left-tagged, pass] | call astu:unify-tagged,
      * => @False null,
     },

   // 型変数または複合型以外の型
    *    ==> [pass, %right] | call astu:unify-simple
 }
};

積・複合型の単一化

• unify-array-items
• unify-object-properties
• unify-tagged

command unify-array-items :: [[TypeExpr*] left, [TypeExpr*] right] -> Result
{
 [nth 1 > left, nth 2 > right];

  // 最初に長さを調べる
  [%left | list:length, %right | list:length] | eq |
  when {
   Diff => @False null, // 失敗
   Same => [%left, %right] | list:zip |
           // 配列の項目ごとに単一化
           each { call astu:unify } | cpl:gather,
  }
};

command unify-object-properties :: [{* : TypeExpr?} left, {* : TypeExpr?} right] -> Result
{
 [nth 1 > left, nth 2 > right];
  
  /* プロパティ名セットを揃える操作を入れてない。
   *   **手抜き**
   */

  // 最初にプロパティ名セットを調べる
  [%left | properties | list:sort, %right | properties | list:sort] | eq |
  when {
   Diff => @False null, // 失敗
   Same => [
            %left  | each {pass}, 
            %right | each {pass}
           ] | list:zip | dump --prefix="unify-object-properties" |
           // オブジェクトのプロパティごとに単一化
           each { call astu:unify } | cpl:gather,
  }
};


command unify-tagged :: [(@*! TypeExpr) left, (@*! TypeExpr) right] -> Result
{
 [nth 1 > left, nth 2 > right];

  // 最初にタグ名を調べる
  [%left | tag, %right | tag] | eq |
  when {
   Diff => @False null, // 失敗
   Same => // 次に内容（untagged部）を調べる 
           [%left | untagged,  %right | untagged] | call astu:unify
  }
};

基本的な型と特殊な型の単一化

• unify-simple

command unify-simple :: [TypeExpr left, TypeExpr right] -> Result
{
  dump --prefix="unify-simple" |
  cond {
   ["never",               any] => @True [],
   [any,                "any?"] => @True [],
   ["any",              "any" ] => @True [],
   
   ["undefined",   "undefined"] => @True [],
   ["null",        "null"]      => @True [],
   ["null",        "any" ]      => @True [],
   ["boolean",     "boolean"]   => @True [],
   ["boolean",     "any"    ]   => @True [],
   ["nummer",      "number" ]   => @True [],
   ["nummer",      "any"    ]   => @True [],
   ["string",      "string" ]   => @True [],
   ["string",      "any"    ]   => @True [],
   ["binary",      "binary" ]   => @True [],
   ["binary",      "any"    ]   => @True [],

   [@_boolean boolean, "boolean"] => @True [],
   [@_boolean boolean, "any"    ] => @True [],

   [@_number number, "number"]  => @True [],
   [@_number number, "any"   ]  => @True [],
   [@_number number, @_number number]  => compare-values,

   [@_string string, "string"]  => @True [],
   [@_string string, "any"   ]  => @True [],
   [@_string string, @_string string]  => compare-values,
  
   * => @False null,
 }
};

command compare-values :: [any, any] -> Result
{
  [untagged, untagged] | eq |
  when {
   Same => @Ture [],
   Diff => @False null,
  }
};

単一化の結果の表示

command print-result :: Result -> string
{
 when {
  True => dump --prefix="print-result" |
     each {
       [nth 1 | astu:print, " ⊆ ", nth 2 | astu:print] | text:concat
      } | text:join "\n",
  * => "**CAN NOT**"
 }
};

command do :: [TypeExpr left, TypeExpr right]  -> void
{
  unify | print-result | cout
};

単一化を利用したバリデーションと型等号

command validate :: [any, TypeExpr] -> Result
{
  [nth 1 | to-type , nth 2] | unify
};

command do-val :: [any, TypeExpr]  -> void
{
  validate | print-result | cout
};

/** teq = type equals */
command teq :: [TypeExpr, TypeExpr] -> Result
{
  [nth 1 > left, nth 2 > right];
 
 [
   [%left,  %right] | unify, 
   [%right, %left ] | unify
 ] | cpl:gather
};

command do-teq :: [TypeExpr, TypeExpr]  -> void
{
  teq | print-result | cout
};