on master help sign in
Lead poly draft
commit8f3bc614d8234b14062d27a5849af1fcb480ad07 authorDavid Kerschner <dkerschner@hcoop.net> dateWed 17 Jul 2019, 18:41 (7 years ago) parent8f0aac3
1 file changed+148
learn/hoon/hoon-tutorial/lead-polymorphism.md+148
learn/hoon/hoon-tutorial/lead-polymorphism.mdnew file+148
@@ -0,0 +1,148 @@
1++++
2+title = "Walkthrough: Lead Polymorphism"
3+weight = 33
4+template = "doc.html"
5++++
6+
7+There are four kinds of cores: gold, iron, zinc, and lead. You are able to use core variance rules to create programs which take other programs as arguments. Which particular rules depends on which kind of core your program needs to complete. Lead cores have opaque payloads. That is, the payload can not be written to or read from. Let's take an example of using lead cores.
8+
9+```
10+=< (to-list (take fib 10))
11+|%
12+++ stream
13+ |* of=mold
14+ $_ ^? |.
15+ ^- $@(~ [item=of more=^$])
16+ ~
17+++ stream-type
18+ |* s=(stream)
19+ $_ => (s)
20+ ?~ . !!
21+ item
22+++ to-list
23+ |* s=(stream)
24+ %- flop
25+ =| r=(list (stream-type s))
26+ |- ^+ r
27+ =+ (s)
28+ ?~ - r
29+ %= $
30+ r [item r]
31+ s more
32+ ==
33+++ take
34+ |* [s=(stream) n=@]
35+ =| i=@
36+ ^+ s
37+ |.
38+ ?: =(i n) ~
39+ =+ (s)
40+ ?~ - ~
41+ :- item
42+ %= ..$
43+ i +(i)
44+ s more
45+ ==
46+++ fib
47+ ^- (stream @ud)
48+ =+ [p=0 q=1]
49+ |. :- q
50+ %= .
51+ p q
52+ q (add p q)
53+ ==
54+--
55+```
56+
57+There are 5 arms in this core: `stream`, `stream-type`, `to-list`, `take`, and `fib`.
58+
59+
60+```
61+++ stream
62+ |* of=mold
63+ $_ ^? |.
64+ ^- $@(~ [item=of more=^$])
65+ ~
66+```
67+
68+`stream` mold builder. It is a wet gate that takes one argument `of` which is a `mold`. `$_` is a rune that produces a type from an example. Here we're going to create a `trap` with `|.` and cast it to lead with `^?`. This means that it's payload will be inaccessible.
69+
70+The output of the `trap` will be cast into a new type. `$@` is the rune to describe a data structure that can either be an atom or a cell. The first part describes the atom which here is going to be `~`. The second half describes a cell with the head of type `of` with the face `item` and a tail with a face of `more`. The expression `^$` is not a rune, but rather a reference to the enclosing wet gate, so the tail of this cell will be of the same type produced by this wet gate.
71+
72+The final `~` here is used as the type produced when initially calling this wet gate. This is valid because it nests within the type we defined on the previous line.
73+
74+Now you can see that a `stream` is either `~` or a pair of a value of some type and a `stream`. This type represents an infinite series.
75+
76+```
77+++ stream-type
78+ |* s=(stream)
79+ $_ => (s)
80+ ?~ . !!
81+ item
82+```
83+
84+`stream-type` is a wet gate that produces the type of items stored in the `stream`. Since calling a `stream`, which is a `trap`, will either produce `item` and `more` or it will produce `~` If it does produce `~` the `stream` is empty and we can't find what type it is so we simply crash with `!!`
85+
86+```
87+++ take
88+ |* [s=(stream) n=@]
89+ =| i=@
90+ ^+ s
91+ |.
92+ ?: =(i n) ~
93+ =+ (s)
94+ ?~ - ~
95+ :- item
96+ %= ..$
97+ i +(i)
98+ s more
99+ ==
100+```
101+
102+We're going to skip over `to-list` and examine `take` first. `take` is another wet gate. This time it takes a `stream` `s` and an `atom` `n`. We add an `atom` to the subject and then make sure that the trap we are creating is going to be of the same type as `s`, the `stream` passed in.
103+
104+If `i` and `n` are equal, the trap will produce `~`. Otherwise, `s` is kicked and it's result put on the front of the subject. If it's value is `~` then the trap again produces `~`. Otherwise the trap produces a cell of `item`, the first part of the value of `s` and a new trap that increments `i` and sets `s` to be the `more` the trap which produces the next value of the `stream`. The result here is a `stream` that will only ever produce `n` items even if the stream otherwise would have been infinite.
105+
106+```
107+++ to-list
108+ |* s=(stream)
109+ %- flop
110+ =| r=(list (stream-type s))
111+ |- ^+ r
112+ =+ (s)
113+ ?~ - r
114+ %= $
115+ r [item r]
116+ s more
117+ ==
118+```
119+
120+Now with that in hand, let's go back to `to-list`. Again it's a wet gate that takes `s`, a `stream` only here it will, as you might expect, produce a `list`. The rest of this gate is straight forward but we can examine it quickly anyway. As is the proper style, this list that is produced will be reversed, so `flop` is used to put it in the order it is in the stream. Recall that adding to the front of a list is cheap, while adding to the back is expensive.
121+
122+`r` is added to the subject as an empty `list` of whatever type is produced by `s`. A new trap is formed and kicked and will produce the same type as `r`. Then `s` is kicked and it's value added to the subject. If the result is `~` the trap produces `r`. Otherwise, we want to call the trap again adding `item` to the front of `r` and changing `s` to `more`. Now the utility of `take` should be clear. We don't want to feed `to-list` an infinite stream as it would never terminate.
123+
124+```
125+++ fib
126+ ^- (stream @ud)
127+ =+ [p=0 q=1]
128+ |. :- q
129+ %= .
130+ p q
131+ q (add p q)
132+ ==
133+```
134+
135+The final arm in this core is `fib` which is a `stream` of `@ud` and therefore an iron core. It's subject contains `p` and `q`, which will not be accessible outside of this trap. The product of the trap is a pair of an `@ud` and the trap that will produce the next `@ud` in the Fibonacci series.
136+
137+
138+```
139+=< (to-list (take fib 10))
140+```
141+
142+Finally, the first line of our program, will take the first 10 elements of `fib` and produce them as a list.
143+
144+```
145+~[1 1 2 3 5 8 13 21 34 55]
146+```
147+
148+This example is a bit over kill for simply calculating the Fibonacci series, but it nicely illustrates how you might use iron cores. Instead of `fib`, you could have any `stream` that produces some stream of values and you'd still be able to use the `take`, `to-list`, and `stream-type` arms.