updates

data/tutorials/language/0lg_10_polymorphic_variants.md

@@ -10,53 +10,56 @@ category: "Language"
 
 ## Introduction
 
-Product types and data types such as `option` and `list` are variants and polymorphic. In this tutorial, they are called _simple variants_ to distinguished them the _polymorphic variants_ presented tutorial. Simple variants and polymorphic variants are close siblings. Their values are both introduced using labels that may carry data. Both can be recursive and have type parameters. Both are typed checked statically.
+Product types and data types such as `option` and `list` are variants and polymorphic. In this tutorial, they are called _simple variants_ to distinguish them from the _polymorphic variants_ presented in this tutorial. Simple variants and polymorphic variants are close siblings. Their values are both introduced using labels that may carry data. Both can be recursive and have type parameters. Both are statically type-checked.
 
-However, they are type checked using very different algorithms, which result in a very different programming experience. The relationship between value and type (writen with the colon symbol `:`) is changed with polymorphic variants. Usually, values are though as inhabitants of the type, which is though as a set-like things. Polymorphic variant values should rather be thought as pieces of data that can be accepted by functions and polymorphic variant types a way to express compabitibity relationship between those functions. The approach in this tutorial is to build sense from experience using features of polymorphic variants.
+However, they are type checked using very different algorithms, which result in a very different programming experience. The relationship between value and type (writen with the colon symbol `:`) is changed with polymorphic variants. Usually, values are seen as inhabitants of a type, which is though as a set-like things. Polymorphic variant values should rather be thought as pieces of data that can be accepted by functions and polymorphic variant types a way to express compabitibity relationship between those functions. The approach in this tutorial is to build sense from experience using features of polymorphic variants.
 
 By the way, don't trust ChatGPT if it tells you polymorphic variants are dynamically type-checked, it is hallucinating.
 
 ### Origin and Context
 
 Polymorphic variants origins from Jacques Garrigue work on Objective Label, which was [first published in 1996](https://caml.inria.fr/pub/old_caml_site/caml-list-ar/0533.html). It became part of stantard OCaml in [release 3.0](https://caml.inria.fr/distrib/ocaml-3.00/), in 2000, along with labelled and optional function arguments.
 
-The core type system of OCaml follows a [_nominal_](https://en.wikipedia.org/wiki/Nominal_type_system) discipline. Types are explicitely declared. The typing discipline used for polymorphic variants and classes is different, it is [_structural_](https://en.wikipedia.org/wiki/Structural_type_system).
+The core type system of OCaml follows a [_nominal_](https://en.wikipedia.org/wiki/Nominal_type_system) discipline. Types are first explicitely declared, later they are used. The typing discipline used for polymorphic variants and classes is different, it is [_structural_](https://en.wikipedia.org/wiki/Structural_type_system).
 
-In the nominal approach of typing, types are first defined; later, when type-checking an expression, three outcomes are possible
+In the nominal approach of typing, types are first defined; later, when type-checking an expression, three outcomes are possible:
 1. If a matching type is found, it becomes the infered type
 1. If any type can be applied, a type variable is created
 1. If typing inconsistencies are found, an error is raised
 
 This is very similar to solving an equation in mathematics. Equation on numbers accepts either zero, exactly one, several or infinitely many solutions. Nominal type checking finds that either zero, exactly one or any type can be used in an expression.
 
-In the structural approach of typing, type definitions are optional, they can be omitted. Type checking an expression constructs a data structure that represents the types which are compatible with it. These data structures are displayed as type expressions sharing ressemblance with simple variants.
+In the structural approach of typing, type definitions are optional, they can be omitted. Type checking an expression constructs a data structure that represents types which are compatible with it. These data structures are displayed as type expressions sharing ressemblance with simple variants but turns out to have pretty different meaning.
 
 ### Learning Goals
 
 The goal of this tutorial is to make the reader acquire the following capabilities:
+- Write polymorphic variant using code, from strach, using mainstream features
+- Maintain existing code that is using polymorphic variants
 - Sort out polymorphic variant types and errors
   - Add type annotation needed to resolve polymorphic variant type-checking issues
   - Add or remove catch all patterns in polymorphic variant pattern matching
+  - Insert or remove type casts
 - Refactor between simple and polymorphic variants
 - Choose to use polymorphic variant when really needed
 
 ### Variants and Polymorphism
 
-The type expression `'a list` does not designate a single type, it designates a family of types, all the types that can be created by substituing an actual type to type variable `'a`. The type expressions `int list`, `bool option list` or `(float -> float) list list` are real types, actual members of the family `'a list`. The identifiers `list`, `option` and others are type operators. Just like functions, they take parameters, except the parameters are not values, they are types; and result isn't a value but a type too. Therfore, simple variants are polymorphic, but not in the same sense as polymorphic variants.
+The type expression `'a list` does not designate a single type, it designates a family of types, all the types that can be created by substituing an actual type to type variable `'a`. The type expressions `int list`, `bool option list` or `(float -> float) list list` are real types, with associated values. They are example members of the family `'a list`. The identifiers `list`, `option` and others are type operators. Just like functions, they take parameters, except those parameters are not values, they are types; and result aren't values but a type too. Therfore, simple variants are polymorphic, but not in the same sense as polymorphic variants.
 - Simple variants have [parametric poymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism)
 - Polymorphic variants have a form of [structural polymorphism](https://en.wikipedia.org/wiki/Structural_type_system)
 
 ## A First Example
 
 ### Creating Polymorphic Variant Types From Pattern Matching
 
-Polymorphic variant visual signature are backquotes. Pattern matching on them looks just the same as with simple variants, except for backquotes (and capitals, which are not longer required).
+Polymorphic variant visual signature are backquotes. Pattern matching on them looks just the same as with simple variants, except for backquotes (and capitals, which are not longer mandatory). Here is a first example:
 ```ocaml
 # let f = function `Broccoli -> "Broccoli" | `Fruit name -> name;;
 f : [< `Broccoli | `Fruit of string ] -> string = <fun>
 ```
 
-Here`` `Broccoli`` and`` `Fruit`` plays a role similar to the role played by the constructors `Broccoli` and `Fruit` in a variant declared as `type t = Broccoli | Fruit of string`. Except, and most importantly, that the definition doesn't need to be written. The tokens`` `Broccoli`` and `` `Fruit`` are called _tags_ instead of constructors. A tag is defined by a name and a list of parameter types.
+Here`` `Broccoli`` and`` `Fruit`` plays a role similar to the role played by the constructors `Broccoli` and `Fruit` in a variant declared as `type t = Broccoli | Fruit of string`. Except, and most importantly, that the type definition doesn't need to be written. The tokens`` `Broccoli`` and `` `Fruit`` are called _tags_ instead of constructors. A tag is defined by a name and a list of parameter types.
 
 The expression ``[< `Broccoli | `Fruit of string ]`` play the role of a type. However, it does not represent a single type, it represents three different types.
 - The type that only has`` `Broccoli`` as inhabitant, its translation into a simple variant is `type t0 = Broccoli`
@@ -67,12 +70,12 @@ Note each of the above translations into simple variants is correct. However, en
 
 This also illustrates the other strinking feature of polymorphic variants: values can be attached to several types. For instance, the tag `` `Broccoli`` inhabits ``[ `Broccoli ]`` and``[ `Broccoli | `Fruit of String ]``, but it also inhabits any type that containts it.
 
-What is displayed by the type-checker, for instance ``[< `Broccoli | `Fruit of string ]``, isn't a single type. It is a type expression that designates a contrained set of types. For instance, all types defined by a group of tags that contains either`` `Broccoli`` or `` `Fruit of string`` and nothing more. This is the meaning of the `<` sign in this type expression. This a bit similar to what happens with `'a list`, which isn't a single type either, but a type expression that desginates the set of `list` types of something, i.e. the set of types where `'a` has been replaced by some other type.
+What is displayed by the type-checker, for instance ``[< `Broccoli | `Fruit of string ]``, isn't a single type. It is a type expression that designates a constrained set of types. For instance, all types defined by a group of tags that contains either`` `Broccoli`` or `` `Fruit of string`` and nothing more. This is the meaning of the `<` sign in this type expression. This a bit similar to what happens with `'a list`, which isn't a single type either, but a type expression that desginates the set of lists of something, i.e. the set of types where `'a` has been replaced by some other type.
 
-This is the sense of the polymorphism of polymorphic variants. Polymorphic variants types are type expressions. The structural typing algorithm used for polymorphic variants creates type expressions that designate sets of types (here the three types above), which are defined by contraints on sets of tags (the inequality symbols). The polymorphism of polymorphic variant is different.
+This is the sense of the polymorphism of polymorphic variants. Polymorphic variants types are type expressions. The structural typing algorithm used for polymorphic variants creates type expressions that designate sets of types (here the three types above), which are defined by contraints on sets of tags: the inequality symbols. The polymorphism of polymorphic variant is different.
 
 In the rest of this tutorial, the following terminology is used:
-- “simple variants”
+- “simple variants”: product types and variants such as `list`, `option` and others
 - polymorphic variant: type expressions displayed by the OCaml type-checker such as ``[< `Broccoli | `Fruit of string ]``
 
 ### Tag Sharing
@@ -89,7 +92,7 @@ val g : [< `Broccoli | `Edible of string ] -> string = <fun>
 - : string = "Brassica oleracea var. italica"
 ```
 
-Both `f` and `g` accepts the`` `Broccoli`` tag as input because they both have code for it. They do not have the same domain because `f` also accepts `` `Fruit of string`` whilst `g` also accepts `` `Edible of string``. The types of the domains of `f` and `g` expresses this. The tag `` `Broccoli`` satisfies the both the constraints of the domain of `f`: ``[< `Broccoli | `Fruit of string ]`` and the contraints of the domain of `g`: ``[< `Broccoli | `Fruit of string ]``. That type is ``[ `Broccoli ]``. The same way tag defined values belong to several types, tag accepting functions belong to several types too.
+Both `f` and `g` accepts the`` `Broccoli`` tag as input because they both have code for it. They do not have the same domain because `f` also accepts `` `Fruit`` whilst `g` accepts `` `Edible`` instead. The types of the domains of `f` and `g` expresses this. The tag `` `Broccoli`` satisfies the both the constraints of the domain of `f`: ``[< `Broccoli | `Fruit of string ]`` and the contraints of the domain of `g`: ``[< `Broccoli | `Fruit of string ]``. The same way tag defined values belong to several types, tag accepting functions belong to several types too.
 
 ### Static Type Checking