Update & removed outdated docs

doc/EN/python/bytecode_instructions.md

@@ -0,0 +1,117 @@
+# Python Bytecode Instructions
+
+Python bytecode variable manipulation instructions are accessed through namei (name index). This is to realize Python's dynamic variable access (access by string using eval, etc.).
+Each instruction is 2 bytes, and instructions and arguments are stored in a little endian.
+Instructions that do not take arguments also use 2 bytes (the argument part is 0).
+
+## STORE_NAME(namei)
+
+```python
+globals[namei] = stack.pop()
+```
+
+## LOAD_NAME(namei)
+
+```python
+stack.push(globals[namei])
+```
+
+Only called at the top level.
+
+## LOAD_GLOBAL(namei)
+
+```python
+stack.push(globals[namei])
+```
+
+To Load what was STORE_NAME at the top level in the inner scope, but namei at the top level is not necessarily the same as namei in a code object of a certain scope (namei, not name, is the same).
+
+## LOAD_CONST(namei)
+
+```python
+stack.push(consts[namei])
+```
+
+Load constants in the constants table.
+Currently (Python 3.9), CPython MAKE_FUNCTION every time a lambda function is called "\<lambda\>".
+
+````console
+>>> dis.dis("[1,2,3].map(lambda x: x+1)")
+1 0 LOAD_CONST 0 (1)
+        2 LOAD_CONST 1 (2)
+        4 LOAD_CONST 2 (3)
+        6 BUILD_LIST 3
+        8 LOAD_ATTR 0 (map)
+        10 LOAD_CONST 3 (<code object <lambda> at 0x7f272897fc90, file "<dis>", line 1>)
+        12 LOAD_CONST 4 ('<lambda>')
+        14 MAKE_FUNCTION 0
+        16 CALL_FUNCTION 1
+        18 RETURN_VALUE
+````
+
+## STORE_FAST(namei)
+
+```python
+fastlocals[namei] = stack.pop()
+```
+
+Probably corresponds to STORE_NAME at the top level.
+This is supposed to store an unreferenced (or single) variable.
+Is it for optimization that the global space has its own instruction?
+
+## LOAD_FAST(namei)
+
+stack.push(fastlocals[namei])
+fastlocals is varnames?
+
+## LOAD_CLOSURE(namei)
+
+```python
+cell = freevars[namei]
+stack.push(cell)
+```
+
+After that BUILD_TUPLE is called.
+It is only called in a closure, and cellvars is supposed to store references in the closure.
+Unlike LOAD_DEREF, the entire cell (container with references) is pushed onto the stack
+
+## STORE_DEREF(namei)
+
+```python
+cell = freevars[namei]
+cell.set(stack.pop())
+```
+
+Variables without references in the inner scope are STORE_FAST, but referenced variables are STORE_DEREF.
+In Python, the reference count is increased or decreased within this instruction
+
+## LOAD_DEREF(namei)
+
+```python
+cell = freevars[namei]
+stack.push(cell.get())
+```
+
+## Name List
+
+### varnames
+
+List of names of internal variables of the function corresponding to `fast_locals`.
+Even if there is a variable with the same name in names, it is not basically the same (it is newly created, and the outside variable cannot be accessed from its scope).
+In other words, variables defined in scope without external references go into varnames
+
+### names
+
+Corresponding to `globals`.
+A list of names of external constants (reference only) used in a scope (even ordinary variables at the top level go into names).
+In other words, constants defined outside the scope go into names
+
+## free variable
+
+Corresponds to `freevars`.
+Variables captured by closure. It behaves static within the same function instance.
+
+## cell variables
+
+Corresponds to `cellvars`.
+Variables captured by an inner closure function within a function. A copy is made, so the original variable remains intact.

doc/EN/python/bytecode_specification.md

