Can't get Type 3" to work

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.
:set -XDataKinds :set -XTypeOperators :kind! (1 + 17) Type 3
(1 + 17) Type 3 :: Nat = 54 But it doesn't work for me. When I try this, I get... $ ghci --version The Glorious Glasgow Haskell Compilation System, version 8.2.2 $ ghci λ> :set -XDataKinds λ> :set -XTypeOperators λ> :kind! (1 + 17) Type 3 <interactive>:1:2: error: Not in scope: type constructor or class '+' <interactive>:1:10: error: Not in scope: type constructor or class 'Type'

That looks like someone had a search-and-replace error.
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.)
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*.
On Sun, Dec 2, 2018 at 7:09 PM Amy de Buitléir
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.
:set -XDataKinds :set -XTypeOperators :kind! (1 + 17) Type 3
(1 + 17) Type 3 :: Nat = 54
But it doesn't work for me. When I try this, I get...
$ ghci --version The Glorious Glasgow Haskell Compilation System, version 8.2.2
$ ghci
λ> :set -XDataKinds λ> :set -XTypeOperators λ> :kind! (1 + 17) Type 3
<interactive>:1:2: error: Not in scope: type constructor or class ‘+’
<interactive>:1:10: error: Not in scope: type constructor or class ‘Type’ _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
-- brandon s allbery kf8nh allbery.b@gmail.com

Ah, thank you, that makes perfect sense. For anyone else who struggles with that example, you also need :set -XTypeOperators and import GHC.TypeLits. λ> :set -XDataKinds λ> :set -XTypeOperators λ> import GHC.TypeLits λ> :kind! (1 + 17) * 3 (1 + 17) * 3 :: Nat = 54 Unfortunately, I also get an error on the next line: λ> :kind! (Div 128 8) ^ 2 <interactive>:1:2: error: Not in scope: type constructor or class 'Div' Div is defined in GHC.TypeLits, so I don't understand why that didn't work. On 2018-12-03 00:12, Brandon Allbery wrote:
That looks like someone had a search-and-replace error.
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.)
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*.
On Sun, Dec 2, 2018 at 7:09 PM Amy de Buitléir
wrote: 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.
:set -XDataKinds :set -XTypeOperators :kind! (1 + 17) Type 3
(1 + 17) Type 3 :: Nat = 54
But it doesn't work for me. When I try this, I get...
$ ghci --version The Glorious Glasgow Haskell Compilation System, version 8.2.2
$ ghci
λ> :set -XDataKinds λ> :set -XTypeOperators λ> :kind! (1 + 17) Type 3
<interactive>:1:2: error: Not in scope: type constructor or class '+'
<interactive>:1:10: error: Not in scope: type constructor or class 'Type' _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
--
brandon s allbery kf8nh allbery.b@gmail.com

Div was introduced in GHC 8.4, I believe.
пн, 3 дек. 2018 г. в 05:49, Amy de Buitléir
Ah, thank you, that makes perfect sense. For anyone else who struggles with that example, you also need :set -XTypeOperators and import GHC.TypeLits.
λ> :set -XDataKinds λ> :set -XTypeOperators λ> import GHC.TypeLits λ> :kind! (1 + 17) * 3 (1 + 17) * 3 :: Nat = 54
Unfortunately, I also get an error on the next line:
λ> :kind! (Div 128 8) ^ 2
<interactive>:1:2: error: Not in scope: type constructor or class ‘Div’
Div is defined in GHC.TypeLits, so I don't understand why that didn't work.
On 2018-12-03 00:12, Brandon Allbery wrote:
That looks like someone had a search-and-replace error.
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.)
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*.
On Sun, Dec 2, 2018 at 7:09 PM Amy de Buitléir
wrote: 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.
:set -XDataKinds :set -XTypeOperators :kind! (1 + 17) Type 3
(1 + 17) Type 3 :: Nat = 54
But it doesn't work for me. When I try this, I get...
$ ghci --version The Glorious Glasgow Haskell Compilation System, version 8.2.2
$ ghci
λ> :set -XDataKinds λ> :set -XTypeOperators λ> :kind! (1 + 17) Type 3
<interactive>:1:2: error: Not in scope: type constructor or class '+'
<interactive>:1:10: error: Not in scope: type constructor or class 'Type' _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
-- brandon s allbery kf8nh allbery.b@gmail.com
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
Alexey Vagarenko
-
Amy de Buitléir
-
Brandon Allbery