[Haskell-cafe] Can't get Type 3" to work

[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'

[Brandon Allbery]

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*.

Post by 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
Not in scope: type constructor or class ‘+’
Not in scope: type constructor or class ‘Type’
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[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.

Post by Brandon Allbery
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*.

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
Not in scope: type constructor or class '+'
Not in scope: type constructor or class 'Type' _______________________________________________
Haskell-Cafe mailing list
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

[Alexey Vagarenko]

Div was introduced in GHC 8.4, I believe.

Post by 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
λ> :kind! (Div 128 8) ^ 2
Not in scope: type constructor or class ‘Div’
Div is defined in GHC.TypeLits, so I don't understand why that didn't work.
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*.

Post by 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
Not in scope: type constructor or class '+'
Not in scope: type constructor or class 'Type'
_______________________________________________
Haskell-Cafe mailing list
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
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Amy de Buitléir]

Thank you. I upgraded my GHC and it works now.

Post by Alexey Vagarenko
Div was introduced in GHC 8.4, I believe.