@@ -0,0 +1,71 @@
+# Python bytecode specification
+
+## Format
+
+* 0~3 byte(u32): magic number (see common/bytecode.rs for details)
+* 4~7 byte(u32): 0 padding
+* 8~12 byte(u32): timestamp
+* 13~ byte(PyCodeObject): code object
+
+## PyCodeObject
+
+* 0     byte(u8): '0xe3' (prefix, this means code's 'c')
+* 01~04 byte(u32): number of args (co_argcount)
+* 05~08 byte(u32): number of position-only args (co_posonlyargcount)
+* 09~12 byte(u32): number of keyword-only args (co_kwonlyargcount)
+* 13~16 byte(u32): number of locals (co_nlocals)
+* 17~20 byte(u32): stack size (co_stacksize)
+* 21~24 byte(u32): flags (co_flags) ()
+* ?     byte: bytecode instructions, ends with '0x53', '0x0' (83, 0): RETURN_VALUE (co_code)
+* ?     byte(PyTuple): constants used in the code (co_consts)
+* ?     byte(PyTuple): names used in the code (co_names)
+* ?     byte(PyTuple): variable names defined in the code, include params (PyTuple) (co_varnames)
+* ?     byte(PyTuple): variables captured from the outer scope (co_freevars)
+* ?     byte(PyTuple): variables used in the inner closure (co_cellvars)
+* ?     byte(PyUnicode or PyShortAscii): file name, where it was loaded from (co_filename)
+* ?     byte(PyUnicode or PyShortAscii): the name of code itself, default is \<module\> (co_name)
+* ?~?+3 byte(u32): number of first line (co_firstlineno)
+* ?     byte(bytes): line table, represented by PyStringObject? (co_lnotab)
+
+## PyTupleObject
+
+* 0     byte: 0x29 (means ')')
+* 01~04 byte(u32): number of tuple items
+* ?     byte(PyObject): items
+
+## PyStringObject
+
+* If I use a character other than ascii, does it become PyUnicode?
+* "あ", "𠮷", and "α" are PyUnicode (no longer used?)
+
+* 0     byte: 0x73 (means 's')
+* 1~4   byte: length of string
+* 5~    byte: payload
+
+## PyUnicodeObject
+
+* 0     byte: 0x75 (means 'u')
+* 1~4   byte: length of string
+* 5~    byte: payload
+
+## PyShortAsciiObject
+
+* This is called short, but even if there are more than 100 characters, this will still short
+* or rather, there is no ascii that is not short (is short a data type?)
+
+* 0     byte: 0xFA (means 'z')
+* 1~4   byte: length of string
+* 5~    byte: payload
+
+## PyInternedObject
+
+* interned objects are registered in a dedicated map and can be compared with is
+* String, for example, can be compared in constant time regardless of its length
+
+* 0     byte: 0x74 (means 't')
+
+## PyShortAsciiInternedObject
+
+* 0     byte: 0xDA (means 'Z')
+* 1~4   byte: length of string
+* 5~    byte: payload

doc/EN/python/class_system.md

@@ -0,0 +1,94 @@
+# Python class system (compare with Erg)
+
+## Methods
+
+Methods may be forward referenced, but this is not a special technique used.
+This is because the existence of a method is dynamically checked.
+(In Erg, method existence is checked statically. For forward references, functions must be constants.)
+
+```python
+>>> class C:
+...   def f(self, x):
+...       if x == 0: return 0
+...       else: return self.g(x)
+...   def g(self, x): return self.f(x - 1)
+```
+
+## Inheritance, overriding
+
+Some overridden method m is simply overwritten, like a variable reassignment.
+A method that refers to m in the parent class will refer to the overridden m in the child class.
+
+```python
+>>> class C:
+...   def f(self): return 1
+...   def g(self): return self.f()
+...
+>>> class D(C):
+...   def f(self): return 2
+...
+>>>> D().g()
+2
+```
+
+So, even if it is overridden by mistake obviously, it will not be an error until runtime.
+
+```python
+>>>> class C:
+...   def f(self): return 1
+...   def g(self): return self.f() + 1
+...
+>>> class D(C):
+...   def f(self): return "a"
+...
+>>> D().g()
+Traceback (most recent call last):
+  File "<stdin>", line 1, in <module
+  File "<stdin>", line 3, in g
+TypeError: can only concatenate str (not "int") to str
+```
+
+Erg statically checks for consistency with the parent class.
+The `Override` decorator must be given when overriding, and the type of the overriding function must be a subtype of the type of the function being overridden.
+
+```erg
+>>> C = Class()
+...   .f self = 1
+...   .g self = self.f() + 1
+...
+>>> D = Inherit C
+...   .f self = "a"
+...
+Error[#XX]: File "<stdin>", line 5, in D
+To override f, it must be added `Override` decorator and its type must be `Self.() -> Nat` or the subtype of that
+f(self) is already defined in C. To override f, it must be added `Override` decorator and its type must be `Self. To override, it must be given an `Override` decorator and its type must be `Self.() -> Nat` or the subtype of that.f(self).
+```
+
+## Type checking
+
+Type checking is generally all about checking the type of function arguments.
+In Python, most operations are method calls. If the class to which the object belongs does not have a method attached to it at the time of the call, that's it.
+
+```python
+def f(x):
+    return x.m()
+
+class C:
+    def m(self): return None
+
+c = C()
+f(c)
+f(1) # TypeError
+```
+
+```erg
+# f: |T, X <: {.m = Self.() -> T}| X -> T
+f(x) = x.m()
+
+C = Class()
+C.m(self) = None
+
+c = C.new()
+f(c)
+f(1) # TypeError: f takes a type has method `.m` as an argument, but passed Nat
+```

doc/EN/syntax/type/advanced/quiantified_dependent.md

@@ -0,0 +1,27 @@
+# Quantified Dependent Type
+
+Erg has quantified and dependent types. Then, naturally, it is possible to create a type that combines the two. That is the quantified dependent type.
+
+```erg
+NonNullStr = |N: Nat| StrWithLen N | N ! = 0 # same as {S | N: Nat; S: StrWithLen N; N ! = 0}
+NonEmptyArray = |N: Nat| [_; N | N > 0] # same as {A | N: Nat; A: Array(_, N); N > 0}
+```
+
+The standard form of a quantified dependent type is `K(A, ... | Pred)`. ``K`` is a type constructor, `A, B` are type arguments, and `Pred` is a conditional expression.
+
+A quantified dependent type as a left-hand side value can only define methods in the same module as the original type.
+
+```erg
+K A: Nat = Class ...
+K(A).
+    ...
+K(A | A >= 1).
+    method ref! self(A ~> A+1) = ...
+```
+
+A quantified dependent type as a right-hand side value requires that the type variable to be used be declared in the type variable list (`||`).
+
+```erg
+# T is a concrete type
+a: |N: Nat| [T; N | N > 1]
+```

doc/JA/python/bytecode_instructions.md

@@ -6,23 +6,33 @@ Python bytecodeの変数操作系の命令はnamei (name index)を通してア
 
 ## STORE_NAME(namei)
 
+```python
 globals[namei] = stack.pop()
+```
 
 ## LOAD_NAME(namei)
 
+```python
 stack.push(globals[namei])
+```
+
 トップレベルでしか呼び出されない。
 
 ## LOAD_GLOBAL(namei)
 
+```python
 stack.push(globals[namei])
-トップレベルでSTORE_NAMEしたものを内側のスコープでLoadするためのものだが
+```
-トップレベルでのnamei==あるスコープのコードオブジェクトでのnameiとは限らない(nameiではなくnameが同じ)
+
+トップレベルでSTORE_NAMEしたものを内側のスコープでLoadするためのものだが、トップレベルでの`namei`ならばあるスコープのコードオブジェクトでのnameiとも同じとは限らない(nameiではなくnameが同じ)
 
 ## LOAD_CONST(namei)
 
+```python
 stack.push(consts[namei])
-定数テーブルにある定数をロードする
+```
+
+定数テーブルにある定数をロードする。
 現在(Python 3.9)のところ、CPythonではいちいちラムダ関数を"\<lambda\>"という名前でMAKE_FUNCTIONしている
 
 ```console
@@ -53,29 +63,37 @@ fastlocalsはvarnames?
 
 ## LOAD_CLOSURE(namei)
 
+```python
 cell = freevars[namei]
 stack.push(cell)
+```
+
 そのあとBUILD_TUPLEが呼ばれている
 クロージャの中でしか呼び出されないし、cellvarsはクロージャの中での参照を格納するものと思われる
 LOAD_DEREFと違ってcell(参照を詰めたコンテナ)ごとスタックにpushする
 
 ## STORE_DEREF(namei)
 
+```python
 cell = freevars[namei]
 cell.set(stack.pop())
+```
+
 内側のスコープで参照のない変数はSTORE_FASTされるが、参照される変数はSTORE_DEREFされる
 Pythonではこの命令内で参照カウントの増減がされる
 
 ## LOAD_DEREF(namei)
 
+```python
 cell = freevars[namei]
 stack.push(cell.get())
+```
 
 ## 名前リスト
 
 ### varnames
 
-fast_localsに対対応する、関数の内部変数の名前リスト
+fast_localsに対応する、関数の内部変数の名前リスト
 namesで同名の変数があっても、基本的に同じものではない(新しく作られ、そのスコープからは外の変数にアクセスできない)
 つまり、スコープ内で定義された外部参照のない変数はvarnamesに入る
 

doc/JA/python/bytecode_specification.md

@@ -9,7 +9,7 @@
 
 ## PyCodeObject
 
-* 0     byte(u8): '0xe3' (this means code's 'c')
+* 0     byte(u8): '0xe3' (prefix, this means code's 'c')
 * 01~04 byte(u32): number of args (co_argcount)
 * 05~08 byte(u32): number of position-only args (co_posonlyargcount)
 * 09~12 byte(u32): number of keyword-only args (co_kwonlyargcount)
@@ -35,8 +35,8 @@
 
 ## PyStringObject
 
-** ascii以外の文字を使うとPyUnicodeになる？
+* ascii以外の文字を使うとPyUnicodeになる？
-** "あ", "𠮷", "α"だとPyUnicodeになった(もう使われていない？)
+* "あ", "𠮷", "α"だとPyUnicodeになった(もう使われていない？)
 
 * 0     byte: 0x73 (means 's')
 * 1~4   byte: length of string
@@ -50,8 +50,8 @@
 
 ## PyShortAsciiObject
 
-** shortと言っているが、100文字以上あってもこれになる
+* shortと言っているが、100文字以上あってもこれになる
-** というかshortじゃないasciiはない(shortはデータ型？)
+* というかshortじゃないasciiはない(shortはデータ型？)
 
 * 0     byte: 0xFA (means 'z')
 * 1~4   byte: length of string

doc/JA/python/python_vers.txt

@@ -1,6 +0,0 @@
-version   magic number
-3.7.5     3394
-3.8.0     3413
-3.8.5     3413
-3.9.0     3425
-3.9.1     3425

doc/JA/syntax/type/advanced/quantified_dependent.md

@@ -7,20 +7,21 @@ NonNullStr = |N: Nat| StrWithLen N | N != 0 # same as {S | N: Nat; S: StrWithLen
 NonEmptyArray = |N: Nat| [_; N | N > 0] # same as {A | N: Nat; A: Array(_, N); N > 0}
 ```
 
-量化依存型の標準形は`T(A, ... | Pred)`です。`T`は型構築子、`A, B`は型引数、`Pred`は条件式です。
+量化依存型の標準形は`K(A, ... | Pred)`です。`K`は型構築子、`A, B`は型引数、`Pred`は条件式です。
 
 左辺値としての量化依存型は、元の型と同じモジュール内でのみメソッドを定義出来ます。
 
 ```erg
-T A: Nat = Class ...
+K A: Nat = Class ...
-T(A).
+K(A).
     ...
-T(A | A >= 1).
+K(A | A >= 1).
     method ref! self(A ~> A+1) = ...
 ```
 
 右辺値としての量化依存型は、使用する型変数を型変数リスト(`||`)で宣言する必要がある。
 
 ```erg
+# Tは具体的な型
 a: |N: Nat| [T; N | N > 1]
 ```

doc/JA/syntax/type/advanced/rank2type.md

@@ -1,25 +0,0 @@
-# ランク2型
-
-Ergでは`id|T|(x: T) -> T = x`などのように色々な型を受け取れる関数、すなわち多相関数を定義できる。
-では、多相関数を受け取れる関数は定義できるだろうか？
-例えば、このような関数である(この定義は誤りを含むことに注意してほしい)。
-
-```erg
-# pair_map(i -> i * 2, (1, "a")) == (2, "aa")になってほしい
-pair_map|T, L, R|(f: T -> T, (l: L, r: R)) -> (L, R) = (f(l), f(r))
-```
-
-`1`と`"a"`の型が違うので、無名関数は一度単相化して終わりではないことに注意してほしい。2回単相化する必要がある。
-しかしはErgは型変数を一度しか単相化しない。すなわち、`T -> T`は`f(tup.0)`の時点で`Int -> Int`に決定されてしまう。
-
-```erg
-# pair_map: |L, R: Type; F <: L -> L; F <: R -> R|(F, (L, R)) -> (L, R)
-pair_map|L, R|(f, (l: L, r: R)): (L, R) = (f(l), f(r))
-```
-
-何も指定しなかった場合はこうなる。
-
-```erg
-# pair_map: |F, T, U, V, W: Type; F <: T -> V; F <: U -> W| (F, (T, U)) -> (V, W)
-pair_map(f, (l, r)) = (f(l), f(r))
-```

doc/JA/syntax/type/advanced/recursive_type_inferring.md

@@ -1,50 +0,0 @@
-# 再帰型の型推論
-
-再帰型の型推論では、任意回の呼び出しで生成されるオブジェクトの集合を計算することとなる。
-これは実質的には無限回の操作で生成される空間と同義である。
-`fn T`をサブルーチン`fn`に対する`T`型オブジェクトの適用による戻り値型とするとき、関数呼び出しをn回行って導出される型をfn^n Tと表す。つまり、fn(fn(...(fn(T)))) == fn^n Tである。
-複数引数の場合、前の呼び出しの結果が第1引数となる場合、つまりfn(fn(fn(fn(x, y_1)..., y_n-2) y_n-1) y_n)はfn^n X Y^nと表す。
-同様に、前の呼び出しの結果が第2引数となる場合、つまりfn(x_1 fn(x_2 ...fn(x_n y)))はfn^n X^n Yまたは(fn X)^n Yと表す。
-例としては階乗関数`fact n: Nat = n * fact n-1`がある。`fact: 1.. * fact (1.. - {1}) == (1.. *)^n {1}`である。
-
-再帰型ではいくらでも呼び出しうるため、関数の戻り値に使われている関数fnの無眼回適用で生成されるfn^∞ Tが戻り値型である。
-現在実装されている推論規則は以下の通り。
-
-指定のない限り、x, y, z: Nat
-
-* id^∞ t == {t}
-* ({0} +)^∞ x..y == x..y
-* ({0} -)^∞ x..y = -y..-x
-* ({1} *)^∞ x..y == x..y
-* ({z} +)^∞ x..y == Nat
-* ({z} -)^∞ x..y = Int
-* ({""} +)^∞ {s} == {s}
-* ({s = Str len = 1..} +)^∞ {\_ = Str} == Str
-
-## 非依存化
-
-Independizationは依存型を一般の型に戻す操作である。例として、{1} -> Natなどがある。
-普通のダウンキャストの場合は、{1} -> {0, 1} -> {0, 1, 2}などとなる場合がある。これはその名前空間で定義のある依存型による。
-依存型は無限にあるため、定義のあるものにしかダウンキャストしないのである。
-しかしIndependizationは一意的である。
-非依存化は依存型の推論が失敗した場合に行われる。
-{1, True}など、別々のクラスに属するオブジェクト同士の非依存化は失敗(コンパイルエラー)する。
-{-1, 0, 1}など同一のクラスであれば成功する。その際、クラスは可能な限り子クラスになる(この場合はInt)。
-型変数を含んだ型、例えば{True} or '0は、型変数を含まない方が非依存化されたあと消去される(この場合はBool)。
-もともとErgのランタイムにはクラスしか存在しないので、この操作は型消去の一種であり、情報は失われるが健全性が壊れることはない(TODO:証明を与える)。
-
-## 依存推論のテスト
-
-```erg
-func 0, 0, _ = True
-func 0, _, _ = False
-func(i, x, a) =
-    # a[i-1] を選ばない場合 (func(i-1, x, a) が OK なら OK)
-    if func(i-1, x, a):
-        return True
-    # a[i-1] を選ぶ場合 (func(i-1, x-a[i-1], a) が OK なら OK)
-    if func(i-1, x-a[i-1], a):
-        return True
-
-    False
-```

doc/JA/syntax/type/advanced/type_inferring.md

@@ -1,164 +0,0 @@
-# 型推論
-
-> __Warning__： この文書の情報は古く、一部に間違いを含みます。
-
-Ergでは多くの場合引数の型を省略することが可能である。
-内部的には、省略された引数は型変数で型付けされる。つまり、なんでも受け入れる型である。
-そこから、関数内部での使われ方に応じて最小の型制約が課される。
-多くの場合、型推論によってシグネチャから型変数がすべて除去されることはない。
-例えば、`x + 1`と書かれていたとき、`x`は`'0`型で、その制約は'0 <: `+`({1}, '1)である。
-ほかの言語、例えばOCamlではこの時点でxはIntと決定されてしまうが、ErgではNat, Int, Float, ...あるいはユーザー定義のクラス・型などが入る可能性もある。よって、この定義の時点では単に'0と置くだけで、戻り値型の推論は使用時に行われる。
-Ergでは再帰関数の定義も可能であるが、現在のところ、技術的な理由で再帰関数の戻り値は推論されない。推論が不可能な場合が多いからである。
-
-```erg
-fib 0 = 0
-fib 1 = 1
-fib n: Nat = fib(n-1) + fib(n-2)
-```
-
-上記の`fib`の定義は、
-
-```erg
-fib n: Nat =
-    match x:
-        0 -> 0
-        1 -> 1
-        n -> fib(n-1) + fib(n-2)
-```
-
-と同じである。
-
-## 型推論の例
-
-```erg
-fib 0 = 0
-fib 1 = 1
-fib n: Nat = fib(n-1) + fib(n-2)
-
-# 相互再帰関数も定義可能
-even 0 = True
-even n: 1.. = odd n-1
-odd 0 = False
-odd n: 1.. = even n-1
-
-sig _: Neg = -1
-sig 0 = 0
-sig _: Pos = 1
-
-f 1 = 0
-f 2 = 1
-f(x): Nat = f x*2
-```
-
-これらの関数の推論は以下のように行われる。
-ただし、以下の記法を使用する。
-
-* `f x: T`なる関数があったとき、`f`の戻り値の型を`f T`と表す。すなわち、`f: T -> U`のとき`U = f T`である。
-* `∴`は「故に」「よって」を表す。
-* minはその型を実現する最小の単相型を表す。
-  `'T`に制約がないとき、`min('T) = Never`
-  `T`が単相型のとき、`min(T) = T`
-
-## fib
-
-* fib 0とfib 1に関しては直接型付け可能。
-  fib: {0} -> {0}
-  fib: {1} -> {1}
-  fib: {0, 1} -> {0, 1} (この関数は宣言だけ登録され、実体は使用されるまで生成されない。実体はmatchによって生成される)
-* fib: 2.. -> '0 | '0 <: min(fib 2.. - {1} + fib 2.. - {2})
-  fib: 2.. -> '0 | '0 <: min(fib 1.. + fib 0..)
-* fib: 1.. -> '1とfib 0.. -> '2の型推論を行う(実際は新しい名前空間で推論するので'1, '2にインクリメントする必要はないが、見やすさのためにこうしている)
-  * fib: 1.. -> '1について、既に存在する宣言から順に決め打ちする
-    * fib {1} -> {1}が見つかったので、1..から{1}を抜く->2..
-    * fib 2.. -> '0が見つかったので、2..から2..を抜く->Never
-    * Neverになったので完成、fib: 1.. -> {1} or '0
-  * fib: 0.. -> '2についても同様にしてfib: 0.. -> {0, 1} or '0
-* fib: 2.. -> '0 | '0 <: min(({1} or '0) + ({0, 1} or '0))
-  再帰型の推論では「任意回の操作によって得られる型(see erg_type_inferring_recursive.md)」を計算する
-  つまり、'0は{1}と{0, 1}の任意回の加算によって生成される型である
-  {0}+{0}以外の正数集合の任意回可算はNatを生成する
-* 合計で宣言されたのは
-  fib: {0} -> {0}
-  fib: {1} -> {1}
-  fib: {0, 1} -> {0, 1}
-  fib: 2.. -> Nat
-  fib: {0} or 2.. -> Nat
-  fib: 1.. -> Nat
-  fib: Nat -> Nat
-  の7種類。
-
-## even, odd
-
-* even 0とodd 0に関しては直接型付け可能。
-  even.{0} \_ = True
-  odd.{0} \_ = False
-* even nとodd nの戻り値型を'0, '1としておく。
-  even: 1.. -> '0 | '0 <: odd 1.. - 1
-  ∴ even: 1.. -> '0 | '0 <: odd 0..
-    odd 0..:
-      odd {0} -> {False}
-      odd 1.. -> '1
-  ∴ even: 1.. -> '0 | '0 <: {False} or '1
-  odd: 1.. -> '1 | '1 <: even 1.. -1
-  ∴ odd: 1.. -> '1 | '1 <: even 0..
-    even 0..:
-      even {0} -> {True}
-      even 1.. -> '0 | '0 <: {False} or '1
-  odd:  1.. -> '1 | '1 <: {True, False} or '1
-  odd: 1.. -> {True, False}
-  even: 1.. -> {True, False}
-* 合計で宣言されたのは
-  even: {0} -> {True}
-  odd: {0} -> {False}
-  odd: 1.. -> Bool
-  even: 1.. -> Bool
-  even: Nat -> Bool
-  odd: Nat -> Bool
-
-## sig
-
-* sig _: ..=-1 = -1より
-  sig.(..0) \_ = -1
-  が定義される。一意性のため、x: Natのとき..=xは..x+1に置換される(Floatでは置換できない)。
-* sig 0 = 0より内部で
-  sig.{0} \_ = 0
-  sig.(..0) \_0 =
-      match _0:
-        _1: ..0 -> sig.(..0) _1
-        _1: {0} -> sig.{0} _1
-  が定義される。
-* sig: _: 1.. = 1より
-  sig.(1..) \_ = 1
-  (..=-1 or 1..) <.> NZInt
-  sig.NZInt \_0 =
-      match \_0:
-        _1: ..0 -> sig.(..0) _1
-        _1: 1.. -> sig.(1..) _1
-  (..=-1 or 0 or 1..) <.> Int
-  sig.Int \_0 =
-      match \_0:
-        _1: ..0 -> sig.(..0) _1
-        _1: {0} -> sig.{0} _1
-        _1: 1.. -> sig.(1..) _1
-  が定義される。
-
-## f
-
-* まず宣言されるのは以下の通り。
-  f: {1} -> {0}
-  f: {2} -> {1}
-  f: {1, 2} -> {0, 1}
-  f: {"a"} -> {2}
-  f: {1, "a"} -> {0, 2}
-  f: {2, "a"} -> {1, 2}
-  f: {1, 2, "a"} -> {0, 1, 2}
-* f: '0 -> '1 | '1 <: f '0 * {2}, Mul('0, {2}, '2)
-* '2を決め打つ
-  * '2 <: {1}とすると、Mul '0, {2}, {1}より'0 <: {0.5}
-    f: {0.5} -> {0}
-  * '2 <: {2}とすると、Mul '0, {2}, {2}より'0 <: {1}
-    f: {1} -> {1}だが、これはf: {1} -> {0}に矛盾、型エラー
-  * '2 <: {"a"}とすると、Mul '0, {2}, {"a"}を満たす解は存在しない
-  * '2を型変数のままにする('2 != {1, 2, "a"})と、'2 <: '0
-    f: '0 -> '1 | Mul('0, {2}, '0)
-    '1の制約がないので、推論不能

doc/JA/syntax/type/advanced/type_inferring_v2.md

@@ -1,149 +0,0 @@
-# 型推論
-
-> __Warning__: この項の情報は古く、一部に間違いを含みます。
-
-Ergでは多くの場合サブルーチンの引数の型、および戻り値型を省略できる。
-この項では、その推論アルゴリズムと、推論ができない場合について解説する。
-
-以下に示す`id`関数は最もシンプルな多相型関数である。
-
-```erg
-id x = x
-```
-
-xの型は特に指定されていないが、これは以下のコードと同じである。
-
-```erg
-id: |T| T -> T
-id x = x
-```
-
-実際、型指定の省略されている部分は、内部的には`id: |'1, '2| '1 -> '2`と一旦型変数が割り当てられる
-(仮に割り振られた型変数は`'数字`で表現することとする)。
-そして、ブロック内での`x`の使われ方によって`'2`の型が決定される。
-この場合はそのまま返しているので、`'2`型は`'1`型に単一化される。
-
-次に、単相サブルーチンを使用しているサブルーチンの推論を見る。
-
-```erg
-p! x = x.times! do! print! x
-```
-
-```erg
-p!: '1 => '2
-print!: ...Object => NoneType
-do!: () => NoneType
-.times!: Nat.(() => NoneType) => NoneType
-'1 := Nat, '2 := NoneType
-```
-
-中で使用している`.times!`の戻り値型が単相(一つの種類の型しか受け付けない)なので、`p!`も単相である。
-もう少し複雑な例を見る。今度は多相サブルーチンを含むサブルーチンの型推論である。
-
-```erg
-f x, y, z = x + y + z
-```
-
-まず、このように型が割り当てられる。
-
-```erg
-f: ('1, '2, '3) -> '4
-f x, y, z = x + y + z
-```
-
-`x + y`について、この型は`+`('1, '2)である。フィットするものを`+`の実装及び宣言から探索する。
-グローバル空間には``+`: ('L, 'R) -> 'O`という宣言が存在する。この場合これがフィットする。
-では`+`('1, '2)の型は何だろうか。単純に'Oとしてはいけない。なぜなら、(x + y) + zの型、
-すなわち`+`(`+`('1, '2), '3)もフィットするため、x+yとx+y+zの型が同一になってしまう。
-なので、この場合は新しい型変数を割り当てる。
-具体的には、型変数を単一化せずに使う場合、戻り値型は新しく発行する。
-この場合、`+`('1, '2) == '5とする。
-`+`(`+`('1, '2), '3)についても同様に、`+`(`+`('1, '2), '3) == '6である。
-最終的な戻り値の'6は'4に単一化する。
-最後に型境界の処理を行う。'4型がどのような条件で与えられる型なのか明示する必要があるのである。
-結論から言うと以下のようになる。
-
-```erg
-f: |'1 <: {`+` = Self.'2 -> '5}, '5 <: {`+` = Self.'3 -> '4}| ('1, '2, '3) -> '4
-f x, y, z = x + y + z
-```
-
-この型境界により'4の型が決定される。
-このように見ると全てのサブルーチンが型推論可能なように思えるかもしれないが、残念ながらそうはいかない。
-推論ができない例としては、再帰関数がある。
-
-```erg
-fib 0 = 0
-fib 1 = 1
-fib n = fib(n-1) + fib(n-2)
-```
-
-先ほどと同じようにすると、型境界は以下のようになる。
-
-```erg
-fib: |
-    '1: -{0, 1}
-    '1 <: {`-` = ('Self, {1}) -> '3}
-    '1 <: {`-` = ('Self, {2}) -> '4}
-    '5 == <fib> '3,
-    '6 == <fib> '4,
-    '5 <: {`+` = (Self, '6) -> '2}
-| '1 -> '2
-fib n = fib(n-1) + fib(n-2)
-```
-
-試しにNatを代入してみる。
-
-```erg
-fib: |
-    {`-` = (Nat-{0, 1}, {1}) -> 1.._}
-    {`-` = (Nat-{0, 1}, {2}) -> 0.._}
-    {fib = {1} -> {1}}
-    {fib = {0} -> {0}}
-    {fib = 1.._ -> ?}
-    {fib = 0.._ -> ?}
-    {`+` = ?, ? -> ?}
-| Nat -> ?
-```
-
-```erg
-fib: |
-    {`-` = (1.._).{1} -> 0.._}
-    {`-` = (1.._).{2} -> -1.._}
-    {fib = 0.._ -> ?} # fib Natに戻ってしまう!
-    {fib = -1.._ -> ?}
-    {`+` = ?.? -> ?}
-| 1.._ -> ?
-```
-
-こういうわけで、型推論が無限ループしてしまう。
-よって、再帰関数は戻り値の指定が必須である(Haskell等の言語ではリテラルから型を推論するが、Ergは依存型を持つのでリテラルの型が一意に決まらない)。
-これは相互再帰関数の場合もだが、どれか一つを型指定するだけでよい。
-
-```erg
-odd 0 = False
-odd(n): Bool = even n-1
-even 0 = True
-even n = odd n-1
-```
-
-```erg
-odd:|
-    '1 <: Not {0}
-    {`-` = '1, {1} -> '2}
-    {even = '2 -> Bool} # 推論ではなく強制
-| '1 -> Bool
-odd n = even n-1
-
-even: |
-    '1 <: Not {0}
-    {`-` = '1, {1} -> '2}
-    {odd = '2 -> Bool}
-| '1 -> Bool
-even n = odd n-1
-```
-
-しかし、この型付けには問題がある。減算が定義されている数なら何でも受け付けてしまうのである。
-つまり、`odd -1`が型検査を通ってしまう。これは明らかにナンセンスで、永遠に計算結果は現れない。
-この場合は`odd(n: Nat): Bool = even n-1`と、引数の型も明示しておくべきである。
-こうすれば`even`の方もナンセンスな引数は受け付けない。

doc/JA/syntax/type/advanced/widening.md

@@ -53,15 +53,15 @@ ids<Int or Str or NoneType>(i, j) # OK
 
 `A and B`は以下の可能性がある。
 
-* `A and B == A`: `A < B`または`A == B`のとき。
+* `A and B == A`: `A <: B`または`A == B`のとき。
-* `A and B == B`: `A > B`または`A == B`のとき。
+* `A and B == B`: `A :> B`または`A == B`のとき。
-* `A and B == {}`: `A != B`のとき。
+* `A and B == {}`: `!(A :> B)`かつ`!(A <: B)`のとき。
 
 `A or B`は以下の可能性がある。
 
-* `A or B == A`: `A > B`または`A == B`のとき。
+* `A or B == A`: `A :> B`または`A == B`のとき。
-* `A or B == B`: `A < B`または`A == B`のとき。
+* `A or B == B`: `A <: B`または`A == B`のとき。
-* `A or B`は簡約不能(独立した型): `A != B`のとき。
+* `A or B`は簡約不能(独立した型): `!(A :> B)`かつ`!(A <: B)`のとき。
 
 ## サブルーチン定義での型拡大