<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 9, 2021 at 10:11 AM Galaxy Being <<a href="mailto:borgauf@gmail.com">borgauf@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Getting stuck in <i>Real World Haskell</i>'s chapter on pretty printing (chap 5), I decided to take a look at one of the suggested sources, i.e., John Hughes' <i><a href="https://www.researchgate.net/publication/226525714_The_Design_of_a_Pretty-printing_Library" target="_blank">The Design of a Pretty-printing Library</a></i>. Not that I fully got the first three section, still, let me skip ahead to section 4, <i>Designing a Sequence Type </i>where we're designing a supposedly generic sequence type, I'm guessing in the same universal, fundamental way that Peano's Axioms give a generic underpinning of the natural numbers. Good. I get it. This is why Haskell is unique. So he says we take the following <i>signature</i> as our starting point</div><div><br></div><div><font face="monospace">nil :: Seq a<br>unit :: a -> Seq a<br>cat :: Seq a -> Seq a -> Seq a<br>list :: Seq a -> [a]<br></font></div><br clear="all"><div>where <font face="monospace">nil , unit ,</font> and <font face="monospace">cat </font>give us ways to build sequences, and <font face="monospace">list</font> is an <i>observation </i>[explained before]. The correspondence with the usual list operations is</div><div><br><font face="monospace">nil = []<br>unit x = [x]<br>cat = (++)</font></div><div><br>These operations are to satisfy the following laws:</div><div><br><font face="monospace">xs `cat` ( ys `cat` zs ) = ( xs `cat` ys ) `cat` zs<br>nil `cat` xs = xs<br>xs `cat` nil = xs<br>list nil = []<br>list ( unit x `cat` xs ) = x : list xs</font><br></div><div><br></div><div>My first question is why must we satisfy these laws? Where did these laws come from? Is this a universal truth thing? I've heard the word <i>monoid </i>and <i>semigroup</i> tossed around. Is this germane here?</div></div></blockquote><div><br></div><div>This is how the paper defines what the word Sequence means in a mathematical way, otherwise there might be some ambiguity for what a Sequence should be. The laws are the design for the Sequence type. Some of them also happen to be the laws that define Monoid and Semigroup.</div><div><br></div><div>The first law is associativity, which means Sequence can implement Semigroup. The next two laws are the identity laws, which means Sequence can implement Monoid. <a href="https://wiki.haskell.org/Monoid#The_basics">https://wiki.haskell.org/Monoid#The_basics</a></div><div> <br></div><div>The last two laws say that you can take any Sequence and make a list out of it without losing any information (all elements in the same order). This is also related to Foldable but it's stronger because of the ordering. <a href="https://wiki.haskell.org/Foldable_and_Traversable">https://wiki.haskell.org/Foldable_and_Traversable</a></div><div><br></div><div>Reading all of the laws together (Monoid + Foldable with ordering) you can infer that Sequence is isomorphic to list. With <font face="monospace">mconcat</font> you can turn a list into a Sequence and with <font face="monospace">list</font><font face="arial, sans-serif"> you can get the original list back. This also means that Sequence should be able to lawfully (but perhaps not as efficiently) implement any other typeclass or operation that is implemented for list.</font></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Next in <i>4.1 Term Representation</i> I'm immediately lost with the concept of <i>term. </i>On a hunch, I borrowed a book <i>Term Rewriting and All That </i>from Baader and Nipkow which I'm sure goes very deep into the concept of terms, but I'm not there yet. What is meant by <i>term</i>? As 4.1 continues, confusing is this passage</div><div><br></div><div>The most direct way to represent values of [the?] sequence type is just as terms of the<br>algebra [huh?], for example using</div><div><br><font face="monospace">data Seq a = Nil j Unit a j Seq a `Cat` Seq a</font></div><div><br>But this trivial representation does not exploit the algebraic laws that we know to<br>hold [huh?], and moreover the list observation will be a little tricky to de ne (ideally we would like to implement observations by very simple, non-recursive functions: the real work should be done in the implementations of the Seq operators themselves). Instead, we may choose a restricted subset of terms -- call them simplified forms -- into which every term can be put using the algebraic laws. Then we can represent sequences using a datatype that represents the syntax of simplified forms.</div></div></blockquote><div><br></div><div>This essentially states that the <font face="monospace">Unit a</font> constructor is redundant because it's equivalent to <font face="monospace">Seq a Nil</font><font face="arial, sans-serif">. Having fewer possible representations greatly simplifies how easy it is to reason about a data type and usually also simplifies its implementation.</font></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>In this case, there is an obvious candidate for simplified forms: terms of the form <font face="monospace">nil </font>and <font face="monospace">unit x `cat` xs</font> , where <font face="monospace">xs</font> is also in simplified form. Simplified forms can be represented using the type</div><div><br></div><div><span style="font-family:monospace">data Seq a = Nil j a `UnitCat` Seq a</span></div><div><font face="monospace"><br></font>with the interpretation</div><div><br><font face="monospace">Nil = nil<br>x `UnitCat` xs = unit x `cat` xs</font><br></div><div><font face="monospace"><br></font></div><div><font face="arial, sans-serif">All of this presupposes much math lore that I'm hereby asking someone on this mailing list to point me towards. I threw in a few [huh?] as specific points, but in general, I'm not there yet. Any explanations appreciated.</font></div></div></blockquote><div><br></div><div>This section of the paper explains how a first attempt at implementing a Sequence type from first principles could end up with a representation that is indistinguishable from the list type other than the names (<font face="monospace">nil = []; cat = (:)</font>). The important part is the end of <b>4.1</b> where we learn why this representation doesn't have the desired performance characteristics for this use case and then in <b>4.2</b> a more suitable representation is derived.</div><div> </div><div>-bob</div><div><br></div></div></div>