Merge pull request gluon-lang#109 from Marwes/explain_typesystem

[WIP] docs: Add more explanations about the type system

TUTORIAL.md

@@ -224,51 +224,6 @@ and SExpr = { location: Int, expr: SExpr_ }
 in Atom "name"
 ```
 
-### Types
-
-#### Function types
-
-```
-<type> -> <type>
-```
-
-Function types are written using the `->` operator which is right associative. This means that the type of `(+)` which is usually written as `Int -> Int -> Int` is parsed as `Int -> (Int -> Int)` (A function taking one argument of `Int` and returning a function of `Int -> Int`).
-
-#### Record type
-
-```
-{ (<identifier> : <type>)* }
-{ pi: Float, sin: Float -> Float }
-```
-
-Records are gluon's main way of creating associating related data and they should look quite familiar if you are familiar with dynamic languages such as javascript. Looks can be deceiving however as gluon's records can neither add more fields or change the values of existing fields.
-
-#### Enumeration type
-
-```
-( | <identifier> (<type>)* )*
-
-| Err e | Ok t
-```
-
-Gluon also has a second way of grouping data which is the enumeration type which allows you to represent a value being one of several variants. In the example above is the representation of gluons standard `Result` type which represents either the value having been successfully computed (`Ok t`) or that an error occurred (`Err e`).
-
-#### Alias type
-
-```
-<identifier> (<type>)*
-Int
-Float
-Option Int
-Ref String
-```
-
-The last kind of type which gluon has is the alias type. An alias type is a type which explicitly names some underlying type which can either be one of the three types mentioned above or an abstract type which is the case for the `Int`, `String` and `Ref` types. If the underlying type is abstract then the type is only considered equivalent to its own alias (ie if you define an abstract type of `MyInt` which has the same representation as `Int` the typechecker still considers these two types as being not equal to each other).
-
-#### Higher-kinded types (TODO)
-
-Gluon has higher kinded types.
-
 ### Indentation
 
 If you have been following along this far you may be thinking think that the syntax so far is pretty limiting. In particular you wouldn't be wrong in thinking that the `let` and `type` syntax are clunky due to their need to be closed by the `in` keyword. Luckily gluon offers a more convenient way of writing bindings by relying on indentation.
@@ -313,6 +268,78 @@ in
 module.id module.pi
 ```
 
+## Typesystem
+
+### Function types
+
+```
+<type> -> <type>
+```
+
+Function types are written using the `(->)` operator which is right associative. This means that the function type `Int -> (Int -> Int)` (A function taking one argument of Int and returning a function of `Int -> Int`) can be written as `Int -> Int -> Int`.
+
+### Record type
+
+```
+{ (<identifier> <identifier>* = <type>,)* (<identifier> : <type>,)* }
+{ pi : Float, sin : Float -> Float }
+```
+
+Records are gluon's main way of creating associating related data and they should look quite familiar if you are familiar with dynamic languages such as javascript. Looks can be deceiving however as gluon's records are more similar to a struct in Rust or C as the order of the fields are significant, `{ x : Int, y : String } != { y : String, x : Int }`. Furthermore records are immutable meaning fields cannot be added or removed and the values within cannot be modified.
+
+In addition to storing values, records also have a secondary function of storing types which is gluon's way of exporting types. If you have used modules in an ML language this may look rather familiar, looks can be deceiving however as 'type fields' must match exactly in gluon which means there is no subtyping relationship between records (`{ Test = { x : Int } }` is not a subtype of `{ Test = Float }`). This may change in the future.
+
+```f#
+{ Test = { x : Int } }
+```
+
+### Enumeration type
+
+```
+( | <identifier> (<type>)* )*
+
+| Err e | Ok t
+```
+
+Gluon also has a second way of grouping data which is the enumeration type which allows you to represent a value being one of several variants. In the example above is the representation of gluon's standard `Result` type which represents either the value having been successfully computed (`Ok t`) or that an error occurred (`Err e`).
+
+### Alias type
+
+```
+<identifier> (<type>)*
+Int
+Float
+Option Int
+Ref String
+```
+
+The last kind of type which gluon has is the alias type. An alias type is a type which explicitly names some underlying type which can either be one of the three types mentioned above or an abstract type which is the case for the `Int`, `String` and `Ref` types. If the underlying type is abstract then the type is only considered equivalent to itself (ie if you define an abstract type of `MyInt` which happens to have the same representation as `Int` the typechecker will consider these two types as being distinct).
+
+### Higher-kinded types
+
+Higher-kinded types are a fairly abstract concept in gluon and you may very well create entire programs without any knowledge about them. Sometimes they are a very valuable tool to have as they can be used to create very powerful abstractions.
+
+Just as all values such as `0 : Int`, `"Hello World!" : String` and `Some 4.0 : Option Float` each have a type these types themselves have their own 'type' or the 'kind' as it is called. For the types of concrete values the `Kind` is always `Type` so for the earlier examples `Int : Type`, `String : Type` and `Option Float : Type`. That is not very useful on its own but it becomes more interesting when we consider the kind of `Option : Type -> Type`. `Type -> Type` looks rather like the type of a functions such as `show_int : Int -> String` but instead of taking a value it takes a type and produces a new type. In effect this lets us abstract over types instead of just over values. This abstraction facility can be seen in the `Functor : (Type -> Type) -> Type` type which takes a type with kind `Type -> Type` as argument which is exactly the kind of `Option` (or `List`, `Result a`).
+
+### Overloading
+
+Sometimes there there is a need to overload a name with multiple differing implementations and let the compiler chose the correct implementation. If you have written any amount of Gluon code so far you are likely to have already encountered this with numeric operators such as `(+)` or comparison operators such as `(==)`. While these operators are core parts of gluon they are not special cased by the compiler which lets you define and use overloaded bindings yourself.
+
+To explain how overloading works first look at the example below where `show_type` has two implementations, one which takes an `Int` and one which takes a `Float`.
+
+```f#,rust
+let show_type _ : Int -> String = "Int"
+let show_type _ : Float -> String = "Float"
+
+show_type 0 // Returns "Int"
+show_type 0.0 // Returns "Float"
+// show_type "" // Would be a type error
+```
+
+When the typechecker encounters the second `show_type` binding in this example it does not simply shadow the first binding as is common in many programming languages. Instead the typechecker checks the type of the binding already in scope and calculates the 'intersection' of the two bindings. In the example above the first binding has the type `Int -> String` while the second is `Float -> String`. By calculating the 'intersection' the typechecker calculates the most specialized type which both bindings can still successfully unify to which in this case is `a -> String`. Any subsequent use of `show_type` will then be observed as `a -> String` which succeeds with both a `Int` and `Float` argument.
+
+Unfortunately it would also succeed if a `String` (or any other) type were used as the argument which is not acceptable as we have only implemented `show_type` for `Int` and `Float`. To catch this case (and to figure out which overload should be use where) the typechecker does an extra pass after successfully typechecking the entire expression. In this pass all uses of overloaded bindings are checked against the overload candidates until a match is found. Thus the third call, were it not commented out, would produce an error as there is no overloaded binding matching the type `String -> String`.
+
 ## Importing modules
 
 As is often the case it is convenient to separate code into multiple files which can later be imported and used from multiple other files. To do this we can use the `import` macro which takes a single string literal as argument and loads and compiles that file at compile time before the importing module is compiled.