Merge pull request #88 from GreasySlug/doc_untranslated

Translate the Japanese documents into English and some text corrections #87

doc/EN/syntax/type/06_nst_vs_sst.md

@@ -0,0 +1,43 @@
+# Nominal Subtyping vs. Structural Subtyping
+
+```erg
+Months = 0..12
+
+# NST
+MonthsClass = Class Months
+MonthsClass.
+    name self =
+        match self:
+            1 -> "january"
+            2 -> "february"
+            3 -> "march"
+            ...
+
+# SST
+MonthsImpl = Patch Months
+MonthsImpl.
+    name self =
+        match self:
+            1 -> "January"
+            2 -> "February"
+            3 -> "March"
+            ...
+
+assert 12 in Months
+assert 2.name() == "February"
+assert not 12 in MonthsClass
+assert MonthsClass.new(12) in MonthsClass
+# It can use structural types, even though wrapped in a class.
+assert MonthsClass.new(12) in Months
+# If both exist, class methods take priority.
+assert MonthsClass.new(2).name() == "february"
+```
+
+## In The End, Which Should I Use, NST or SST?
+
+If you cannot decide which one to use, our recommendation is NST.
+SST requires abstraction skills to write code that does not break down in any use case. Good abstraction can lead to high productivity, but wrong abstraction (commonality by appearances) can lead to counterproductive results. (NSTs can reduce this risk by deliberately keeping abstraction to a minimum. If you are not a library implementor, it is not a bad idea to code only with NSTs.
+
+<p align='center'>
+    <a href='./04_class.md'>Previous</a> | <a href='./06_inheritance.md'>Next</a>
+</p>

doc/EN/syntax/type/09_attributive.md

@@ -0,0 +1,9 @@
+# Attributive Type
+
+Attribute types are types that contain Record and Dataclass, Patch, Module, etc.
+Types belonging to attribute types are not value types.
+
+## Record Type Composite 
+
+It is possible to flatten Record types composited.
+For example, `{... {.name = Str; .age = Nat}; ... {.name = Str; .id = Nat}}` becomes `{.name = Str; .age = Nat; .id = Nat}`.

doc/EN/syntax/type/10_interval.md

@@ -0,0 +1,36 @@
+# Interval Type
+
+The most basic use of `Range` objects is as iterator.
+
+```erg
+for! 0..9, i =>
+    print! i
+```
+
+Note that unlike Python, it includes a end number.
+
+However, this is not only use for the `Range` objects. It can also be used the type. Such a type is called the Interval type.
+
+```erg
+i: 0..10 = 2
+```
+
+The `Nat` type is equivalent to `0..<Inf` and, `Int` and `Ratio` are equivalent to `-Inf<..<Inf`,
+`0..<Inf` can also be written `0.._`. `_` means any instance of `Int` type.
+
+Since it is can also be used as iterator, it can be specified in reverse order, such as `10..0`, however `<..`, `..<` and `<..<` cannot be reversed.
+
+```erg
+a = 0..10 # OK
+b = 0..<10 # OK
+c = 10..0 # OK
+d = 10<..0 # Syntax error
+e = 10..<0 # Syntax error
+f = 10<..<0 # Syntax error
+```
+
+A Range operator can be used for non-numeric types, as long as they are `Ord` immutable types.
+
+```erg
+Alphabet = "A".."z"
+```

doc/EN/syntax/type/11_enum.md

@@ -0,0 +1,85 @@
+# Enumerative Type
+
+Enum types generated by Set.
+Enum types can be used as-is with type specifications, but further methods can be defined by classifying them into classes or defining patches.
+
+A partially typed system with an enumerated type is called an enumerated partially typed.
+
+```erg
+Bool = {True, False}
+Status = {"ok", "error"}
+```
+
+Since `1..7` can be rewritten as `{1, 2, 3, 4, 5, 6, 7}`, so when element is finite, the Enum types essentially equivalent the Range types.
+
+```erg
+Binary! = Class {0, 1}!.
+    invert! ref! self =
+        if! self == 0:
+            do!
+                self.set! 1
+            do!
+                self.set! 0
+
+b = Binary!.new !0
+b.invert!()
+```
+
+Incidentally, Erg's Enum types are a concept that encompasses enumerative types common in other languages.
+
+```rust
+// Rust
+enum Status { Ok, Error }
+```
+
+```erg
+# Erg
+Status = {"Ok", "Error"}
+```
+
+The difference with Rust is that it uses a structural subtype(SST).
+
+```rust
+// There is no relationship between Status and ExtraStatus.
+enum Status { Ok, Error }
+enum ExtraStatus { Ok, Error, Unknown }
+
+// Methods can be implemented
+impl Status {
+    // ...
+}
+impl ExtraStatus {
+    // ...
+}
+```
+
+```erg
+# Status > ExtraStatus, and elements of Status can use methods of ExtraStatus.
+Status = Trait {"Ok", "Error"}
+    # ...
+ExtraStatus = Trait {"Ok", "Error", "Unknown"}
+    # ...
+```
+
+Methods can also be added by patching.
+
+Use the `or` operator to explicitly indicate inclusion or to add a choice to an existing Enum type.
+
+```erg
+ExtraStatus = Status or {"Unknown"}
+```
+
+An enumerated type in which all classes to which an element belongs are identical is called a homogenous enumerated type.
+
+By default, a class whose requirement type is an homogeneous enumerated type can be treated as a subclass of the class to which the element belongs.
+
+If you do not wish to do so, you can make it a wrapper class.
+
+```erg
+Abc = Class {"A", "B", "C"}
+Abc.new("A").is_uppercase()
+
+OpaqueAbc = Class {inner = {"A", "B", "C"}}.
+    new inner: {"A", "B", "C"} = Self.new {inner;}
+OpaqueAbc.new("A").is_uppercase() # TypeError
+```

doc/EN/syntax/type/13_algebraic.md

@@ -0,0 +1,85 @@
+# Algebraic type
+
+Algebraic types are types that are generated by operating types by treating them like algebra.
+Operations handled by them include Union, Intersection, Diff, Complement, and so on.
+Normal classes can only perform Union, and other operations will result in a type error.
+
+## Union
+
+Union types can give multiple possibilities for types. As the name suggests, they are generated by the `or` operator.
+A typical Union is the `Option` type. The `Option` type is a `T or NoneType` patch type, primarily representing values that may fail.
+
+
+```erg
+IntOrStr = Int or Str
+assert dict.get("some key") in (Int or NoneType)
+
+# Implicitly become `T != NoneType`
+Option T = T or NoneType
+```
+
+## Intersection
+
+Intersection types are got by combining types with the `and` operation.
+
+```erg
+Num = Add and Sub and Mul and Eq
+```
+
+As mentioned above, normal classes cannot be combined with the `and` operation. This is because instances belong to only one class.
+
+## Diff
+
+Diff types are got by `not` operation.
+It is better to use `and not` as a closer notation to English text, but it is recommended to use just `not` because it fits better alongside `and` and `or`.
+
+```erg
+CompleteNum = Add and Sub and Mul and Div and Eq and Ord
+Num = CompleteNum not Div not Ord
+
+True = Bool not {False}
+OneTwoThree = {1, 2, 3, 4, 5, 6} - {4, 5, 6, 7, 8, 9, 10}
+```
+
+## Complement
+
+Complement types is got by the `not` operation, which is a unary operation. The `not T` type is a shorthand for `{=} not T`.
+Intersection with type `not T` is equivalent to Diff, and Diff with type `not T` is equivalent to Intersection.
+However, this way of writing is not recommended.
+
+```erg
+# the simplest definition of the non-zero number type
+NonZero = Not {0}
+# deprecated styles
+{True} == Bool and not {False} # 1 == 2 + - 1
+Bool == {True} not not {False} # 2 == 1 - -1
+```
+
+## True Algebraic type
+
+There are two algebraic types: apparent algebraic types that can be simplified and true algebraic types that cannot be further simplified.
+The "apparent algebraic types" include `or` and `and` of Enum, Interval, and the Record types.
+These are not true algebraic types because they are simplified, and using them as type specifiers will result in a Warning; to eliminate the Warning, you must either simplify them or define their types.
+
+```erg
+assert {1, 2, 3} or {2, 3} == {1, 2, 3}
+assert {1, 2, 3} and {2, 3} == {2, 3}
+assert -2..-1 or 1..2 == {-2, -1, 1, 2}
+
+i: {1, 2} or {3, 4} = 1 # TypeWarning: {1, 2} or {3, 4} can be simplified to {1, 2, 3, 4}
+p: {x = Int, ...} and {y = Int; ...} = {x = 1; y = 2; z = 3}
+# TypeWaring: {x = Int, ...} and {y = Int; ...} can be simplified to {x = Int; y = Int; ...}
+
+Point1D = {x = Int; ...}
+Point2D = Point1D and {y = Int; ...} # == {x = Int; y = Int; ...}
+q: Point2D = {x = 1; y = 2; z = 3}
+```
+
+True algebraic types include the types `Or` and `And`. Classes such as `or` between classes are of type `Or`.
+
+```erg
+assert Int or Str == Or(Int, Str)
+assert Int and Marker == And(Int, Marker)
+```
+
+Diff, Complement types are not true algebraic types because they can always be simplified.

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

@@ -1,15 +1,15 @@
 # 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 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.
+The standard form of quantified dependent types are `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.
+Quantified dependent types as left-hand side values can only define methods in the same module as the original type.
 
 ```erg
 K A: Nat = Class ...
@@ -19,7 +19,7 @@ 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 (`||`).
+Quantified dependent types as right-hand side values require that the type variable to be used be declared in the type variable list (`||`).
 
 ```erg
 # T is a concrete type

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

@@ -0,0 +1,72 @@
+# Shared Reference
+
+Shared references are one of those language features that must be handled with care.
+In TypeScript, for example, the following code will pass type checking.
+
+```typescript
+class NormalMember {}
+class VIPMember extends NormalMember {}
+
+let vip_area: VIPMember[] = []
+let normal_area: NormalMember[] = vip_area
+
+normal_area.push(new NormalMember())
+console.log(vip_area) # [NormalMember]
+```
+
+A NormalMember has entered the vip_area. It is an obvious bug, however what went wrong?
+The cause is the shared reference [denatured](./variance.md). The `normal_area` is created by copying the `vip_area`, but in doing so the type has changed.
+But `VIPMember` inherits from `NormalMember`, so `VIPMember[] <: NormalMember[]`, and this is not a problem.
+The relation `VIPMember[] <: NormalMember[]` is fine for immutable objects. However, if you perform a destructive operation like the one above, there will be a breakdown.
+
+In Erg, such code is played back due to the ownership system.
+
+```erg
+NormalMember = Class()
+VIPMember = Class()
+
+vip_area = [].into [VIPMember; !_]
+normal_area: [NormalMember; !_] = vip_area
+
+normal_area.push!(NormalMember.new())
+log vip_area # OwnershipError: `vip_room` was moved to `normal_room`
+```
+
+However, it can be inconvenient for an object to be owned by only one place.
+For this reason, Erg has a type `SharedCell!T!`, which represents a shared state.
+
+```erg
+$p1 = SharedCell!.new(!1)
+$p2 = $p1.mirror!()
+$p3 = SharedCell!.new(!1)
+# If $p1 == $p2, a comparison of the content type Int!
+assert $p1 == $p2
+assert $p1 == $p3
+# Check if $p1 and $p2 point to the same thing with `.addr!`.
+assert $p1.addr!() == $p2.addr!()
+assert $p1.addr!() != $p3.addr!()
+$p1.add! 1
+assert $p1 == 2
+assert $p2 == 2
+assert $p3 == 1
+```
+
+Objects of type `SharedCell!` must be prefixed with `$`. Also, by their nature, they cannot be constants.
+
+The `SharedCell! T!` type is also a subtype of `T!` and can call methods of type `T!`. The only methods specific to the `SharedCell!T!` type are `.addr!`, `.mirror!` and `.try_take`.
+
+An important fact is that `SharedCell! T!` is non-variant, i.e., no inclusions are defined for different type arguments.
+
+```erg
+$vip_area = SharedCell!.new([].into [VIPMember; !_])
+$normal_area: SharedCell!([NormalMember; !_]) = $vip_area.mirror!() # TypeError: expected SharedCell!([NormalMember; !_]), but got SharedCell!([VIPMember; !_])
+# hint: SharedCell!(T) is non-variant, which means it cannot have a supertype or a subtype.
+```
+
+However, the following code have not problem. In the last line, it's the `VIPMember` argument that has been typed converted.
+
+```erg
+$normal_area = SharedCell!.new([].into [NormalMember; !_])
+$normal_area.push!(NormalMember.new()) # OK
+$normal_area.push!(VIPMember.new()) # OK
+```