# 部分的型づけそる場

## 前提

Lit と and / or を含む (intersect と union を表す)

S, T = Top | Bottom | T -> T | or (Tn) | and (Tn) | int | num... | 1 | 2 ... | true | false

VS, VT = Top | Bottom | VT -> VT | ... | x (型変数)

における型づけ。

subtyping の計算は型変数を含まない T でのみできるとする

subtyping の計算

or (Tn)

Constraint

VT <: VT

のセットについて解決を試みる。

## 基本的な考えかた

cts : Set [Constraint]

を受け取る

### 1. cts の中身を適切に分解し、最大限 x <: VT または VT <: x という形に帰着させる

基本的な分解操作の一覧
- VS <: and (VTn)
→ n について VS <: VT_n
- or (VSn) <: VT
→ n について VS_n <: VT
- (VS1 -> VS2) <: (VT1 -> VT2)
→ VT1 <: VS1 と VS2 <: VT2

これらを施すと次のような形に帰着する (？)

i. 両辺とも T ← 嬉しい！
ii. 右辺か左辺が x で、もう片方が VT ← わりと嬉しい！
iii. 右辺が or で, 左辺が x でない
- VS <: or (VTn)

iv. 左辺が and で, 右辺が x でない

- and (VSn) <: VT

v. 片方の辺が VT の func type で、もう片方の辺が x でも func でも and/or でもない, したがって下のどれかになる

- VS1 -> VS2 <: int/num... /0/1 ...
- int/num...0/1/... <: VS1 -> VS2
- VS1 -> VS2 <: Top/Bottom
- Top/Bottom <: VS1 -> VS2

### 2. cts 矛盾チェック

i の場合は決定的に subtyping のチェックができる (本当に？)
v の場合も同様

ii の場合の特殊な場合として、 x <: x があげられる。この場合は矛盾を起こさないので OK！ → チェック済みとする

これによって矛盾が起きたら cts は矛盾しているものとしてブランチを棄却
これによってチェックしたものは cts から消す

### 3. 境界の計算と境界条件の伝播

前の作業によって ii, iii, iv の場合のみが残っている

ここで、ii (つまり片方が x のもの) を使って型境界を計算する

下限と上限を全て集めると次のようになる

{下限の型...} <: x <: {上限の型...}

なお、iii, iv および (ii の変数でない方)に x がある可能性が残っているので、この下限、上限を満たせば必ず型解決できるわけではない

※iii, iv の場合はダメなのはわかりやすいが ii の場合は次のようなものがある

x <: number
(1 -> numebr) <: y <: (x -> number)

このセットでは、x ~ 1 なら OK だが x ~ number なら矛盾である

さて、計算した下限 VS_n, VT_n について、次のような Constraint を新たに cts に追加する

or (VS_m) <: and (VT_n) # ここで normalize が効きそう

(なお、すでに追加しているもの、自明に矛盾なものはその限りでない)
また、x に関係する制約を
or (VS_m) <: x と

x <: and (VT_n) のみに統一する。

### 4. 自明な代入と cts の refinement

上限と下限に同じ式が含まれているなら、x に代入する。

1 ~ 4 を変化がなくなるまで繰り返す

### 5. ブランチの分岐 → 分岐できない場合は 7 へ

次のような形の Constraint が残っている

ii. 右辺か左辺が x で、もう片方が VT
iii. 右辺が or で, 左辺が x でない
iv. 左辺が and で, 右辺が x でない

ここで ii を二つに分解して考える

ii(a). 右辺か左辺が x で、もう片方がTop, Bottom, 変数, 1, 2... , num, int,... のような一回の型
ii(b), 右辺か左辺が x で、もう片方がfunction (なお、and / or は iii, iv および分解で排除される)

このうち、iii, iv, ii(b) について、次のように cts を分解する

#### ii(b) の場合

cts を cts1 と cts2 にコピーする

x <: VS -> VT の場合
x は Bottom か関数型である必要がある。
- cts1 では x に Bottom を代入する
- cts2 では新しい変数 y, z に対し x に y -> z を代入する

VS -> VT <: x の場合
x は Top か関数型である必要がある
- cts1 では x に Top を代入する
- cts2 では新しい変数 y, z に対し x に y -> z を代入する

もとの Constraint は削除

#### iii の場合

x <: or (VTn) となっている

n 個の cts を作成し、それぞれ x <: VTn を制約として追加する

もとの Constraint は削除

#### iv の場合

iii と同様

### 6. 分岐した cts の計算

分岐したそれぞれについて solve し、矛盾がないブランチが見つかったなら矛盾なし、すべて矛盾があった場合、矛盾とする

### 7. 矛盾 / 非矛盾の判定

すでに ii(b) しか残っていない。すなわち Top, Bottom, x, lit, prim 間の制約に帰着している。

4 の制約伝播によって、この時点で矛盾がなければ矛盾がないとしてよい (未証明、要検証、または反例求)
　→ ChatGPT はサイクルが無ければ問題ないと言っています！　でも 4 でサイクル消える気がする y <: x <: y となったとき x <= y と代入されるので

## 補遺

### Normalize について

各種 and/or を取る操作において、より単純な形に変換した方が良い結果を生む。次のような変換を行う

VT | Bottom = VT
VT | Top = Top
VT | VT = VT
VT & Bottom = Bottom
VT & Top = VT
VT & VT = VT

T1 | T2 where T1 <: T2 = T2 (subtyping を計算するので、変数を含まない型のみ)
T1 & T2 where T1 <: T2 = T1

分配法則 (or に寄せる) (パフォーマンス悪化の可能性あり？) (逆変換の方が良いか　共通部分見つけるのダルそうだけど)

VT1 & (VT2 | VT3) = (VT1 & VT2) | (VT1 & VT3)

関数化 (関数の分解法則が使える可能性が上がる？)

(VT1 -> VT2) | (VT3 -> VT4) = (VT1 & VT2 -> VT2 | VT4)
(VT1 -> VT2) & (VT3 -> VT4) = (VT1 | VT2 -> VT2 & VT4)

例えば左辺なら | にして右辺なら 関数にする (& も同様) とかいいかも　分解規則をできるだけ使いたい

吸収

VT1 & (VT1 | VT2) = VT1

VT1 | (VT1 & VT2) = VT1

バックエンドは JavaScript で、基本的に

(A -> B) | (C -> D) の意味としては 「A -> B または C -> D という関数型入っている」で、ここに型変換はからまないので、この関数に A & B を適用して C | D を得ることは合法。 逆に (A & B) -> (C | D) も (A -> B) | (C -> D) として見ることが出来る (外延的な等価) JavaScript の instanceof などの使用は制限するのでこれらの型は等しくなる

ブランチングは特殊。 A <: distinguishable なら、branch : A | B -> (A -> C) -> B | C ができる。