From b9ff06bb353a81e6dc7e467f14f458617d6711e1 Mon Sep 17 00:00:00 2001
From: Shunsuke Shibayama <sbym1346@gmail.com>
Date: Sun, 26 Mar 2023 01:04:37 +0900
Subject: [PATCH] docs: update compound.md

---
 crates/erg_compiler/lib/std.d/Dict.d.er | 12 ++++++++
 doc/EN/syntax/type/20_compound.md       | 41 +++++++++++++++++--------
 doc/JA/syntax/type/20_compound.md       | 36 +++++++++++++++++-----
 3 files changed, 68 insertions(+), 21 deletions(-)
 create mode 100644 crates/erg_compiler/lib/std.d/Dict.d.er

diff --git a/crates/erg_compiler/lib/std.d/Dict.d.er b/crates/erg_compiler/lib/std.d/Dict.d.er
new file mode 100644
index 00000000..4feea9e6
--- /dev/null
+++ b/crates/erg_compiler/lib/std.d/Dict.d.er
@@ -0,0 +1,12 @@
+.DictItems: ClassType
+.DictKeys: ClassType
+.DictValues: ClassType
+
+.Dict: ClassType
+.Dict.
+    copy: |D <: .Dict|(self: D) -> D
+    fromkeys: |K, V| (iterable: Iterable K, value: V := NoneType) -> .Dict K, V
+    get: |K, V, Default|(self: .Dict(K, V), key: K, default: Default := NoneType) -> V or Default
+    items: |K, V|(self: .Dict(K, V)) -> .DictItems(K, V)
+    keys: |K, V|(self: .Dict(K, V)) -> .DictKeys(K, V)
+    values: |K, V|(self: .Dict(K, V)) -> .DictValues(K, V)
diff --git a/doc/EN/syntax/type/20_compound.md b/doc/EN/syntax/type/20_compound.md
index 81cb7a6b..db871b9a 100644
--- a/doc/EN/syntax/type/20_compound.md
+++ b/doc/EN/syntax/type/20_compound.md
@@ -7,7 +7,7 @@
 (), (X,), (X, Y), (X, Y, Z), ...
 ```
 
-Tuples have a partial type rule for length as well as type inside.
+Tuples have a subtype rule for length as well as type inside.
 For any Tuple `T`, `U`, the following holds.
 
 ```erg
@@ -37,13 +37,13 @@ The same subtype rules exist for arrays as for tuples.
 * forall N in 0..<Len(T) (Len(T) <= Len(U)), U[N] == T[N] => U <: T (oblivion rule)
 ```
 
-Arrays like the one below are not valid types. It is an intentional design to emphasize that the elements of the array are equalized.
+Arrays like the one below are not valid types. It is an intentional design to emphasize that the elements of the array are homogenized.
 
 ```erg
 [Int, Str]
 ```
 
-Because of this, detailed information about each element is lost. To preserve this, a Refinement type is used.
+Because of this, detailed information about each element is lost. To preserve this, refinement types can be used.
 
 ```erg
 a = [1, "a"]: {A: [Int or Str; 2] | A[0] == Int}
@@ -53,12 +53,13 @@ a[0]: Int
 ## Set Type
 
 ```erg
-{}, {X}, ...
+{}, {X; _}, ...
 ```
 
-The Set type itself has no length information. This is because duplicate elements are eliminated in sets, but duplicate elements cannot generally be determined at compile time. In the first place, the length of the information is not very meaningful in a Set.
+Set types have length information, but mostly useless. This is because duplicate elements are eliminated in sets, but duplicate elements cannot generally be determined at compile time.
+In the first place, the length of the information is not very meaningful in a Set.
 
-`{}` is the empty set, a subtype of all types.
+`{}` is the empty set, a subtype of all types. Note that `{X}` is not a set type, but a type that contains only one constant `X`.
 
 ## Dict Type
 
@@ -66,18 +67,17 @@ The Set type itself has no length information. This is because duplicate element
 {:}, {X: Y}, {X: Y, Z: W}, ...
 ```
 
+All dict types are subtypes of `Dict K, V`. `{X: Y} <: Dict X, Y` and `{X: Y, Z: W} <: Dict X or Z, Y or W`.
+
 ## Record Type
 
 ```erg
 {=}, {i = Int}, {i = Int; j = Int}, {.i = Int; .j = Int}, ...
 ```
 
-There is no subtype relationship between private and public type of attribute, however they can be converted to each other by `.Into`.
+A private record type is a super type of a public record type.
 
-```erg
-r = {i = 1}.Into {.i = Int}
-assert r.i == 1
-```
+e.g. `{.i = Int} <: {i = Int}`
 
 ## Function Type
 
@@ -85,14 +85,29 @@ assert r.i == 1
 () -> ()
 Int -> Int
 (Int, Str) -> Bool
+# named parameter
 (x: Int, y: Int) -> Int
+# default parameter
 (x := Int, y := Int) -> Int
-(...objs: Obj) -> Str
+# variable-length parameter
+(*objs: Obj) -> Str
 (Int, Ref Str!) -> Int
+# qualified parameter
 |T: Type|(x: T) -> T
+# qualified parameter with default type
 |T: Type|(x: T := NoneType) -> T # |T: Type|(x: T := X, y: T := Y) -> T (X != Y) is invalid
 ```
 
