使用*作为Nat的基元

Question

我目前正在阅读Sandy Maguire的Thinking with Types，第2章介绍术语，类型和种类。其中有一个与类型级基元进行简单交互以在Nat上执行算术的示例。 ] s。

以下会话在本书中显示为有效，但在我的计算机上失败：

Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :set -XDataKinds
Prelude GHC.TypeLits> :set -XTypeOperators
Prelude GHC.TypeLits> :kind! (1 + 17) * 3

<interactive>:1:1: error:
    * Expected kind `* -> Nat -> k0', but `1 + 17' has kind `Nat'
    * In the type `(1 + 17) * 3'

尽管本书中的下一个示例有效：

Prelude GHC.TypeLits> :kind! (128 `Div` 8) ^ 2
(128 `Div` 8) ^ 2 :: Nat
= 256

我怀疑问题与*有关，也表示种类。桑迪·马奎尔（Sandy Maguire）写道，此语法预定用于弃用，但如果仍然存在，我可以看到GHCi认为我的意思是kind *而不是类型级别的[[function *。] >我在正确的轨道上吗？如果是，我可以使用一些标志来使示例工作吗？

我目前正在阅读桑迪·马奎尔的《类型思维》，第二章介绍术语，类型和种类。其中有一个示例，用于与...

Answer 1

我怀疑问题与*有关，也表示 种类。