diff options
Diffstat (limited to 'documentation/book/the_lux_programming_language/chapter_6.md')
| -rw-r--r-- | documentation/book/the_lux_programming_language/chapter_6.md | 167 |
1 files changed, 95 insertions, 72 deletions
diff --git a/documentation/book/the_lux_programming_language/chapter_6.md b/documentation/book/the_lux_programming_language/chapter_6.md index a57ff4913..61582d1bf 100644 --- a/documentation/book/the_lux_programming_language/chapter_6.md +++ b/documentation/book/the_lux_programming_language/chapter_6.md @@ -9,18 +9,20 @@ We've talked about Lux types already, but only in a very high-level way. On this chapter, you'll see how types are constructed, and hopefully that will give you some insight to understand better the subjects of later chapters. ```clojure -(type: #export #rec Type - (#Primitive Text (List Type)) - (#Sum Type Type) - (#Product Type Type) - (#Function Type Type) - (#Parameter Nat) - (#Var Nat) - (#Ex Nat) - (#UnivQ (List Type) Type) - (#ExQ (List Type) Type) - (#Apply Type Type) - (#Named Name Type)) +(type: .public Type + (Rec Type + (Variant + {#Primitive Text (List Type)} + {#Sum Type Type} + {#Product Type Type} + {#Function Type Type} + {#Parameter Nat} + {#Var Nat} + {#Ex Nat} + {#UnivQ (List Type) Type} + {#ExQ (List Type) Type} + {#Apply Type Type} + {#Named Name Type}))) ``` This is the type of types. @@ -31,53 +33,65 @@ But as I've said before, Lux types are values like any other. `Type` is a variant type, which just means that there are multiple options for type values. -Also, you may have noticed that `#rec` tag in the definition. You need to add it whenever you're defining a recursive type that takes no parameters. +Also, you may have noticed that `Rec` macro in the definition. + +You need to add it whenever you're defining a recursive type that takes no parameters. So, the definition of `List` doesn't need it, but the definition of `Type` does. -Let's go over each of them. +Let's go over each option for `Type`. --- ```clojure -(#Primitive Text (List Type)) +{#Primitive Text (List Type)} ``` -This is what connects Lux's type-system with the host platform's. These types represent classes (in the JVM), with their respective parameters, if they have them (as would be the case for `ArrayList<Long>` in the JVM). +This is what connects Lux's type-system with the host platform's. + +These types represent classes (in the JVM) with their respective parameters, if they have them (as would be the case for `ArrayList<Long>` in the JVM). --- ```clojure -(#Sum Type Type) -(#Product Type Type) +{#Sum Type Type} +{#Product Type Type} ``` -You may have noticed that none of those options are called `#Variant` or `#Tuple`. The reason is that variants and tuples are just names for mathematical constructs called "sums" and "products". Funny names, right? +You may have noticed that none of those options are called `#Variant` or `#Tuple`. + +The reason is that variants and tuples are just names for mathematical constructs called _"sums"_ and _"products"_. + +Funny names, right? -Well, mathematicians see variants as a way of "adding" types and tuples as a way of "multiplying" types, Of course, it's a bit difficult to picture that if you're thinking of numbers. +Well, mathematicians see variants as a way of "adding" types and tuples as a way of "multiplying" types. -But a way to see variants is as an _"OR"_ operation for types: you get this option _OR_ that option. Conversely, tuples are like an _"AND"_ operation for types: you get this type _AND_ that type. +Of course, it's a bit difficult to picture that if you're thinking of numbers. -But, you may be wondering: "why do `#Variant` and `#Tuple` only take 2 types, instead of a list like `#Primitive` does?" +But a way to see variants is as an _"OR"_ operation for types: you get this option _OR_ that option. -Well, as it turns out, you don't need a list of types to implement variants and tuples, because you can actually chain `#Variant` and `#Tuple` with other instances of themselves to get the same effect. +Conversely, tuples are like an _"AND"_ operation for types: you get this type _AND_ that type. + +But, you may be wondering: "why do `#Sum` and `#Product` only take 2 types, instead of a list like `#Primitive` does?" + +Well, as it turns out, you don't need a list of types to implement variants and tuples, because you can actually chain `#Sum` and `#Product` with other instances of themselves to get the same effect. What do I mean? Well, let me show you. To the left, you'll see the type as it's written in normal Lux code, and to the right you'll see the type value it generates. ```clojure -(|) => Nothing -(| Bit) => Bit -(| Bit Int) => (#Sum Bit Int) -(| Bit Int Real) => (#Sum Bit (#Sum Int Real)) -(| Bit Int Real Char) => (#Sum Bit (#Sum Int (#Sum Real Char))) - -(&) => Any -(& Bit) => Bit -(& Bit Int) => (#Product Bit Int) -(& Bit Int Real) => (#Product Bit (#Product Int Real)) -(& Bit Int Real Char) => (#Product Bit (#Product Int (#Product Real Char))) +(Or) => Nothing +(Or Bit) => Bit +(Or Bit Int) => {#Sum Bit Int} +(Or Bit Int Real) => {#Sum Bit {#Sum Int Real}} +(Or Bit Int Real Char) => {#Sum Bit {#Sum Int {#Sum Real Char}}} + +(And) => Any +(And Bit) => Bit +(And Bit Int) => {#Product Bit Int} +(And Bit Int Real) => {#Product Bit {#Product Int Real}} +(And Bit Int Real Char) => {#Product Bit {#Product Int {#Product Real Char}}} ``` You can see where this is going. @@ -86,21 +100,25 @@ If I have a way to to pair up 2 types, and I can nest that, then I can chain thi What is a variant/tuple of 1 type? It's just the type itself; no pairing required. -This embedding means that [true 123 456.789 "X"] is the same as [true [123 456.789 "X"]], and the same as [true [123 [456.789 "X"]]]. +This embedding means that `[true 123 456.789 "X"]` is the same as `[true [123 456.789 "X"]]`, and the same as `[true [123 [456.789 "X"]]]`. -It also means 5 is the same as [5], and [[5]], and [[[[[5]]]]]. +It also means `5` is the same as `[5]`, and `[[5]]`, and `[[[[[5]]]]]`. As far as the compiler is concerned, there are no differences. -That might sound crazy, but there are some really cool benefits to all of this. If you're curious about that, you can check out [Appendix E](appendix_e.md) for more information on how Lux handles this sort of stuff. +That might sound crazy, but there are some really cool benefits to all of this. + +If you're curious about that, you can check out [Appendix E](appendix_e.md) for more information on how Lux handles this sort of stuff. -And what happens when the variant/tuple has 0 types? That's when `Nothing` and `Any` come into play. +And what happens when the variant/tuple has 0 types? + +That's when `Nothing` and `Any` come into play. `Nothing` is a type that has no instances; which is to say, there's no expression which can yield a value of such a type. It might seem oddd to have a type which has no instancces, but it can be useful to model computations which fail at runtime (thereby yielding no value). -So, another way of thinking of `Nothing` is as the type of failed expressions. +So, another way of thinking of `Nothing` is as the type of failed/erroneous computations. `Any`, on the other hand, is the opposite. @@ -108,7 +126,7 @@ You can think of it as the super-type of all other types: the type of all values This means that not only `(: Nat 123)`, but also `(: Any 123)`. -Since `Any` does not give you any specific information about a value, it only tells you that a value exists, regardless of what its specific type happens to be. +This works because `Any` does not give you any specific information about a value, it only tells you that a value exists, regardless of what its specific type happens to be. So, whenever a function accepts or returns a dummy value of some kind, `Any` is a good candidate for that. @@ -123,9 +141,10 @@ You might think that dummy values are, well, _dumb_, but they show up all the ti Consider the `Maybe` type: ```clojure -(type: #export (Maybe a) - #None - (#Some a)) +(type: .public (Maybe a) + (Variant + {#None} + {#Some a})) ``` The `#Some` tag holds values of type `a`, but what does `#None` hold? Nothing? @@ -133,7 +152,7 @@ The `#Some` tag holds values of type `a`, but what does `#None` hold? Nothing? Well, `Maybe` is a variant, which means it's a `#Sum`, which looks like this: ```clojure -(#Sum Type Type) +{#Sum Type Type} ``` So we know that `#None` must hold _something_. But what? @@ -143,23 +162,19 @@ Well, `Any`thing, really. So the type definition for `Maybe` is equivalent to this: ```clojure -(type: #export (Maybe a) - (#None Any) - (#Some a)) +(type: .public (Maybe a) + {#None Any} ... Alternatively, {#None []} + {#Some a}) ``` If you don't care what value you store somewhere, then you can store `Any` value in there. -In practice, you can create instances of `Maybe` by writing this `(#None [])`, or `(#None 123)`, or just `#None`. - -If you only write the tag, then Lux treats it as if you paired it up with an empty tuple. - -So `#None` is equivalent to `(#None [])`. +In practice, you can create instances of `Maybe` by writing this `{#None []}`, or `{#None 123}`, or just `{#None}`. --- ```clojure -(#Function Type Type) +{#Function Type Type} ``` Now that we have discussed variant and tuple types, it shouldn't come as a surprise that a similar trick can be done with function types. @@ -168,7 +183,7 @@ You see, if you can implement functions of 1 argument, you can implement functio All I need to do is to embed the rest of the function as the return value to the outer function. - It might sound like this whole business of embedding tuples, variants and functions inside one another must be super inefficient; but trust me: Lux has taken care of that. + It might sound like this whole business of embedding variants, tuples and functions inside one another must be super inefficient; but trust me: Lux has taken care of that. The Lux compiler features many optimizations that compile things down in a way that gives you maximum efficiency. So, to a large extent, these embedded encodings are there for the semantics of the language, but not as something that you'll pay for at run-time. @@ -179,7 +194,7 @@ Yep, that's a direct consequence of this theoretical model. --- ```clojure -(#Parameter Nat) +{#Parameter Nat} ``` This type is there mostly for keeping track of type-parameters in _universal and existential quantification_. @@ -189,7 +204,7 @@ We'll talk about those later. But, suffice it to say that `#Parameter` helps the --- ```clojure -(#Var Nat) +{#Var Nat} ``` These are type variables. @@ -203,37 +218,43 @@ Type-variables, however, cannot be _re-bound_ once they have been set, to avoid --- ```clojure -(#Ex Nat) +{#Ex Nat} ``` An existential type is an interesting concept (which is related, but not the same as existential quantification). -You can see it as a type that exists, but is unknown to you. It's like receiving a type in a box you can't open. +You can see it as a type that exists, but is unknown to you. + +It's like receiving a type in a box you can't open. -What can you do with it, then? You can compare it to other types, and the comparison will only succeed if it is matched against itself. +What can you do with it, then? + +You can compare it to other types, and the comparison will only succeed if it is matched against itself. It may sound like a useless thing, but it can power some advanced techniques. --- ```clojure -(#UnivQ (List Type) Type) +{#UnivQ (List Type) Type} ``` This is what the `All` macro generates: _universal quantification_. -That `(List Type)` you see there is meant to be the _context_ of the universal quantification. It's kind of like the environment of a function closure, only with types. +That `(List Type)` you see there is meant to be the _context_ of the universal quantification. + +It's kind of like the environment of a function closure, only with types. The other `Type` there is the _body_ of the universal quantification. To understand better what's going on, let's transform the type of our `iterate_list` function from [Chapter 5](chapter_5.md) into its type value. ```clojure -(All [a b] (-> (-> a b) (List a) (List b))) +(All (_ a b) (-> (-> a b) (List a) (List b))) -## => +... => -## (#.UnivQ #.End (#.UnivQ #.End (-> (-> (#.Parameter 3) (#.Parameter 1)) (List (#.Parameter 3)) (List (#.Parameter 1)))) +... {.#UnivQ {.#End} {.#UnivQ {.#End} (-> (-> {.#Parameter 3} {.#Parameter 1}) (List {.#Parameter 3}) (List {.#Parameter 1})}} ``` **Note**: I didn't transform the type entirely to avoid unnecessary verbosity. @@ -242,24 +263,24 @@ As you can see, I do the same embedding trick to have universal quantification w Also, `a` and `b` are just nice syntactic labels that get transformed into `#Parameter` types. - The reason the type-parameters have those IDs is due to a technique called [De Bruijn Indices](https://en.wikipedia.org/wiki/De_Bruijn_index). + The reason the type-parameters have those numeric IDs is due to a technique called [De Bruijn Indices](https://en.wikipedia.org/wiki/De_Bruijn_index). --- ```clojure -(#ExQ (List Type) Type) +{#ExQ (List Type) Type} ``` Existential quantification works pretty much the same way as universal quantification. Its associated macro is `Ex`. -Whereas universal quantification works with type-variables, existential quantification works with existential types. +Where universal quantification works with type-variables, existential quantification works with existential types. --- ```clojure -(#Apply Type Type) +{#Apply Type Type} ``` This is the opposite of quantification. @@ -268,14 +289,14 @@ This is the opposite of quantification. With `#Apply`, `(List Int)` transforms into `(#Apply Int List)`. -For multi-parameter types, like `Dictionary` (from `lux/data/collection/dictionary`), `(Dictionary Text User)` would become `(#Apply User (#Apply Text Dictionary))`. +For multi-parameter types, like `Dictionary` (from `library/lux/data/collection/dictionary`), `(Dictionary Text User)` would become `(#Apply User (#Apply Text Dictionary))`. As you can see, the nesting is slightly different than how it is for tuples, variant and functions. --- ```clojure -(#Named Name Type) +{#Named Symbol Type} ``` `#Named` is less of a necessity and more of a convenience. @@ -298,9 +319,11 @@ That may sound odd (if you come from Java or other languages with nominal types) ## Regarding Error Messages -When you get error messages from the type-checker during your coding sessions, types will show up in intuitive ways most of the time, with a few exceptions you might want to know. +When you get error messages from the type-checker during your coding sessions, types will show up in intuitive ways most of the time, with a few exceptions you might want to know about. + +Existential types show up in error messages like `⟨e:246⟩` (where 246 is the ID of the type). -Existential types show up in error messages like `⟨e:246⟩` (where 246 is the ID of the type). Whereas type-variables show up like `⌈v:278⌋`. +Whereas type-variables show up like `⌈v:278⌋`. Those types tend to show up when there are errors in the definition of some polymorphic function. |