+## Bound Method Type
+
+```erg
+Int.() -> Int
+Int.(other: Int) -> Int
+# e.g. 1.__add__: Int.(Int) -> Int
+```
+
+The type `C.(T) -> U` is a subtype of `T -> U`. They are almost the same, but ``C.(T) -> U`` is the type of a method whose receiver type is `C`, and the receiver is accessible via an attribute `__self__`.
+
 <p align='center'>
     <a href='./19_bound.md'>Previous</a> | Next
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/JA/syntax/type/20_compound.md b/doc/JA/syntax/type/20_compound.md
index a03e7805..874f22b6 100644
--- a/doc/JA/syntax/type/20_compound.md
+++ b/doc/JA/syntax/type/20_compound.md
@@ -8,6 +8,8 @@
 (), (X,), (X, Y), (X, Y, Z), ...
 ```
 
+上のタプル型は構文糖であり、`(X, Y) == Tuple [X, Y]`である。
+
 タプルには、中の型だけでなく長さについての部分型規則が存在する。
 任意のタプル`T`, `U`について、以下が成り立つ。
 
@@ -31,6 +33,8 @@
 [], [X; 0], [X; 1], [X; 2], ..., [X; _] == [X]
 ```
 
+上の配列型は構文糖であり、`[X; N] == Array X, N`である。
+
 配列に関してもタプルと同様の部分型規則が存在する。
 
 ```erg
@@ -54,12 +58,14 @@ a[0]: Int
 ## セット型
 
 ```erg
-{}, {X}, ...
+{}, {T; _}, ...
 ```
 
-セット型自体は長さの情報を持たない。セットでは要素の重複は排除されるが、重複の判定は一般にコンパイル時には出来ないためである。そもそもセットにおいて長さの情報はあまり意味をなさない。
+上のセット型は構文糖であり、`{T; N} == Set T, N`である。
 
-`{}`は空集合であり、すべての型のサブタイプである。
+セット型は長さの情報を持つが、あまり使われない。セットでは要素の重複は排除されるが、重複の判定は一般にコンパイル時には出来ないためである(そのため、長さは確定できず、多くの場合でパラメータは消去される)。そもそもセットにおいて長さの情報はあまり意味をなさない。
+
+`{}`は空集合であり、すべての型のサブタイプである。`{T}`とすると定数`T`のみを含む型となるので注意。
 
 ## 辞書型
 
@@ -67,17 +73,21 @@ a[0]: Int
 {:}, {X: Y}, {X: Y, Z: W}, ...
 ```
 
+上の形の辞書型はすべて`Dict K, V`のサブタイプである。`Dict K, V`は均質化された辞書型を意味する。
+`{K: V} <: Dict K, V`であり、`{X: Y, Z: W} <: Dict X or Z, Y or W`である。
+
 ## レコード型
 
 ```erg
 {=}, {i = Int}, {i = Int; j = Int}, {.i = Int; .j = Int}, ...
 ```
 
-属性が非公開の型と公開の型の間に部分型関係はないが、`.Into`によって相互に変換可能である。
+上の形のレコード型はすべて`Record`のサブタイプである。
+属性が非公開のレコード型は公開のレコード型のスーパータイプである。
+属性は非公開化できるが、逆はできないということである。
 
 ```erg
-r = {i = 1}.Into {.i = Int}
-assert r.i == 1
+{.i = Int} <: {i = Int}
 ```
 
 ## 関数型
@@ -88,12 +98,22 @@ Int -> Int
 (Int, Str) -> Bool
 (x: Int, y: Int) -> Int
 (x := Int, y := Int) -> Int
-(...objs: Obj) -> Str
+(*objs: Obj) -> Str
 (Int, Ref Str!) -> Int
 |T: Type|(x: T) -> T
 |T: Type|(x: T := NoneType) -> T # |T: Type|(x: T := X, y: T := Y) -> T (X != Y) is invalid
 ```
 
+## バインドされたメソッド型
+
+```erg
+Int.() -> Int
+Int.(other: Int) -> Int
+# e.g. 1.__add__: Int.(Int) -> Int
+```
+
+`C.(T) -> U`の型は`T -> U`のサブタイプである。実際両者はほとんど変わらないが、`C.(T) -> U`は`C`をレシーバ型とするメソッドの型であり、`__self__`という属性からレシーバにアクセスできる。
+
 <p align='center'>
     <a href='./19_bound.md'>Previous</a> | Next
-</p>
\ No newline at end of file
+</p>