<div dir="ltr">Div was introduced in GHC 8.4, I believe.</div><br><div class="gmail_quote"><div dir="ltr">пн, 3 дек. 2018 г. в 05:49, Amy de Buitléir <<a href="mailto:amy@nualeargais.ie">amy@nualeargais.ie</a>>:<br></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>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">
<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" target="_blank">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" rel="noopener noreferrer" target="_blank">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="m_1730073336056407060gmail_signature" dir="ltr">
<div dir="ltr">
<div>
<div dir="ltr">
<div>brandon s allbery kf8nh</div>
<div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a></div>
</div>
</div>
</div>
</div>
</blockquote>
<p><br></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" rel="noreferrer" target="_blank">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>