<html><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /></head><body style='font-size: 10pt; font-family: Verdana,Geneva,sans-serif'>
<p>Ah, thank you, that makes perfect sense. For anyone else who struggles with that example, you also need :set -XTypeOperators and import GHC.TypeLits.</p>
<p>λ> :set -XDataKinds<br />λ> :set -XTypeOperators<br />λ> import GHC.TypeLits<br />λ> :kind! (1 + 17) * 3<br />(1 + 17) * 3 :: Nat<br />= 54</p>
<p>Unfortunately, I also get an error on the next line:</p>
<p>λ> :kind! (Div 128 8) ^ 2<br /><br /><interactive>:1:2: error:<br /> Not in scope: type constructor or class ‘Div’</p>
<p>Div is defined in GHC.TypeLits, so I don't understand why that didn't work.</p>
<p><br /></p>
<p>On 2018-12-03 00:12, Brandon Allbery wrote:</p>
<blockquote type="cite" style="padding: 0 0.4em; border-left: #1010ff 2px solid; margin: 0"><!-- html ignored --><!-- head ignored --><!-- meta ignored -->
<div dir="ltr">That looks like someone had a search-and-replace error.
<div> </div>
<div>It used to be that the kind of normal values was *. Type level math made this problematic; by default, in recent ghc that kind is called Type instead. (See the StarIsType LANGUAGE pragma.)</div>
<div> </div>
<div>So someone did a search and replace to fix the kinds, and changed what should have been a type level multiplication by accident. Change it to a*.</div>
</div>
<br />
<div class="gmail_quote">
<div dir="ltr">On Sun, Dec 2, 2018 at 7:09 PM Amy de Buitléir <<a href="mailto:amy@nualeargais.ie">amy@nualeargais.ie</a>> wrote:</div>
<blockquote class="gmail_quote" style="margin: 0 0 0 .8ex; border-left: 1px #ccc solid; padding-left: 1ex;">
<div style="font-size: 10pt; font-family: Verdana,Geneva,sans-serif;">
<p>I'm reading "Thinking with Types" by Sandy Maguire, and there's a bit of code on p. 27 that I don't understand and can't get to work. The "Type 3" seems to have the effect of multiplying by 3.</p>
<p>> :set -XDataKinds<br />> :set -XTypeOperators<br />> :kind! (1 + 17) Type 3</p>
<p>(1 + 17) Type 3 :: Nat<br />= 54</p>
<p>But it doesn't work for me. When I try this, I get...</p>
<p>$ ghci --version<br />The Glorious Glasgow Haskell Compilation System, version 8.2.2</p>
<p>$ ghci</p>
<p>λ> :set -XDataKinds<br />λ> :set -XTypeOperators<br />λ> :kind! (1 + 17) Type 3<br /><br /><interactive>:1:2: error:<br /> Not in scope: type constructor or class '+'<br /><br /><interactive>:1:10: error:<br /> Not in scope: type constructor or class 'Type'</p>
</div>
_______________________________________________<br /> Haskell-Cafe mailing list<br /> To (un)subscribe, modify options or view archives go to:<br /> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank" rel="noopener noreferrer">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br /> Only members subscribed via the mailman list are allowed to post.</blockquote>
</div>
<br clear="all" />
<div> </div>
-- <br />
<div class="gmail_signature" dir="ltr">
<div dir="ltr">
<div>
<div dir="ltr">
<div>brandon s allbery kf8nh</div>
<div><a href="mailto:allbery.b@gmail.com">allbery.b@gmail.com</a></div>
</div>
</div>
</div>
</div>
</blockquote>
<p><br /></p>
</body></html>